diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d4ec89b41..835ee509c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -174,6 +174,7 @@ static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAndExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTopoExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOrchestrate ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -994,8 +995,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "faultclasses", Abc_CommandFaultClasses, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "orchestrate", Abc_CommandOrchestrate, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "aigaug", Abc_CommandAIGAugmentation, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "orchestrate", Abc_CommandOrchestrate, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "aigaug", Abc_CommandAIGAugmentation, 1 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_stop", Abc_CommandBmsStop, 0 ); @@ -1005,6 +1006,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "andexact", Abc_CommandAndExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 ); + Cmd_CommandAdd( pAbc, "Exact synthesis", "topoexact", Abc_CommandTopoExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 ); @@ -11387,6 +11389,126 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 ); + Abc_Ntk_t * pNtkRes = NULL; + Abc_Ntk_t * pTopo = NULL; + int nTimeOut = 0; + int nSeed = 0; + char * pFileName = NULL; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "TSvh" ) ) != EOF ) + { + switch ( c ) + { + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSeed < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pNtkCur == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) + { + Abc_Print( -1, "This command expect an AIG as the current network and BLIF file on the command line.\n" ); + return 1; + } + if ( argc == globalUtilOptind + 1 ) + pFileName = argv[globalUtilOptind]; + if ( pFileName == NULL ) + { + Abc_Print( -1, "File name is not given on the command line.\n" ); + return 1; + } + pTopo = Io_Read( pFileName, Io_ReadFileType(pFileName), 1, 0 ); + if ( pTopo == NULL ) + { + Abc_Print( -1, "The topology file is not specified on the command line.\n" ); + return 1; + } + if ( Abc_NtkGetFaninMax(pTopo) > 6 ) + { + Abc_NtkDelete( pTopo ); + Abc_Print( -1, "The topology network has nodes with more than 6 inputs.\n" ); + return 1; + } + if ( Abc_NtkCiNum(pAbc->pNtkCur) != Abc_NtkCiNum(pTopo) ) + { + Abc_NtkDelete( pTopo ); + Abc_Print( -1, "The number of combinational inputs of the networks does not match.\n" ); + return 1; + } + if ( Abc_NtkCoNum(pAbc->pNtkCur) != Abc_NtkCoNum(pTopo) ) + { + Abc_NtkDelete( pTopo ); + Abc_Print( -1, "The number of combinational outputs of the networks does not match.\n" ); + return 1; + } + pTopo = Abc_NtkDupDfs( pNtkRes = pTopo ); + Abc_NtkDelete( pNtkRes ); + pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fVerbose ); + Abc_NtkDelete( pTopo ); + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "Command has failed.\n" ); + return 0; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + Abc_Print( -2, "usage: topoexact [-TS num] \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-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" ); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -49804,9 +49926,9 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp; Vec_Int_t * vPos; - int c, nRegs = 0, iOutNum = -1, nOutRange = 1, iPartNum = -1, nLevelMax = 0, nTimeWindow = 0, fUseAllCis = 0, fExtractAll = 0, fComb = 0, fVerbose = 0; + int c, nRegs = 0, iOutNum = -1, nOutRange = 1, iPartNum = -1, iConeNum = -1, nLevelMax = 0, nTimeWindow = 0, fUseAllCis = 0, fExtractAll = 0, fComb = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ORPLWaecvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ORPLWCaecvh" ) ) != EOF ) { switch ( c ) { @@ -49865,6 +49987,17 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeWindow < 0 ) goto usage; break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + iConeNum = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iConeNum < 1 ) + goto usage; + break; case 'a': fUseAllCis ^= 1; break; @@ -49917,6 +50050,17 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } } + if ( iConeNum > 0 ) + { + if ( iConeNum >= Gia_ManObjNum(pAbc->pGia) || !Gia_ObjIsAnd(Gia_ManObj(pAbc->pGia, iConeNum)) ) + { + Abc_Print( -1, "Abc_CommandAbc9Cone(): Object with Id %d is not a node.\n", iConeNum ); + return 1; + } + pTemp = Gia_ManDupDfsNode( pAbc->pGia, Gia_ManObj(pAbc->pGia, iConeNum) ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + } if ( iPartNum >= 0 ) { Vec_Int_t * vClass; @@ -49957,13 +50101,14 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cone [-ORPLW num] [-aecvh]\n" ); + Abc_Print( -2, "usage: &cone [-ORPLWC num] [-aecvh]\n" ); Abc_Print( -2, "\t extracting multi-output sequential logic cones\n" ); Abc_Print( -2, "\t-O num : the index of first PO to extract [default = %d]\n", iOutNum ); Abc_Print( -2, "\t-R num : (optional) the number of outputs to extract [default = %d]\n", nOutRange ); Abc_Print( -2, "\t-P num : (optional) the partition number to extract [default = %d]\n", iPartNum ); Abc_Print( -2, "\t-L num : (optional) extract cones with higher level [default = %d]\n", nLevelMax ); Abc_Print( -2, "\t-W num : (optional) extract cones falling into this window [default = %d]\n", nTimeWindow ); + Abc_Print( -2, "\t-C num : (optional) extract cone of one node with ID equal to [default = unused]\n" ); Abc_Print( -2, "\t-a : toggle keeping all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" ); Abc_Print( -2, "\t-e : toggle writing all outputs into individual files [default = %s]\n", fExtractAll? "yes": "no" ); Abc_Print( -2, "\t-c : toggle performing cone extraction combinationally [default = %s]\n", fComb? "yes": "no" ); diff --git a/src/base/abci/abcTopo.c b/src/base/abci/abcTopo.c new file mode 100644 index 000000000..802543555 --- /dev/null +++ b/src/base/abci/abcTopo.c @@ -0,0 +1,220 @@ +/**CFile**************************************************************** + + FileName [abcTopo.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Topologically constrained exact synthesis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcTopo.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "base/abc/abc.h" +#include "misc/util/utilTruth.h" +#include "sat/kissat/kissat.h" + +#define KISSAT_UNSAT 20 +#define KISSAT_SAT 10 +#define KISSAT_UNDEC 0 + +static int AbcTopo_KissatTerminate( void * pData ) +{ + abctime * pTimeStop = (abctime *)pData; + return pTimeStop && *pTimeStop && Abc_Clock() > *pTimeStop; +} + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Exact synthesis of the MO function into a fixed-topology network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkTopoDup( Abc_Ntk_t * pTopo, Vec_Wrd_t * vTruths ) +{ + Abc_Ntk_t * pNew = Abc_NtkDup(pTopo); + Abc_Obj_t * pObj; int i; + Abc_NtkForEachNode( pTopo, pObj, i ) { + extern char * Bbl_ManTruthToSop( unsigned * pTruth, int nVars ); + char * pSop = Bbl_ManTruthToSop( (unsigned *)Vec_WrdEntryP(vTruths, i), Abc_ObjFaninNum(pObj) ); + pObj->pData = Abc_SopRegister( (Mem_Flex_t *)pNew->pManFunc, pSop ); + ABC_FREE( pSop ); + } + return pNew; +} +Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, 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_NtkForEachNode( pTopo, pObj, i ) { + assert( Abc_ObjFaninNum(pObj) <= 6 ); + nMints += 1 << Abc_ObjFaninNum(pObj); + nNodeClausesPerMint += 2 * (1 << Abc_ObjFaninNum(pObj)); // two clauses per minterm + } + // derive input/output mapping of the original function, which will be synthesized + Gia_Man_t * pGia = Abc_NtkClpGia( pFunc ); + Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pGia) ); + Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( pGia, vSimsPi, 1 ); + int nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(pGia); + assert( Abc_NtkCiNum(pTopo) == Gia_ManCiNum(pGia) ); + assert( Abc_NtkPoNum(pTopo) == Gia_ManPoNum(pGia) ); + assert( Vec_WrdSize(vSims) == Gia_ManPoNum(pGia) * nWords ); + // map network objects to compact variable IDs (PIs first, then internal nodes) + Vec_Int_t * vObj2Var = Vec_IntStart( Abc_NtkObjNumMax(pTopo) ); + int iMap = 0; + Abc_NtkForEachCi( pTopo, pObj, i ) + Vec_IntWriteEntry( vObj2Var, Abc_ObjId(pObj), iMap++ ); + Abc_NtkForEachNode( pTopo, pObj, i ) + Vec_IntWriteEntry( vObj2Var, Abc_ObjId(pObj), iMap++ ); + assert( iMap == Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo) ); + // create Kissat SAT solver with as many variables as there are minterms + // plus additionally allocate vars to represent values of each node under each input minterm + kissat * pSat = kissat_init(); + int nVarsAlloc = nMints + (1 << Abc_NtkCiNum(pTopo)) * (Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo)); + kissat_reserve( pSat, nVarsAlloc ); + if ( nSeed > 0 ) + kissat_set_option( pSat, "seed", nSeed ); + if ( fVerbose ) + printf( "Running fixed-topology exact synthesis: PI = %d Nodes = %d PO = %d\n", + Abc_NtkCiNum(pTopo), Abc_NtkNodeNum(pTopo), Abc_NtkPoNum(pTopo) ); + // for each minterm, iterate through each PI, each internal node, and each outputs + // 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); + for ( m = 0; m < nTopoMints; m++ ) { + int iVarBase = nMints + m * (Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo)); + // set PI values for this minterm + Abc_NtkForEachCi( pTopo, pObj, k ) { + int fPiVal = Abc_TtGetBit( Vec_WrdArray(vSimsPi) + k * nWords, m ); + int iPiVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pObj) ); + int Lit = Abc_Var2Lit( iPiVar, !fPiVal ); + kissat_add( pSat, Abc_LitIsCompl(Lit) ? -(Abc_Lit2Var(Lit) + 1) : (Abc_Lit2Var(Lit) + 1) ); + kissat_add( pSat, 0 ); + } + // for each internal node + int iMint = 0; + Abc_NtkForEachNode( pTopo, pObj, n ) { + int nFanins = Abc_ObjFaninNum(pObj); + int iNodeMintBase = iMint; + int iNodeVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pObj) ); + // for each configuration of fanin values + for ( k = 0; k < (1 << nFanins); k++ ) { + // add clauses for both polarities of the node output + for ( int v = 0; v < 2; v++ ) { + int pLits[8], nLits = 0; + // add literal for the truth table variable (minterm k of this node) + pLits[nLits++] = Abc_Var2Lit( iNodeMintBase + k, v ); + // add literal for the node output value + pLits[nLits++] = Abc_Var2Lit( iNodeVar, !v ); + // check fanin values match minterm k + Abc_Obj_t * pFanin; + Abc_ObjForEachFanin( pObj, pFanin, f ) { + int iFaninVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pFanin) ); + int fFaninVal = (k >> f) & 1; + pLits[nLits++] = Abc_Var2Lit( iFaninVar, !fFaninVal ); + } + // add clause + for ( i = 0; i < nLits; i++ ) + kissat_add( pSat, Abc_LitIsCompl(pLits[i]) ? -(Abc_Lit2Var(pLits[i]) + 1) : (Abc_Lit2Var(pLits[i]) + 1) ); + kissat_add( pSat, 0 ); + } + } + iMint += 1 << nFanins; + } + assert( iMint == nMints ); + // constrain primary outputs to match the target function + Abc_NtkForEachPo( pTopo, pObj, n ) { + Abc_Obj_t * pDriver = Abc_ObjFanin0(pObj); + int iDriverVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pDriver) ); + // get expected output value from simulation and add unit clause + int fExpected = Abc_TtGetBit( Vec_WrdArray(vSims) + n * nWords, m ); + int Lit = Abc_Var2Lit( iDriverVar, !fExpected ); + kissat_add( pSat, Abc_LitIsCompl(Lit) ? -(Abc_Lit2Var(Lit) + 1) : (Abc_Lit2Var(Lit) + 1) ); + kissat_add( pSat, 0 ); + } + } + if ( fVerbose ) + printf( "Minterm variables = %d. Internal variables = %d. Clauses = %d.\n", nMints, nVarsAlloc - nMints, nClauses ); + + abctime timeStop = 0; + if ( nTimeOut ) + { + timeStop = Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC; + kissat_set_terminate( pSat, &timeStop, AbcTopo_KissatTerminate ); + } + else + kissat_set_terminate( pSat, NULL, NULL ); + int status = kissat_solve( pSat ); + if ( status == KISSAT_SAT ) + { + // if it is satisfiable, collect the satisfying assignment into the array + Vec_Wrd_t * vTruths = Vec_WrdStart( Abc_NtkObjNumMax(pTopo) ); + int iMint = 0; + Abc_NtkForEachNode( pTopo, pObj, i ) { + // iMint shows the first SAT variable of this node + // collect values into Truth + word TruthSmall = 0; + for ( int v = 0; v < (1 << Abc_ObjFaninNum(pObj)); v++ ) + if ( kissat_value( pSat, iMint + v + 1 ) > 0 ) + TruthSmall |= (word)1 << v; + // increment the minterm counter + iMint += 1 << Abc_ObjFaninNum(pObj); + // save the result into the array of truth tables + Vec_WrdWriteEntry( vTruths, i, Abc_Tt6Stretch( TruthSmall, Abc_ObjFaninNum(pObj) ) ); + if ( fVerbose ) { + int nDigits = 1 << (Abc_ObjFaninNum(pObj)-2); + printf( "Node %2d (fanins = %d) 0x%0*lx\n", i, Abc_ObjFaninNum(pObj), nDigits, TruthSmall ); + } + } + assert( iMint == nMints ); + // create network with the corresponding truth tables + pRes = Abc_NtkTopoDup( pTopo, vTruths ); + Vec_WrdFree( vTruths ); + if ( fVerbose ) + printf( "The problem has a solution.\n" ); + } + else if ( status == KISSAT_UNSAT && fVerbose ) + printf( "The problem has no solution.\n" ); + else if ( status == KISSAT_UNDEC && fVerbose ) + printf( "The solver returned unknown.\n" ); + kissat_release( pSat ); + Vec_WrdFree( vSims ); + Vec_WrdFree( vSimsPi ); + Vec_IntFree( vObj2Var ); + Gia_ManStop( pGia ); + if ( fVerbose ) + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + return pRes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 4e4690404..fe063a42a 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -71,6 +71,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcSymm.c \ src/base/abci/abcTim.c \ src/base/abci/abcTiming.c \ + src/base/abci/abcTopo.c \ src/base/abci/abcUnate.c \ src/base/abci/abcUnreach.c \ src/base/abci/abcVerify.c \ diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 93d3ea326..67b31ca7a 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -75,12 +75,14 @@ struct Bmc_EsPar_t_ int Seed; int n1HotAlgo; int fDumpBlif; + int fGenTruths; int fVerbose; int fSilent; char * pTtStr; char * pSymStr; char * pPermStr; char * pGuide; + Vec_Wrd_t* vTruths; }; static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c index 5f291c20a..2ae25c8b5 100644 --- a/src/sat/bmc/bmcMaj8.c +++ b/src/sat/bmc/bmcMaj8.c @@ -389,6 +389,50 @@ static inline int Exa8_ManEval( Exa8_Man_t * p ) SeeAlso [] ***********************************************************************/ +static Vec_Wrd_t * Exa8_ManSaveTruthTables( Exa8_Man_t * p, int fCompl ) +{ + int i, k, nWordsNode, nMintsNode; + assert( p->nLutSize <= 8 ); + nMintsNode = 1 << p->nLutSize; + nWordsNode = (p->nLutSize <= 6) ? 1 : (p->nLutSize == 7 ? 2 : 4); + Vec_Wrd_t * vTruths = Vec_WrdStart( p->nObjs * nWordsNode ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + word Truth[4] = {0, 0, 0, 0}; + int iVarStart = 1 + p->LutMask*(i - p->nVars); + for ( k = 0; k < p->LutMask; k++ ) + { + if ( Exa8_KissatVarValue( p, iVarStart + k ) ) + { + int bit = k + 1; // minterm index (minterm 0 is fixed to 0) + int w = bit >> 6; + int b = bit & 63; + Truth[w] |= ((word)1 << b); + } + } + // complement the output fully if needed (including minterm 0) + if ( i == p->nObjs - 1 && fCompl ) + { + for ( int w = 0; w < nWordsNode; w++ ) + { + word Mask; + int rem = nMintsNode - w * 64; + if ( rem <= 0 ) + Mask = 0; + else if ( rem >= 64 ) + Mask = ~(word)0; + else + Mask = (((word)1) << rem) - 1; + Truth[w] = (~Truth[w]) & Mask; + } + } + if ( p->nLutSize < 6 ) + Truth[0] = Abc_Tt6Stretch( Truth[0], p->nLutSize ); + for ( int w = 0; w < nWordsNode; w++ ) + Vec_WrdWriteEntry( vTruths, i * nWordsNode + w, Truth[w] ); + } + return vTruths; +} static void Exa8_ManPrintSolution( Exa8_Man_t * p, int fCompl ) { int i, k, iVar; @@ -692,7 +736,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr ); ABC_FREE( pFun ); } - if ( pPars->pTtStr ) + if ( pPars->pTtStr && pPars->nVars <= 7 ) Abc_TtReadHex( pTruth, pPars->pTtStr ); else assert( 0 ); if ( pPars->fUseIncr && !pPars->fSilent ) @@ -741,6 +785,11 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars ) printf( "\".\n" ); if ( pPars->fDumpBlif ) Exa8_ManDumpBlif( p, fCompl ); + if ( p->pPars->fGenTruths ) { + if ( p->pPars->vTruths ) + Vec_WrdFreeP( &p->pPars->vTruths ); + p->pPars->vTruths = Exa8_ManSaveTruthTables( p, fCompl ); + } Res = 1; } else if ( status == KISSAT_UNSAT ) @@ -845,6 +894,46 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) return Result; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars ) +{ + Bmc_EsPar_t Pars, * pPars = &Pars; + Bmc_EsParSetDefault( pPars ); + pPars->fKissat = 1; + pPars->fLutCascade = 1; + pPars->fMinNodes = 1; + pPars->fUsePerm = 1; + pPars->fGenTruths = 1; + pPars->nLutSize = 6; + int v, o, nOuts = Abc_Base2Log(nVars+1); + Vec_Ptr_t * vRes = Vec_PtrAlloc( nOuts ); + for ( o = 0; o < nOuts; o++ ) { + char pBuffer[100]; + for ( v = 0; v <= nVars; v++ ) + pBuffer[v] = '0' + ((v >> o) & 1); + pBuffer[nVars+1] = '\0'; + pPars->pSymStr = pBuffer; + int status = Exa8_ManExactSynthesis( pPars ); + if ( status != 1 ) { + printf( "Synthesis failed for output %d.\n", o ); + break; + } + Vec_PtrPush( vRes, pPars->vTruths ); + pPars->vTruths = NULL; + } + return vRes; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////