From a8a58c63ba2046a7f1c4d23d915d939465debdaa Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 14 Dec 2025 22:54:25 -0800 Subject: [PATCH] Updateing "topoexact". --- src/base/abci/abc.c | 14 +++++++++----- src/base/abci/abcTopo.c | 38 +++++++++++++++++++++++++++++++++++--- 2 files changed, 44 insertions(+), 8 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ba77e7ad7..2a96f7213 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -11406,15 +11406,15 @@ usage: ***********************************************************************/ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fAndGates, int fVerbose ); Abc_Ntk_t * pNtkRes = NULL; Abc_Ntk_t * pTopo = NULL; int nTimeOut = 0; int nSeed = 0; char * pFileName = NULL; - int c, fVerbose = 0; + int c, fAndGates = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TSvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TSavh" ) ) != EOF ) { switch ( c ) { @@ -11440,6 +11440,9 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nSeed < 0 ) goto usage; break; + case 'a': + fAndGates ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -11492,7 +11495,7 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } pTopo = Abc_NtkDupDfs( pNtkRes = pTopo ); Abc_NtkDelete( pNtkRes ); - pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fVerbose ); + pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fAndGates, fVerbose ); Abc_NtkDelete( pTopo ); if ( pNtkRes == NULL ) { @@ -11503,10 +11506,11 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: topoexact [-TS num] \n" ); + Abc_Print( -2, "usage: topoexact [-TS num] [-avh] \n" ); Abc_Print( -2, "\t exact synthesis solution for the fixed topology\n" ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-S : the random seed to randomize the SAT solver [default = %d]\n", nSeed ); + Abc_Print( -2, "\t-a : toggle using only and-gates (not xor-gates) [default = %s]\n", fAndGates ? "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 : BLIF file name with the topology\n" ); diff --git a/src/base/abci/abcTopo.c b/src/base/abci/abcTopo.c index aa5bcf75e..ded7c069f 100644 --- a/src/base/abci/abcTopo.c +++ b/src/base/abci/abcTopo.c @@ -65,17 +65,18 @@ Abc_Ntk_t * Abc_NtkTopoDup( Abc_Ntk_t * pTopo, Vec_Wrd_t * vTruths ) } return pNew; } -Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fVerbose ) +Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fAndGates, int fVerbose ) { Abc_Ntk_t * pRes = NULL; abctime clkTotal = Abc_Clock(); assert( Abc_NtkIsSopLogic(pTopo) ); // count how many variables we need to encode minterms of each node - Abc_Obj_t * pObj; int i, nMints = 0, nNodeClausesPerMint = 0; + Abc_Obj_t * pObj; int i, nMints = 0, nNodeClausesPerMint = 0, nTwoFaninNodes = 0; Abc_NtkForEachNode( pTopo, pObj, i ) { assert( Abc_ObjFaninNum(pObj) <= 6 ); nMints += 1 << Abc_ObjFaninNum(pObj); nNodeClausesPerMint += 2 * (1 << Abc_ObjFaninNum(pObj)); // two clauses per minterm + nTwoFaninNodes += (Abc_ObjFaninNum(pObj) == 2); } // derive input/output mapping of the original function, which will be synthesized Gia_Man_t * pGia = Abc_NtkClpGia( pFunc ); @@ -107,7 +108,38 @@ Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut // and add constraints that tell us that the value of the node's output agrees with the values of its fanins // while the value of the primary outputs is realized correctly by those internal nodes that drive the outputs int m, n, k, f, nTopoMints = 1 << Abc_NtkCiNum(pTopo); - int nClauses = nTopoMints * (Abc_NtkCiNum(pTopo) + Abc_NtkPoNum(pTopo) + nNodeClausesPerMint); + int nClauses = nTopoMints * (Abc_NtkCiNum(pTopo) + Abc_NtkPoNum(pTopo) + nNodeClausesPerMint) + + (fAndGates ? 2 * nTwoFaninNodes : 0); + if ( fAndGates && nTwoFaninNodes ) + { + // block XOR/XNOR truth tables for two-input nodes + int iMint = 0; + Abc_NtkForEachNode( pTopo, pObj, i ) + { + int nFanins = Abc_ObjFaninNum(pObj); + if ( nFanins == 2 ) + { + int pLits[4], j; + // forbid 0110 + pLits[0] = Abc_Var2Lit( iMint + 0, 0 ); + pLits[1] = Abc_Var2Lit( iMint + 1, 1 ); + pLits[2] = Abc_Var2Lit( iMint + 2, 1 ); + pLits[3] = Abc_Var2Lit( iMint + 3, 0 ); + for ( j = 0; j < 4; j++ ) + kissat_add( pSat, Abc_LitIsCompl(pLits[j]) ? -(Abc_Lit2Var(pLits[j]) + 1) : (Abc_Lit2Var(pLits[j]) + 1) ); + kissat_add( pSat, 0 ); + // forbid 1001 + pLits[0] = Abc_Var2Lit( iMint + 0, 1 ); + pLits[1] = Abc_Var2Lit( iMint + 1, 0 ); + pLits[2] = Abc_Var2Lit( iMint + 2, 0 ); + pLits[3] = Abc_Var2Lit( iMint + 3, 1 ); + for ( j = 0; j < 4; j++ ) + kissat_add( pSat, Abc_LitIsCompl(pLits[j]) ? -(Abc_Lit2Var(pLits[j]) + 1) : (Abc_Lit2Var(pLits[j]) + 1) ); + kissat_add( pSat, 0 ); + } + iMint += 1 << nFanins; + } + } for ( m = 0; m < nTopoMints; m++ ) { int iVarBase = nMints + m * (Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo)); // set PI values for this minterm