From c272188946b1142c7853c0820c2f034bf8edf86a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 1 Oct 2017 19:49:28 +0300 Subject: Exact synthesis of majority gates. --- src/base/abci/abc.c | 32 ++++++++++++++++++-------------- src/opt/sbd/sbd.c | 28 +++++++++++++++++----------- src/sat/bmc/bmcMaj.c | 24 +++++++++++++++++------- 3 files changed, 52 insertions(+), 32 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5caf8145..ad3673d0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8072,17 +8072,17 @@ usage: ***********************************************************************/ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose ); - int c, nVars = 3, nNodes = 1, fUseConst = 0, fVerbose = 1; + extern void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose ); + int c, nVars = 3, nNodes = 1, fUseConst = 0, fUseLine = 0, fVerbose = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NMcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INfcvh" ) ) != EOF ) { switch ( c ) { - case 'N': + case 'I': 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; } nVars = atoi(argv[globalUtilOptind]); @@ -8090,10 +8090,10 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nVars < 0 ) goto usage; break; - case 'M': + case 'N': 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; } nNodes = atoi(argv[globalUtilOptind]); @@ -8101,9 +8101,12 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nNodes < 0 ) goto usage; break; - case 'c': + case 'f': fUseConst ^= 1; break; + case 'c': + fUseLine ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -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 ); return 1; } - Maj_ManExactSynthesis( nVars, nNodes, fUseConst, fVerbose ); + Maj_ManExactSynthesis( nVars, nNodes, fUseConst, fUseLine, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: majexact [-NM ] [-cvh]\n" ); - Abc_Print( -2, "\t exactly synthesizes N-input MAJ using MAJ3 gates\n" ); - Abc_Print( -2, "\t-N : the number of input variables [default = %d]\n", nVars ); - Abc_Print( -2, "\t-M : 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, "usage: majexact [-IN ] [-fcvh]\n" ); + Abc_Print( -2, "\t exact synthesis of multi-input MAJ using MAJ3 gates\n" ); + Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", nVars ); + Abc_Print( -2, "\t-N : the number of MAJ3 nodes [default = %d]\n", nNodes ); + 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-h : print the command usage\n" ); return 1; diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c index 5c5b1f2b..75fc8750 100644 --- a/src/opt/sbd/sbd.c +++ b/src/opt/sbd/sbd.c @@ -43,14 +43,14 @@ ABC_NAMESPACE_IMPL_START 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 Prev = Vec_IntEntry( vSet, 0 ); Vec_IntForEachEntryStart( vSet, Entry, i, 1 ) { - assert( 2*Prev >= Entry ); - if ( 2*Prev == Entry ) + assert( Degree*Prev >= Entry ); + if ( Degree*Prev == Entry ) { Prev = Entry; continue; @@ -58,19 +58,24 @@ int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars ) Below = nVars; Vec_IntForEachEntryStart( vSet, Entry2, k, i ) Below += Entry2; - Count += Below * (2*Prev - 1); + Count += Below * (Degree*Prev - 1); Prev = Entry; } - Count += nVars * 2*Prev; + Count += nVars * Degree*Prev; return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count; } 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 ); 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 ); - for ( i = 1; i < 9; i++ ) + for ( i = 1; i <= nNodes; i++ ) { Stop = Hsh_VecSize( p ); for ( e = Start; e < Stop; e++ ) @@ -81,7 +86,7 @@ void Sbd_CountTopos() 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 - 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; Vec_IntAddToEntry( vSet, k, 1 ); Hsh_VecManAdd( p, vSet ); @@ -90,15 +95,16 @@ void Sbd_CountTopos() Vec_IntPush( vSet, 1 ); Hsh_VecManAdd( p, vSet ); } - printf( "%2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) ); - if ( 0 ) + printf( "Nodes = %2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) ); + if ( fVerbose ) { for ( e = Stop; e < Hsh_VecSize(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 ); } + printf( "\n" ); } Start = Stop; } diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 749be285..31460b0e 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -41,6 +41,7 @@ struct Maj_Man_t_ int nWords; // the truth table size in 64-bit words int iVar; // the next available SAT variable int fUseConst; // use constant fanins + int fUseLine; // use cascade topology Vec_Wrd_t * vInfo; // Const0 + Const1 + nVars + nNodes + Maj(nVars) int VarMarks[MAJ_NOBJS][3][MAJ_NOBJS]; // variable marks int VarVals[MAJ_NOBJS+2]; // values of the first 2 + nVars variables @@ -103,6 +104,13 @@ int Maj_ManMarkup( Maj_Man_t * p ) { 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++ ) { Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) ); @@ -119,19 +127,20 @@ int Maj_ManMarkup( Maj_Man_t * p ) for ( j = 0; j < p->nObjs; j++ ) { for ( k = 0; k < 3; k++ ) - printf( "%2d ", p->VarMarks[i][k][j] ); + printf( "%3d ", p->VarMarks[i][k][j] ); printf( "\n" ); } } 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 ); p->nVars = nVars; p->nNodes = nNodes; p->nObjs = 2 + nVars + nNodes; p->fUseConst = fUseConst; + p->fUseLine = fUseLine; p->nWords = Abc_TtWordNum(nVars); p->vOutLits = Vec_WecStart( p->nObjs ); p->iVar = Maj_ManMarkup( p ); @@ -207,10 +216,11 @@ void Maj_ManPrintSolution( Maj_Man_t * p ) { int i, k, iVar; 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 ); - for ( k = 0; k < 3; k++ ) + for ( k = 2; k >= 0; k-- ) { iVar = Maj_ManFindFanin( p, i, k ); if ( iVar >= 2 && iVar < p->nVars + 2 ) @@ -335,11 +345,11 @@ int Maj_ManAddCnf( Maj_Man_t * p, int iMint ) p->iVar += 4*p->nNodes; 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; 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 ); assert( status ); 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 ) 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) ); + printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } if ( status == GLUCOSE_UNSAT ) -- cgit v1.2.3