luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Exact synthesis of majority gates.

This commit is contained in:
Alan Mishchenko 2017-10-01 18:40:30 +03:00
parent d3152aefa7
commit ce8dbc4ac6
2 changed files with 44 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/misc/util/utilTruth.h
View File

@ -1751,6 +1751,22 @@ static inline int Abc_TtFindFirstBit2( word * pIn, int nWords )
return 64*w + Abc_Tt6FirstBit(pIn[w]);
return -1;
}
static inline int Abc_TtFindLastBit( word * pIn, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
for ( w = nWords - 1; w >= 0; w-- )
if ( pIn[w] )
return 64*w + Abc_Tt6LastBit(pIn[w]);
return -1;
}
static inline int Abc_TtFindLastBit2( word * pIn, int nWords )
{
int w;
for ( w = nWords - 1; w >= 0; w-- )
if ( pIn[w] )
return 64*w + Abc_Tt6LastBit(pIn[w]);
return -1;
}
static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
@ -1767,6 +1783,22 @@ static inline int Abc_TtFindFirstDiffBit2( word * pIn1, word * pIn2, int nWords
return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
return -1;
}
static inline int Abc_TtFindLastDiffBit( word * pIn1, word * pIn2, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
for ( w = nWords - 1; w >= 0; w-- )
if ( pIn1[w] ^ pIn2[w] )
return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
return -1;
}
static inline int Abc_TtFindLastDiffBit2( word * pIn1, word * pIn2, int nWords )
{
int w;
for ( w = nWords - 1; w >= 0; w-- )
if ( pIn1[w] ^ pIn2[w] )
return 64*w + Abc_Tt6LastBit(pIn1[w] ^ pIn2[w]);
return -1;
}
static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
@ -1775,14 +1807,6 @@ static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
return 64*w + Abc_Tt6FirstBit(~pIn[w]);
return -1;
}
static inline int Abc_TtFindLastBit( word * pIn, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
for ( w = nWords - 1; w >= 0; w-- )
if ( pIn[w] )
return 64*w + Abc_Tt6LastBit(pIn[w]);
return -1;
}
static inline int Abc_TtFindLastZero( word * pIn, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);

17
src/sat/bmc/bmcMaj.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "bmc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
@ -174,6 +175,7 @@ static inline int Maj_ManFindFanin( Maj_Man_t * p, int i, int k )
}
static inline int Maj_ManEval( Maj_Man_t * p )
{
static int Flag = 0;
int i, k, iMint; word * pFanins[3];
for ( i = p->nVars + 2; i < p->nObjs; i++ )
{
@ -181,7 +183,12 @@ static inline int Maj_ManEval( Maj_Man_t * p )
pFanins[k] = Maj_ManTruth( p, Maj_ManFindFanin(p, i, k) );
Abc_TtMaj( Maj_ManTruth(p, i), pFanins[0], pFanins[1], pFanins[2], p->nWords );
}
iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nWords );
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
else
iMint = Abc_TtFindFirstDiffBit( Maj_ManTruth(p, p->nObjs-1), Maj_ManTruth(p, p->nObjs), p->nVars );
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
}
@ -290,7 +297,6 @@ int Maj_ManAddCnf( Maj_Man_t * p, int iMint )
int iBaseSatVarI = p->iVar + 4*(i - p->nVars - 2);
for ( k = 0; k < 3; k++ )
{
int nLits2 = 0;
for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
{
int iBaseSatVarJ = p->iVar + 4*(j - p->nVars - 2);
@ -346,9 +352,10 @@ void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose )
if ( fVerbose )
{
printf( "Iter %3d : ", i );
printf( "Vars = %5d ", p->iVar );
printf( "Clauses = %5d ", bmcg_sat_solver_clausenum(p->pSat) );
printf( "Conflicts = %7d ", bmcg_sat_solver_conflictnum(p->pSat) );
Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
printf( " Var =%5d ", p->iVar );
printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
printf( "Conf =%8d ", bmcg_sat_solver_conflictnum(p->pSat) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
if ( status == GLUCOSE_UNSAT )