Skip to content

A
abc
Commit c2721889 by Alan Mishchenko
Options

Exact synthesis of majority gates.

parent ce8dbc4a
Showing with 52 additions and 32 deletions
src/base/abci/abc.c
...@@ -8072,17 +8072,17 @@ usage: ...@@ -8072,17 +8072,17 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose ); extern void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose );
int c, nVars = 3, nNodes = 1, fUseConst = 0, fVerbose = 1; int c, nVars = 3, nNodes = 1, fUseConst = 0, fUseLine = 0, fVerbose = 1;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NMcvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "INfcvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
case 'N': case 'I':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nVars = atoi(argv[globalUtilOptind]); nVars = atoi(argv[globalUtilOptind]);
...@@ -8090,10 +8090,10 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -8090,10 +8090,10 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nVars < 0 ) if ( nVars < 0 )
goto usage; goto usage;
break; break;
case 'M': case 'N':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nNodes = atoi(argv[globalUtilOptind]); nNodes = atoi(argv[globalUtilOptind]);
...@@ -8101,9 +8101,12 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -8101,9 +8101,12 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nNodes < 0 ) if ( nNodes < 0 )
goto usage; goto usage;
break; break;
case 'c': case 'f':
fUseConst ^= 1; fUseConst ^= 1;
break; break;
case 'c':
fUseLine ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
...@@ -8118,15 +8121,16 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -8118,15 +8121,16 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Cannot sythesize MAJ gate with an even number of inputs (%d).\n", nVars ); Abc_Print( -1, "Cannot sythesize MAJ gate with an even number of inputs (%d).\n", nVars );
return 1; return 1;
} }
Maj_ManExactSynthesis( nVars, nNodes, fUseConst, fVerbose ); Maj_ManExactSynthesis( nVars, nNodes, fUseConst, fUseLine, fVerbose );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: majexact [-NM <num>] [-cvh]\n" ); Abc_Print( -2, "usage: majexact [-IN <num>] [-fcvh]\n" );
Abc_Print( -2, "\t exactly synthesizes N-input MAJ using MAJ3 gates\n" ); Abc_Print( -2, "\t exact synthesis of multi-input MAJ using MAJ3 gates\n" );
Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", nVars ); Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-M <num> : the number of MAJ3 nodes [default = %d]\n", nNodes ); Abc_Print( -2, "\t-N <num> : the number of MAJ3 nodes [default = %d]\n", nNodes );
Abc_Print( -2, "\t-c : toggle using constant fanins [default = %s]\n", fUseConst ? "yes" : "no" ); Abc_Print( -2, "\t-f : toggle using constant fanins [default = %s]\n", fUseConst ? "yes" : "no" );
Abc_Print( -2, "\t-c : toggle using cascade topology [default = %s]\n", fUseLine ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t-h : print the command usage\n" );
return 1; return 1;
src/opt/sbd/sbd.c
...@@ -43,14 +43,14 @@ ABC_NAMESPACE_IMPL_START ...@@ -43,14 +43,14 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars ) int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars, int Degree )
{ {
int i, k, Entry = 0, Entry2, Count = 0, Below; int i, k, Entry = 0, Entry2, Count = 0, Below;
int Prev = Vec_IntEntry( vSet, 0 ); int Prev = Vec_IntEntry( vSet, 0 );
Vec_IntForEachEntryStart( vSet, Entry, i, 1 ) Vec_IntForEachEntryStart( vSet, Entry, i, 1 )
{ {
assert( 2*Prev >= Entry ); assert( Degree*Prev >= Entry );
if ( 2*Prev == Entry ) if ( Degree*Prev == Entry )
{ {
Prev = Entry; Prev = Entry;
continue; continue;
...@@ -58,19 +58,24 @@ int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars ) ...@@ -58,19 +58,24 @@ int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
Below = nVars; Below = nVars;
Vec_IntForEachEntryStart( vSet, Entry2, k, i ) Vec_IntForEachEntryStart( vSet, Entry2, k, i )
Below += Entry2; Below += Entry2;
Count += Below * (2*Prev - 1); Count += Below * (Degree*Prev - 1);
Prev = Entry; Prev = Entry;
} }
Count += nVars * 2*Prev; Count += nVars * Degree*Prev;
return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count; return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count;
} }
void Sbd_CountTopos() void Sbd_CountTopos()
{ {
Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays int nInputs = 9;
int nNodes = 10;
int Degree = 3;
int fVerbose = 1;
Hsh_VecMan_t * p = Hsh_VecManStart( 10000 ); // hash table for arrays
Vec_Int_t * vSet = Vec_IntAlloc( 100 ); Vec_Int_t * vSet = Vec_IntAlloc( 100 );
int i, k, e, Start, Stop; int i, k, e, Start, Stop;
printf( "Counting topologies for %d inputs and %d degree-%d nodes.\n", nInputs, nNodes, Degree );
Start = Hsh_VecManAdd( p, vSet ); Start = Hsh_VecManAdd( p, vSet );
for ( i = 1; i < 9; i++ ) for ( i = 1; i <= nNodes; i++ )
{ {
Stop = Hsh_VecSize( p ); Stop = Hsh_VecSize( p );
for ( e = Start; e < Stop; e++ ) for ( e = Start; e < Stop; e++ )
...@@ -81,7 +86,7 @@ void Sbd_CountTopos() ...@@ -81,7 +86,7 @@ void Sbd_CountTopos()
for ( k = 0; k < Vec_IntSize(vSet); k++ ) for ( k = 0; k < Vec_IntSize(vSet); k++ )
{ {
// skip if the number of entries on this level is equal to the number of fanins on the previous level // skip if the number of entries on this level is equal to the number of fanins on the previous level
if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) ) if ( k ? (Vec_IntEntry(vSet, k) == Degree*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
continue; continue;
Vec_IntAddToEntry( vSet, k, 1 ); Vec_IntAddToEntry( vSet, k, 1 );
Hsh_VecManAdd( p, vSet ); Hsh_VecManAdd( p, vSet );
...@@ -90,15 +95,16 @@ void Sbd_CountTopos() ...@@ -90,15 +95,16 @@ void Sbd_CountTopos()
Vec_IntPush( vSet, 1 ); Vec_IntPush( vSet, 1 );
Hsh_VecManAdd( p, vSet ); Hsh_VecManAdd( p, vSet );
} }
printf( "%2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) ); printf( "Nodes = %2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
if ( 0 ) if ( fVerbose )
{ {
for ( e = Stop; e < Hsh_VecSize(p); e++ ) for ( e = Stop; e < Hsh_VecSize(p); e++ )
{ {
Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e ); Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
printf( "Params = %3d. ", Sbd_CountConfigVars(vTemp, 5) ); printf( "Params = %3d. ", Sbd_CountConfigVars(vTemp, nInputs, Degree) );
Vec_IntPrint( vTemp ); Vec_IntPrint( vTemp );
} }
printf( "\n" );
} }
Start = Stop; Start = Stop;
} }
......
src/sat/bmc/bmcMaj.c
...@@ -41,6 +41,7 @@ struct Maj_Man_t_ ...@@ -41,6 +41,7 @@ struct Maj_Man_t_
int nWords; // the truth table size in 64-bit words int nWords; // the truth table size in 64-bit words
int iVar; // the next available SAT variable int iVar; // the next available SAT variable
int fUseConst; // use constant fanins int fUseConst; // use constant fanins
int fUseLine; // use cascade topology
Vec_Wrd_t * vInfo; // Const0 + Const1 + nVars + nNodes + Maj(nVars) Vec_Wrd_t * vInfo; // Const0 + Const1 + nVars + nNodes + Maj(nVars)
int VarMarks[MAJ_NOBJS][3][MAJ_NOBJS]; // variable marks int VarMarks[MAJ_NOBJS][3][MAJ_NOBJS]; // variable marks
int VarVals[MAJ_NOBJS+2]; // values of the first 2 + nVars variables int VarVals[MAJ_NOBJS+2]; // values of the first 2 + nVars variables
...@@ -103,6 +104,13 @@ int Maj_ManMarkup( Maj_Man_t * p ) ...@@ -103,6 +104,13 @@ int Maj_ManMarkup( Maj_Man_t * p )
{ {
for ( k = 0; k < 3; k++ ) for ( k = 0; k < 3; k++ )
{ {
if ( p->fUseLine && k == 0 )
{
j = i-1;
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
for ( j = (p->fUseConst && k == 2) ? 0 : 2; j < i - k; j++ ) for ( j = (p->fUseConst && k == 2) ? 0 : 2; j < i - k; j++ )
{ {
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
...@@ -119,19 +127,20 @@ int Maj_ManMarkup( Maj_Man_t * p ) ...@@ -119,19 +127,20 @@ int Maj_ManMarkup( Maj_Man_t * p )
for ( j = 0; j < p->nObjs; j++ ) for ( j = 0; j < p->nObjs; j++ )
{ {
for ( k = 0; k < 3; k++ ) for ( k = 0; k < 3; k++ )
printf( "%2d ", p->VarMarks[i][k][j] ); printf( "%3d ", p->VarMarks[i][k][j] );
printf( "\n" ); printf( "\n" );
} }
} }
return p->iVar; return p->iVar;
} }
Maj_Man_t * Maj_ManAlloc( int nVars, int nNodes, int fUseConst ) Maj_Man_t * Maj_ManAlloc( int nVars, int nNodes, int fUseConst, int fUseLine )
{ {
Maj_Man_t * p = ABC_CALLOC( Maj_Man_t, 1 ); Maj_Man_t * p = ABC_CALLOC( Maj_Man_t, 1 );
p->nVars = nVars; p->nVars = nVars;
p->nNodes = nNodes; p->nNodes = nNodes;
p->nObjs = 2 + nVars + nNodes; p->nObjs = 2 + nVars + nNodes;
p->fUseConst = fUseConst; p->fUseConst = fUseConst;
p->fUseLine = fUseLine;
p->nWords = Abc_TtWordNum(nVars); p->nWords = Abc_TtWordNum(nVars);
p->vOutLits = Vec_WecStart( p->nObjs ); p->vOutLits = Vec_WecStart( p->nObjs );
p->iVar = Maj_ManMarkup( p ); p->iVar = Maj_ManMarkup( p );
...@@ -207,10 +216,11 @@ void Maj_ManPrintSolution( Maj_Man_t * p ) ...@@ -207,10 +216,11 @@ void Maj_ManPrintSolution( Maj_Man_t * p )
{ {
int i, k, iVar; int i, k, iVar;
printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes ); printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes );
for ( i = p->nVars + 2; i < p->nObjs; i++ ) // for ( i = p->nVars + 2; i < p->nObjs; i++ )
for ( i = p->nObjs - 1; i >= p->nVars + 2; i-- )
{ {
printf( "%02d = MAJ(", i-2 ); printf( "%02d = MAJ(", i-2 );
for ( k = 0; k < 3; k++ ) for ( k = 2; k >= 0; k-- )
{ {
iVar = Maj_ManFindFanin( p, i, k ); iVar = Maj_ManFindFanin( p, i, k );
if ( iVar >= 2 && iVar < p->nVars + 2 ) if ( iVar >= 2 && iVar < p->nVars + 2 )
...@@ -335,11 +345,11 @@ int Maj_ManAddCnf( Maj_Man_t * p, int iMint ) ...@@ -335,11 +345,11 @@ int Maj_ManAddCnf( Maj_Man_t * p, int iMint )
p->iVar += 4*p->nNodes; p->iVar += 4*p->nNodes;
return 1; return 1;
} }
void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose ) void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose )
{ {
int i, iMint = 0; int i, iMint = 0;
abctime clkTotal = Abc_Clock(); abctime clkTotal = Abc_Clock();
Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst ); Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst, fUseLine );
int status = Maj_ManAddCnfStart( p ); int status = Maj_ManAddCnfStart( p );
assert( status ); assert( status );
printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", p->nVars, p->nNodes ); printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", p->nVars, p->nNodes );
...@@ -355,7 +365,7 @@ void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose ) ...@@ -355,7 +365,7 @@ void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose )
Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars ); Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
printf( " Var =%5d ", p->iVar ); printf( " Var =%5d ", p->iVar );
printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) ); printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
printf( "Conf =%8d ", bmcg_sat_solver_conflictnum(p->pSat) ); printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
} }
if ( status == GLUCOSE_UNSAT ) if ( status == GLUCOSE_UNSAT )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment