From e58a28b73baba0023874144e492df349955a8d6d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 5 Dec 2025 20:44:46 -0800 Subject: [PATCH 1/4] Command "topoexact". --- src/base/abci/abc.c | 155 ++++++++++++++++++++++++++- src/base/abci/abcTopo.c | 220 ++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + src/sat/bmc/bmc.h | 2 + src/sat/bmc/bmcMaj8.c | 91 +++++++++++++++- 5 files changed, 463 insertions(+), 6 deletions(-) create mode 100644 src/base/abci/abcTopo.c 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 /// //////////////////////////////////////////////////////////////////////// From eaa204829cddeb6d6db4a6679aaf4dff8deefd40 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 5 Dec 2025 20:50:53 -0800 Subject: [PATCH 2/4] Compiler warning. --- src/base/abci/abcTopo.c | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/base/abci/abcTopo.c b/src/base/abci/abcTopo.c index 802543555..aa5bcf75e 100644 --- a/src/base/abci/abcTopo.c +++ b/src/base/abci/abcTopo.c @@ -26,11 +26,7 @@ #define KISSAT_SAT 10 #define KISSAT_UNDEC 0 -static int AbcTopo_KissatTerminate( void * pData ) -{ - abctime * pTimeStop = (abctime *)pData; - return pTimeStop && *pTimeStop && Abc_Clock() > *pTimeStop; -} +ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -40,6 +36,12 @@ static int AbcTopo_KissatTerminate( void * pData ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +static int AbcTopo_KissatTerminate( void * pData ) +{ + abctime * pTimeStop = (abctime *)pData; + return pTimeStop && *pTimeStop && Abc_Clock() > *pTimeStop; +} + /**Function************************************************************* Synopsis [Exact synthesis of the MO function into a fixed-topology network.] From 33001946f0e55ae4b0f93d6f2d3cd63214f17010 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 5 Dec 2025 21:14:01 -0800 Subject: [PATCH 3/4] Accidental bug. --- src/sat/bmc/bmcMaj8.c | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c index 2ae25c8b5..465453d81 100644 --- a/src/sat/bmc/bmcMaj8.c +++ b/src/sat/bmc/bmcMaj8.c @@ -733,10 +733,10 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars ) word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars ); pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 ); Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars ); - if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr ); + if ( !pPars->fSilent && pPars->nVars <= 7 ) printf( "Generated symmetric function: %s\n", pPars->pTtStr ); ABC_FREE( pFun ); } - if ( pPars->pTtStr && pPars->nVars <= 7 ) + if ( pPars->pTtStr ) Abc_TtReadHex( pTruth, pPars->pTtStr ); else assert( 0 ); if ( pPars->fUseIncr && !pPars->fSilent ) @@ -822,7 +822,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) int nNodeMax = pPars->nNodes, Result = 0; int fGenPerm = pPars->pPermStr == NULL; for ( int n = nNodeMin; n <= nNodeMax; n++ ) { - printf( "\nTrying M = %d:\n", n ); + if ( !pPars->fSilent ) printf( "\nTrying M = %d:\n", n ); pPars->nNodes = n; if ( !pPars->fUsePerm && fGenPerm ) { Vec_Str_t * vStr = Vec_StrAlloc( 100 ); @@ -905,7 +905,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars ) +Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int fVerbose ) { Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); @@ -914,6 +914,7 @@ Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars ) pPars->fMinNodes = 1; pPars->fUsePerm = 1; pPars->fGenTruths = 1; + pPars->fSilent = !fVerbose; pPars->nLutSize = 6; int v, o, nOuts = Abc_Base2Log(nVars+1); Vec_Ptr_t * vRes = Vec_PtrAlloc( nOuts ); From e67af0ad9e6d3c965a8a933f1d850349e7f2ca31 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 7 Dec 2025 17:51:22 -0800 Subject: [PATCH 4/4] Command "netexact". --- src/base/abci/abc.c | 156 ++++- src/misc/util/module.make | 1 + src/misc/util/utilNet.c | 1243 +++++++++++++++++++++++++++++++++++++ 3 files changed, 1399 insertions(+), 1 deletion(-) create mode 100755 src/misc/util/utilNet.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 835ee509c..67685e00a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -174,7 +174,8 @@ 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_CommandTopoExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandNetExact ( 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 ); @@ -1007,6 +1008,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) 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", "netexact", Abc_CommandNetExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 ); Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 ); @@ -11509,6 +11511,158 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandNetExact( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Tn_ReadHexTruth( char * pInput, word * pTruth ); + extern void Tn_SolveProblem( int nIns, int nOuts, word * pOuts, char * pTypes, int nEdgeLimit, int nLevelLimit, int nSolsMax, int Seed, int TimeOut, int fVerbose ); + int c, nIns = 0, nOuts = 0, nEdgeLimit = 0, nLevelLimit = 0, nSolsMax = 1, Seed = 0, TimeOut = 0, fVerbose = 0; + char * pTypes = NULL; + word Truths[16] = {0}; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CELNSTVvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pTypes = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Seed < 0 ) + goto usage; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" ); + goto usage; + } + nEdgeLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nEdgeLimit < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nLevelLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevelLimit < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nSolsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSolsMax < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + TimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOut < 0 ) + goto usage; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" ); + goto usage; + } + fVerbose = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( fVerbose < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + for ( c = globalUtilOptind; c < argc; c++ ) { + if ( Abc_TtIsHexDigit(argv[c][0]) == -1 ) { + Abc_Print( -1, "Cannot read truth table \"%s\".\n", argv[c] ); + goto usage; + } + int nVarsOut = Tn_ReadHexTruth( argv[c], Truths + nOuts++ ); + if ( nIns == 0 ) + nIns = nVarsOut; + else if ( nIns != nVarsOut ) { + Abc_Print( -1, "The support size of output functions is not the same.\n" ); + goto usage; + } + } + + printf( "Finished reading %d output%s\n\n", nOuts, nOuts == 1 ? "" : "s" ); + Tn_SolveProblem( nIns, nOuts, Truths, pTypes, nEdgeLimit, nLevelLimit, nSolsMax, Seed, TimeOut, fVerbose ); + return 0; + +usage: + + Abc_Print( -2, "usage: netexact -C [-ELNSTV ] ... \n" ); + Abc_Print( -2, " this program synthesizes networks for multi-output functions\n" ); + Abc_Print( -2, "\n" ); + Abc_Print( -2, " -C : the configuration string (no default)\n" ); + Abc_Print( -2, " -E : the max number of edges (default = no limit)\n" ); + Abc_Print( -2, " -L : the max number of levels (default = no limit)\n" ); + Abc_Print( -2, " -N : the max number of solutions (default = 1)\n" ); + Abc_Print( -2, " -S : the random seed (default = 0)\n" ); + Abc_Print( -2, " -T : the timeout in seconds (default = no timeout)\n" ); + Abc_Print( -2, " -V : the verbosiness levels (default = %d)\n", fVerbose ); + Abc_Print( -2, " : the truth table of the first output in the hexadecimal notation\n" ); + Abc_Print( -2, " : the truth table of the last output in the hexadecimal notation\n" ); + Abc_Print( -2, " the truth tables are assumed to depend on the same variables\n" ); + Abc_Print( -2, " the strings should contain 2^(-2) hexadecimal digits\n" ); + Abc_Print( -2, "\n" ); + Abc_Print( -2, " Example 1: Synthesizing 3-node 2-edge 2-input and-gate:\n" ); + Abc_Print( -2, " %s -C *11** -E 2 8\n", argv[0] ); + Abc_Print( -2, " Example 2: Synthesizing 4-node 5-edge 3-input majority gate:\n" ); + Abc_Print( -2, " %s -C *111*** -E 5 E8\n", argv[0] ); + Abc_Print( -2, " Example 3: Synthesizing 10-edge 3-input 2-output full-adder:\n" ); + Abc_Print( -2, " %s -C *222****** -E 10 E8 96\n", argv[0] ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/misc/util/module.make b/src/misc/util/module.make index 205e2a734..e77877881 100644 --- a/src/misc/util/module.make +++ b/src/misc/util/module.make @@ -9,6 +9,7 @@ SRC += src/misc/util/utilBridge.c \ src/misc/util/utilMiniver.c \ src/misc/util/utilMulSim.c \ src/misc/util/utilNam.c \ + src/misc/util/utilNet.c \ src/misc/util/utilPrefix.cpp \ src/misc/util/utilPth.c \ src/misc/util/utilSignal.c \ diff --git a/src/misc/util/utilNet.c b/src/misc/util/utilNet.c new file mode 100755 index 000000000..e51a02531 --- /dev/null +++ b/src/misc/util/utilNet.c @@ -0,0 +1,1243 @@ +/**CFile**************************************************************** + + FileName [utilNet.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network synthesis.] + + Synopsis [Network synthesis.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: utilNet.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include +#include +#include +#include +#include +#include + +#include "abc_global.h" + +ABC_NAMESPACE_IMPL_START + +// the max number of nodes +#define MSIZE 15 + +/************************************************************* + literal manipulation, etc +**************************************************************/ + + // operations on variables and literals +static inline int tn_v2l( int Var, int c ) { assert(Var >= 0 && !(c >> 1)); return Var + Var + c; } +static inline int tn_l2v( int Lit ) { assert(Lit >= 0); return Lit >> 1; } +static inline int tn_l2c( int Lit ) { assert(Lit >= 0); return Lit & 1; } +static inline int tn_lnot( int Lit ) { assert(Lit >= 0); return Lit ^ 1; } +static inline int tn_lnotc( int Lit, int c ) { assert(Lit >= 0); return Lit ^ (int)(c > 0); } +static inline int tn_lreg( int Lit ) { assert(Lit >= 0); return Lit & ~01; } + +// min/max/abs +static inline int tn_abs( int a ) { return a < 0 ? -a : a; } +static inline int tn_max( int a, int b ) { return a > b ? a : b; } +static inline int tn_min( int a, int b ) { return a < b ? a : b; } + +// swapping two variables +#define TN_SWAP(Type, a, b) { Type t = a; a = b; b = t; } + +/************************************************************* + Vector of 32-bit integers +**************************************************************/ + +typedef struct tn_vi_ { + int size; + int cap; + int* ptr; +} tn_vi; + +// iterator through the entries in the vector +#define tn_vi_for_each_entry( v, entry, i ) \ + for (i = 0; (i < (v)->size) && (((entry) = tn_vi_read((v), i)), 1); i++) +#define tn_vi_for_each_set( v, size, i ) \ + for (i = 0; (i < (v)->size) && (((size) = tn_vi_read((v), i++)), 1); i += size) + +static inline void tn_vi_start (tn_vi* v, int cap) { v->size = 0; v->cap = cap; v->ptr = (int*)malloc( sizeof(int)*v->cap); } +static inline void tn_vi_stop (tn_vi* v) { if ( v->ptr ) free(v->ptr); } +static inline tn_vi* tn_vi_alloc (int cap) { tn_vi* v = (tn_vi *)malloc(sizeof(tn_vi)); tn_vi_start(v, cap); return v; } +static inline void tn_vi_free (tn_vi* v) { if ( v->ptr ) free(v->ptr); free(v); } +static inline int* tn_vi_array (tn_vi* v) { return v->ptr; } +static inline int tn_vi_read (tn_vi* v, int k) { assert(k < v->size); return v->ptr[k]; } +static inline void tn_vi_write (tn_vi* v, int k, int e) { assert(k < v->size); v->ptr[k] = e; } +static inline int tn_vi_size (tn_vi* v) { return v->size; } +static inline void tn_vi_resize (tn_vi* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !! +static inline int tn_vi_pop (tn_vi* v) { assert(v->size > 0); return v->ptr[--v->size]; } +static inline void tn_vi_grow (tn_vi* v) +{ + if (v->size < v->cap) + return; + int newcap = (v->cap < 4) ? 8 : (v->cap / 2) * 3; + v->ptr = (int*)realloc( v->ptr, sizeof(int)*newcap ); + if ( v->ptr == NULL ) + { + printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n", 4.0 * v->cap / (1<<20), 4.0 * newcap / (1<<20) ); + fflush( stdout ); + } + v->cap = newcap; +} +static inline void tn_vi_push (tn_vi* v, int e) { tn_vi_grow(v); v->ptr[v->size++] = e; } +static inline void tn_vi_fill (tn_vi* v, int n, int fill) { int i; tn_vi_resize(v, 0); for (i = 0; i < n; i++) tn_vi_push(v, fill); } +static inline int tn_vi_remove(tn_vi* v, int e) +{ + int j; + for ( j = 0; j < v->size; j++ ) + if ( v->ptr[j] == e ) + break; + if ( j == v->size ) + return 0; + for ( ; j < v->size-1; j++ ) + v->ptr[j] = v->ptr[j+1]; + tn_vi_resize( v, v->size-1 ); + return 1; +} +static inline tn_vi * tn_vi_dup(tn_vi* v) { + tn_vi * p = tn_vi_alloc(v->size); + p->size = v->size; + memmove(p->ptr, v->ptr, sizeof(int)*p->size); + return p; +} +static inline void tn_vi_print(tn_vi* v) { + printf( "Array with %d entries:", v->size ); int i, entry; + tn_vi_for_each_entry( v, entry, i ) + printf( " %d", entry ); + printf( "\n" ); +} +static inline void tn_vi_print_sets(tn_vi* v) { + int i, k, size, count = 0; + tn_vi_for_each_set( v, size, i ) + count++; + printf( "Array with %d sets:\n", count ); + count = 0; + tn_vi_for_each_set( v, size, i ) { + printf( "Set %3d : ", count ); + printf( "Size %3d :", size ); + for ( k = 0; k < size; k++ ) + printf( " %d", tn_vi_read(v, i+k) ); + printf( "\n" ); + count++; + } +} + +/************************************************************* + counting wall time +**************************************************************/ + +static inline iword Tn_Clock() +{ +#if defined(__APPLE__) && defined(__MACH__) + #define APPLE_MACH (__APPLE__ & __MACH__) +#else + #define APPLE_MACH 0 +#endif +#if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__) + struct timespec ts; + if ( clock_gettime(CLOCK_MONOTONIC, &ts) < 0 ) + return (iword)-1; + iword res = ((iword) ts.tv_sec) * CLOCKS_PER_SEC; + res += (((iword) ts.tv_nsec) * CLOCKS_PER_SEC) / 1000000000; + return res; +#else + return (iword) clock(); +#endif +} +static inline void Tn_PrintTime( const char * pStr, iword time ) +{ + printf( "%s = %9.2f sec\n", pStr, 1.0*((double)(time))/((double)CLOCKS_PER_SEC)); +} +static inline int Tn_Base2Log( unsigned n ) +{ + int r; if ( n < 2 ) return (int)n; for ( r = 0, n--; n; n >>= 1, r++ ) {}; return r; +} + +/************************************************************* + Permutation generation +**************************************************************/ + +// generate next permutation in lexicographic order +static void Tn_GetNextPerm(int *currPerm, int nVars) +{ + int i = nVars - 1; + while (i >= 0 && currPerm[i - 1] >= currPerm[i]) + i--; + if (i >= 0) + { + int j = nVars; + while (j > i && currPerm[j - 1] <= currPerm[i - 1]) + j--; + TN_SWAP(int, currPerm[i - 1], currPerm[j - 1]) + i++; + j = nVars; + while (i < j) + { + TN_SWAP(int, currPerm[i - 1], currPerm[j - 1]) + i++; + j--; + } + } +} +static int Tn_Factorial(int nVars) +{ + int i, Res = 1; + for ( i = 1; i <= nVars; i++ ) + Res *= i; + return Res; +} + +// permutation testing procedure +void Tn_PermTest() +{ + int i, k, nVars = 5, currPerm[MSIZE] = {0}; + for ( i = 0; i < nVars; i++ ) + currPerm[i] = i; + int fact = Tn_Factorial( nVars ); + for ( i = 0; i < fact; i++ ) + { + printf( "%3d :", i ); + for ( k = 0; k < nVars; k++ ) + printf( " %d", currPerm[k] ); + printf( "\n" ); + Tn_GetNextPerm( currPerm, nVars ); + } +} + +/************************************************************* + cut/path generation +**************************************************************/ + +// pos cut vars imply the nodes are connected +static inline tn_vi * Tn_CutGen( int n, int nins ) +{ + tn_vi * v = tn_vi_alloc( 1000 ); + int i, j, m, nMiddle = 0, Middle[MSIZE] = {0}; + assert( n <= MSIZE ); + for ( i = 1+nins; i < n-1; i++ ) + Middle[nMiddle++] = i; + assert( nMiddle == n - nins - 2 ); + for ( m = 0; m < (1<> i)&1][nPart[(m >> i)&1]++] = Middle[i]; + Part[1][nPart[1]++] = n-1; + tn_vi_push( v, 2*nPart[0]*nPart[1] ); + for ( i = 0; i < nPart[0]; i++ ) + for ( j = 0; j < nPart[1]; j++ ) { + tn_vi_push( v, Part[0][i] ); + tn_vi_push( v, Part[1][j] ); + } + } + //printf( "Generating cuts for %d nodes and %d inputs:\n", n, nins ); + //tn_vi_print_sets( v ); + return v; +} +// neg path vars imply the nodes are disconnected +static inline tn_vi * Tn_PathGen( int n, int nins ) +{ + tn_vi * v = tn_vi_alloc( 1000 ); + assert( nins < n-2 ); + tn_vi_push( v, 2 ); + tn_vi_push( v, 0 ); + tn_vi_push( v, n-1 ); + for ( int i = 1; i <= n-2-nins; i++ ) { + int nfact = Tn_Factorial(i); + int m, nmints = 1 << (n-2-nins); + for ( m = 0; m < nmints; m++ ) { + int o, nones = 0; + for ( o = 0; o < n-2-nins; o++ ) + nones += (m >> o) & 1; + if ( nones != i ) + continue; + // collect variables + int j, nvars = 0, varMap[MSIZE]; + for ( j = 0; j < n-2-nins; j++ ) + if ( (m >> j) & 1 ) + varMap[nvars++] = 1+nins+j; + assert( nvars == i ); + // generate permutations + int p, currPerm[MSIZE]; + for ( j = 0; j < i; j++ ) + currPerm[j] = j; + for ( p = 0; p < nfact; p++ ) { + tn_vi_push( v, i+2 ); + tn_vi_push( v, 0 ); + for ( j = 0; j < i; j++ ) + tn_vi_push( v, varMap[currPerm[j]] ); + tn_vi_push( v, n-1 ); + Tn_GetNextPerm( currPerm, i ); + } + } + } + //printf( "Generating paths for %d nodes and %d inputs:\n", n, nins ); + //tn_vi_print_sets( v ); + return v; +} +static inline void Tn_SetSwap( tn_vi * p, int Obj1, int Obj2 ) +{ + int i, n, size, * pArray = tn_vi_array(p); + tn_vi_for_each_set( p, size, i ) + for ( n = 0; n < size; n++ ) + if ( pArray[i+n] == Obj1 ) + pArray[i+n] = Obj2; + else if ( pArray[i+n] == Obj2 ) + pArray[i+n] = Obj1; +} + + +/************************************************************* + generating SAT instance +**************************************************************/ + +typedef struct tn_gr_ { + int nIns; // primary inputs + int nOuts; // primary outputs + int nNodes; // all objects (const 1, nIns, internal nodes, nOuts) + int nNodes2; // the square of the above + int nMints; // the number of input minterms + int nEdgeLimit; // maximum transistor count + int nLevelLimit; // maximum transistor depth + int fVerbose; // user flag + char * pTypes; // control type for each node (none, neg, pos, both) + word pOuts[MSIZE]; // truth tables for each output + tn_vi * pVecs[6]; // constraints for each output + FILE * pFile; // file for CNF writing + int nCnfVars; // total number of variables + int nCnfClas; // total number of clauses + int nCnfVars2; // total number of variables + int nCnfClas2; // total number of clauses + tn_vi * vTemp[2]; // temporary vector + tn_vi * vCnf; // collected clauses + tn_vi * vSol; // assignment derived by the solver +} tn_gr; + +/************************************************************* + variable mapping +**************************************************************/ + +static inline int Tn_MapVar( tn_gr * p, int i, int j, int Shift ) +{ + assert( i >= 0 && i < p->nNodes ); + assert( j >= 0 && j < p->nNodes ); + return Shift * p->nNodes2 + i * p->nNodes + j; +} +static inline int Tn_CtrlVar( tn_gr * p, int i, int j, int iVar, int Inv ) +{ + assert( i != j ); + assert( iVar >= 0 && iVar < p->nIns ); + assert( Inv == 0 || Inv == 1 ); + if ( Inv ) + return Tn_MapVar( p, tn_max(i, j), tn_min(i, j), iVar ); + else + return Tn_MapVar( p, tn_min(i, j), tn_max(i, j), iVar ); +} +static inline int Tn_EdgeVar( tn_gr * p, int i, int j, int Mint ) +{ + assert( i != j ); + assert( Mint >= 0 && Mint < (1 << p->nIns) ); + return Tn_MapVar( p, tn_min(i, j), tn_max(i, j), p->nIns + Mint ); +} +static inline int Tn_NodeVar( tn_gr * p, int i, int Mint ) +{ + assert( Mint >= 0 && Mint < (1 << p->nIns) ); + return Tn_MapVar( p, i, i, p->nIns + Mint ); +} +static inline void Tn_PrintMapVar( tn_gr * p ) +{ + int i, j, n, Limit = 3; // p->nIns + (1 << p->nIns); + for ( n = 0; n < Limit; n++ ) { + printf("\n"); + printf( "Set %2d : ", n ); + for ( j = 0; j < p->nNodes; j++ ) + printf( "%4d", j ); + printf( "\n\n" ); + for ( i = 0; i < p->nNodes; i++ ) { + printf( "%6d : ", i ); + for ( j = 0; j < p->nNodes; j++ ) + printf( "%4d", Tn_MapVar(p, i, j, n) ); + printf( "\n" ); + } + } +} + +/************************************************************* + graph manipulation +**************************************************************/ + +static inline tn_gr * Tn_Init( int nIns, int nOuts, word * pOuts, char * pTypes, int nEdgeLimit, int nLevelLimit, int fVerbose ) +{ + tn_gr * p = (tn_gr *)calloc( sizeof(tn_gr), 1 ); int i; + p->nIns = nIns; + p->nOuts = nOuts; + p->nNodes = strlen(pTypes); + p->nNodes2 = p->nNodes * p->nNodes; + p->nMints = 1 << p->nIns; + p->nCnfVars = p->nNodes2 * (p->nIns + p->nMints); + p->pTypes = pTypes; + p->nEdgeLimit = nEdgeLimit; + p->nLevelLimit= nLevelLimit; + p->fVerbose = fVerbose; + for ( i = 0; i < p->nNodes; i++ ) + assert( pTypes[i] == '*' || pTypes[i] == '-' || (pTypes[i] >= '0' && pTypes[i] <= '2') ); + assert( 1 + p->nIns + p->nOuts <= p->nNodes && p->nNodes <= MSIZE ); + for ( i = 0; i < nOuts; i++ ) + p->pOuts[i] = pOuts[i]; + p->vCnf = tn_vi_alloc( 1000 ); + p->pVecs[0] = Tn_CutGen( p->nNodes, p->nIns ); // pos -> connected + p->pVecs[1] = Tn_PathGen( p->nNodes, p->nIns ); // neg -> disconnected + assert( p->nOuts >= 1 && p->nOuts <= 3 ); + if ( nOuts == 2 || nOuts == 3 ) { + Tn_SetSwap( (p->pVecs[2] = tn_vi_dup(p->pVecs[0])), p->nNodes-1, p->nNodes-2 ); + Tn_SetSwap( (p->pVecs[3] = tn_vi_dup(p->pVecs[1])), p->nNodes-1, p->nNodes-2 ); + } + if ( nOuts == 3 ) { + Tn_SetSwap( (p->pVecs[4] = tn_vi_dup(p->pVecs[0])), p->nNodes-1, p->nNodes-3 ); + Tn_SetSwap( (p->pVecs[5] = tn_vi_dup(p->pVecs[1])), p->nNodes-1, p->nNodes-3 ); + } + p->vTemp[0] = tn_vi_alloc( 100 ); + p->vTemp[1] = tn_vi_alloc( 100 ); + //printf( "Created graph with %d input, %d output, %d nodes and %s node types.\n", p->nIns, p->nOuts, p->nNodes, p->pTypes ); + return p; +} +static inline void Tn_Free( tn_gr * p ) +{ + tn_vi_free(p->vCnf); + for ( int i = 0; i < 6; i++ ) + if ( p->pVecs[i] ) + tn_vi_free(p->pVecs[i]); + tn_vi_free(p->vTemp[0]); + tn_vi_free(p->vTemp[1]); + free(p); +} +static inline int Tn_CountLabel( tn_gr * p ) +{ + int i, k, v, nLabels = 0; + if ( p->vSol == NULL ) + return 0; + for ( i = 0; i < p->nNodes-1; i++ ) + for ( k = i+1; k < p->nNodes; k++ ) + for ( v = 0; v < p->nIns; v++ ) + { + int ValP = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 0)) : 0; + int ValN = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 1)) : 0; + assert( ValP + ValN < 2 ); + nLabels += ValP + ValN; + } + return nLabels; +} +static inline void Tn_PrintStats( tn_gr * p ) +{ + printf( "Problem %s has %d inputs, %d outputs, %d nodes, and %d labels.\n", + p->pTypes, p->nIns, p->nOuts, p->nNodes-p->nIns, Tn_CountLabel(p) ); +} +static inline void Tn_PrintGraph( tn_gr * p ) +{ + int i, k, v, nLabels = 0; + if ( 0 && p->vSol ) { + tn_vi_for_each_entry( p->vSol, v, i ) + { + if ( i % p->nNodes2 == 0 ) + printf( "\n" ); + if ( i == p->nIns * p->nNodes2 ) + break; + if ( v == 1 ) + printf( " %d", i ); + } + printf( "\n"); + } + + printf( " " ); + for ( i = 0; i < p->nNodes; i++ ) { + for ( v = 0; v <= p->nIns-2; v++ ) + printf( " " ); + printf( "%2d", i ); + } + printf( "\n" ); + for ( i = 0; i < p->nNodes-1; i++, printf("\n") ) { + printf( "%2d : ", i ); + for ( k = 0; k < p->nNodes; k++ ) { + if ( k <= i ) + { + for ( v = 0; v <= p->nIns; v++ ) + printf( " " ); + continue; + } + for ( v = 0; v < p->nIns; v++ ) + { + int ValP = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 0)) : 0; + int ValN = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 1)) : 0; + assert( ValP + ValN < 2 ); + printf( "%c", ValP + ValN == 0 ? '-' : (ValP ? 'A' : 'a')+v ); + nLabels += ValP + ValN; + } + printf(" "); + } + } + //printf( "\nTotal labels = %d.\n\n", nLabels ); +} +static inline void Tn_PrintGraph2( tn_gr * p ) +{ + int i, k, v, nLabels = 0; + if ( 0 && p->vSol ) { + tn_vi_for_each_entry( p->vSol, v, i ) + { + if ( i % p->nNodes2 == 0 ) + printf( "\n" ); + if ( i == p->nIns * p->nNodes2 ) + break; + if ( v == 1 ) + printf( " %d", i ); + } + printf( "\n"); + } + + printf( " " ); + for ( i = p->nIns + 1; i < p->nNodes; i++ ) { + for ( v = 0; v <= p->nIns-2; v++ ) + printf( " " ); + printf( "%2d", i-p->nIns ); + } + printf( "\n" ); + for ( i = 0; i < p->nNodes-1; i++ ) { + if ( i >= 1 && i <= p->nIns ) + continue; + printf( "%2d : ", i ? i - p->nIns : 0 ); + for ( k = p->nIns + 1; k < p->nNodes; k++ ) { + if ( k <= i ) + { + for ( v = 0; v <= p->nIns; v++ ) + printf( " " ); + continue; + } + for ( v = 0; v < p->nIns; v++ ) + { + int ValP = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 0)) : 0; + int ValN = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 1)) : 0; + assert( ValP + ValN < 2 ); + printf( "%c", ValP + ValN == 0 ? '-' : (ValP ? 'A' : 'a')+v ); + nLabels += ValP + ValN; + } + printf(" "); + } + printf("\n"); + } + //printf( "\nTotal labels = %d.\n\n", nLabels ); +} + +/************************************************************* + CNF writing +**************************************************************/ + +static inline void Tn_DumpFile( tn_gr * p, const char * pFileName ) +{ + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) { + printf( "Cannot open file \"%s\" for writing CNF.\n", pFileName ); + return; + } + fprintf( pFile, "p cnf %d %d\n", p->nCnfVars, p->nCnfClas ); + int i, n, size, nClas = 0, * pArray = tn_vi_array(p->vCnf); + tn_vi_for_each_set( p->vCnf, size, i ) { + for ( n = 0; n < size; n++ ) + fprintf( pFile, "%s%d ", tn_l2c(pArray[i+n]) ? "-" : "", tn_l2v(pArray[i+n]) ); + fprintf( pFile, "0\n" ); + nClas++; + } + assert( nClas == p->nCnfClas ); + fclose( pFile ); + //printf( "Finished dumping CNF with %d variables and %d clauses.\n", p->nCnfVars, p->nCnfClas ); +} + +static inline int Tn_GenClause( tn_gr * p, int * pLits, int nLits ) +{ + int i, k = 0; + for ( i = 0; i < nLits; i++ ) { + if ( pLits[i] == 1 ) + return 0; + else if ( pLits[i] == 0 ) + continue; + else if ( pLits[i] <= 2*p->nCnfVars ) + pLits[k++] = pLits[i]; + else assert( 0 ); + } + nLits = k; + assert( nLits > 0 ); + //if ( p->pFile ) { + if ( 1 ) { + p->nCnfClas++; + //for ( i = 0; i < nLits; i++ ) + // fprintf( p->pFile, "%s%d ", tn_l2c(pLits[i]) ? "-" : "", tn_l2v(pLits[i]) ); + //fprintf( p->pFile, "0\n" ); + tn_vi_push( p->vCnf, nLits ); + for ( i = 0; i < nLits; i++ ) + tn_vi_push( p->vCnf, pLits[i] ); + } + if ( 0 ) + { + for ( i = 0; i < nLits; i++ ) + fprintf( stdout, "%s%d ", tn_l2c(pLits[i]) ? "-" : " ", tn_l2v(pLits[i]) ); + fprintf( stdout, "\n" ); + } + return 1; +} +static inline int Tn_GenClauseVec( tn_gr * p, tn_vi * v ) +{ + return Tn_GenClause( p, tn_vi_array(v), tn_vi_size(v) ); +} +static inline int Tn_GenClause4( tn_gr * p, int Lit0, int Lit1, int Lit2, int Lit3 ) +{ + int pLits[4] = { Lit0, Lit1, Lit2, Lit3 }; + return Tn_GenClause( p, pLits, 4 ); +} +// generate constraints for (Out = a0*b0 + a1*b1 + a2 + a3) +static inline void Tn_GenAndOrGate( tn_gr * pG, int iOutVar, tn_vi * vA, tn_vi * vB ) +{ + tn_vi * pArrays[2] = { vA, vB }; + assert( tn_vi_size(vA) >= tn_vi_size(vB) ); + int v, m, nmints = 1 << tn_vi_size(vB); + for ( m = 0; m < nmints; m++ ) { + int nvars = 0, pVars[MSIZE]; + pVars[nvars++] = tn_v2l( iOutVar, 1 ); + for ( v = 0; v < tn_vi_size(vB); v++ ) + pVars[nvars++] = tn_v2l( tn_vi_read(pArrays[(m>>v)&1], v), 0 ); + for ( ; v < tn_vi_size(vA); v++ ) + pVars[nvars++] = tn_v2l( tn_vi_read(pArrays[0], v), 0 ); + Tn_GenClause( pG, pVars, nvars ); + } + for ( v = 0; v < tn_vi_size(vA); v++ ) { + int nvars = 0, pVars[MSIZE]; + pVars[nvars++] = tn_v2l( iOutVar, 0 ); + if ( v < tn_vi_size(vB) ) + pVars[nvars++] = tn_v2l( tn_vi_read(vB, v), 1 ); + pVars[nvars++] = tn_v2l( tn_vi_read(vA, v), 1 ); + Tn_GenClause( pG, pVars, nvars ); + } +} +/************************************************************* + candinality constraint +**************************************************************/ + +static inline int Tn_AddClause( tn_vi * p, int* begin, int* end ) +{ + tn_vi_push( p, (int)(end-begin) ); + while ( begin < end ) + tn_vi_push( p, (int)*begin++ ); + return 1; +} +static inline int Tn_AddHalfSorter( tn_vi * p, int iVarA, int iVarB, int iVar0, int iVar1 ) +{ + int Lits[3]; + int Cid; + + Lits[0] = tn_v2l( iVarA, 0 ); + Lits[1] = tn_v2l( iVar0, 1 ); + Cid = Tn_AddClause( p, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = tn_v2l( iVarA, 0 ); + Lits[1] = tn_v2l( iVar1, 1 ); + Cid = Tn_AddClause( p, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = tn_v2l( iVarB, 0 ); + Lits[1] = tn_v2l( iVar0, 1 ); + Lits[2] = tn_v2l( iVar1, 1 ); + Cid = Tn_AddClause( p, Lits, Lits + 3 ); + assert( Cid ); + return 3; +} +static inline void Tn_AddSorter( tn_vi * p, int * pVars, int i, int k, int * pnVars ) +{ + int iVar1 = (*pnVars)++; + int iVar2 = (*pnVars)++; + Tn_AddHalfSorter( p, iVar1, iVar2, pVars[i], pVars[k] ); + pVars[i] = iVar1; + pVars[k] = iVar2; +} +static inline void Tn_AddCardinConstrMerge( tn_vi * p, int * pVars, int lo, int hi, int r, int * pnVars ) +{ + int i, step = r * 2; + if ( step < hi - lo ) + { + Tn_AddCardinConstrMerge( p, pVars, lo, hi-r, step, pnVars ); + Tn_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars ); + for ( i = lo+r; i < hi-r; i += step ) + Tn_AddSorter( p, pVars, i, i+r, pnVars ); + for ( i = lo+r; i < hi-r-1; i += r ) + { + int Lits[2] = { tn_v2l(pVars[i], 0), tn_v2l(pVars[i+r], 1) }; + int Cid = Tn_AddClause( p, Lits, Lits + 2 ); + assert( Cid ); + } + } +} +static inline void Tn_AddCardinConstrRange( tn_vi * p, int * pVars, int lo, int hi, int * pnVars ) +{ + if ( hi - lo >= 1 ) + { + int i, mid = lo + (hi - lo) / 2; + for ( i = lo; i <= mid; i++ ) + Tn_AddSorter( p, pVars, i, i + (hi - lo + 1) / 2, pnVars ); + Tn_AddCardinConstrRange( p, pVars, lo, mid, pnVars ); + Tn_AddCardinConstrRange( p, pVars, mid+1, hi, pnVars ); + Tn_AddCardinConstrMerge( p, pVars, lo, hi, 1, pnVars ); + } +} +int Tn_AddCardinConstrPairWise( tn_vi * p, tn_vi * vVars ) +{ + int nVars = tn_vi_size(vVars); + Tn_AddCardinConstrRange( p, tn_vi_array(vVars), 0, nVars - 1, &nVars ); + return nVars; +} +int Tn_AddCardinSolver( int LogN, tn_vi ** pvVars, tn_vi ** pvRes ) +{ + int i, nVars = 1 << LogN; + int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1); + tn_vi * vRes = tn_vi_alloc( 1000 ); + tn_vi * vVars = tn_vi_alloc( nVars ); + for ( i = 0; i < nVars; i++ ) + tn_vi_push( vVars, i ); + int nVarsReal = Tn_AddCardinConstrPairWise( vRes, vVars ); + assert( nVarsReal == nVarsAlloc ); + *pvVars = vVars; + *pvRes = vRes; + return nVarsReal; +} +void Tn_AddCardinality( tn_gr * p, tn_vi * vCard ) +{ + assert( p->nEdgeLimit ); + tn_vi * vVars = NULL; + tn_vi * vRes = NULL; + int LogN = Tn_Base2Log( tn_vi_size(vCard) ); + int nVarsReal = Tn_AddCardinSolver( LogN, &vVars, &vRes ), n, i, Var, size, pLits[2]; + p->nCnfVars2 = p->nCnfVars; + p->nCnfClas2 = p->nCnfClas; + p->nCnfVars += nVarsReal; + tn_vi_for_each_entry( vCard, Var, i ) { + for ( n = 0; n < 2; n++ ) { + pLits[0] = tn_v2l( Var, n ); + pLits[1] = tn_v2l( p->nCnfVars2+i, !n ); + Tn_GenClause( p, pLits, 2 ); + } + } + for ( ; i < (1<nCnfVars2+i, 1 ); + Tn_GenClause( p, pLits, 1 ); + } + int * pArray = tn_vi_array(vRes); + tn_vi_for_each_set( vRes, size, i ) { + for ( n = 0; n < size; n++ ) + pArray[i+n] += 2*p->nCnfVars2; + Tn_GenClause( p, pArray+i, size ); + } + pLits[0] = tn_v2l( p->nCnfVars2+tn_vi_read(vVars, p->nEdgeLimit), 1 ); + Tn_GenClause( p, pLits, 1 ); + tn_vi_free( vVars ); + tn_vi_free( vRes ); +} + +/************************************************************* + CNF generation +**************************************************************/ + +static inline tn_vi * Tn_GenCnfStart( tn_gr * p ) +{ + int i, j, n; + //printf( "The first controls\n" ); + for ( n = 0; n < p->nIns; n++ ) + for ( i = 1; i <=p->nIns; i++ ) + for ( j = 0; j < p->nNodes; j++ ) if ( i != j ) { + Tn_GenClause4( p, tn_v2l(Tn_CtrlVar(p, i, j, n, 0), 1), 0, 0, 0 ); + Tn_GenClause4( p, tn_v2l(Tn_CtrlVar(p, i, j, n, 1), 1), 0, 0, 0 ); + } + //printf( "Unused middle vars\n" ); + for ( n = 0; n < p->nIns; n++ ) + for ( i = 0; i < p->nNodes; i++ ) + Tn_GenClause4( p, tn_v2l(Tn_MapVar(p, i, i, n), 1), 0, 0, 0 ); + //printf( "The other controls\n" ); + tn_vi * vCard = tn_vi_alloc( 100 ); + for ( n = 0; n < p->nIns; n++ ) + for ( i = 0; i < p->nNodes; i++ ) { + if ( i >= 1 && i <= p->nIns ) + continue; + for ( j = i+1; j < p->nNodes; j++ ) { + if ( j >= 1 && j <= p->nIns ) + continue; + if ( p->pTypes[1+n] == '0' ) { // negative - remove positive (i < j) + Tn_GenClause4( p, tn_v2l(Tn_CtrlVar(p, i, j, n, 0), 1), 0, 0, 0 ); + tn_vi_push( vCard, Tn_CtrlVar(p, i, j, n, 1) ); + } + else if ( p->pTypes[1+n] == '1' ) { // positive - remove negative (i > j) + Tn_GenClause4( p, tn_v2l(Tn_CtrlVar(p, i, j, n, 1), 1), 0, 0, 0 ); + tn_vi_push( vCard, Tn_CtrlVar(p, i, j, n, 0) ); + } + else if ( p->pTypes[1+n] == '-' || p->pTypes[1+n] == '*' ) { + Tn_GenClause4( p, tn_v2l(Tn_CtrlVar(p, i, j, n, 0), 1), 0, 0, 0 ); + Tn_GenClause4( p, tn_v2l(Tn_CtrlVar(p, i, j, n, 1), 1), 0, 0, 0 ); + } + else if ( p->pTypes[1+n] == '2' ) { + tn_vi_push( vCard, Tn_CtrlVar(p, i, j, n, 0) ); + tn_vi_push( vCard, Tn_CtrlVar(p, i, j, n, 1) ); + } + else assert( 0 ); + } + } + //printf( "Pair-wise one-hot\n" ); + for ( n = 0; n < p->nIns; n++ ) + for ( i = 0; i < p->nNodes; i++ ) + for ( j = i+1; j < p->nNodes; j++ ) + Tn_GenClause4( p, tn_v2l(Tn_CtrlVar(p, i, j, n, 0), 1), tn_v2l(Tn_CtrlVar(p, i, j, n, 1), 1), 0, 0 ); + return vCard; +} +static inline void Tn_GenCnfMint( tn_gr * p, int m, int mout ) +{ + int i, j, v, size; +/* + //printf( "Generating minterm %d / %d:\n", m, mout ); + Tn_GenClause4( p, tn_v2l(Tn_NodeVar(p, 0, m), 0), 0, 0, 0 ); + for ( i = 0; i < p->nIns; i++ ) + Tn_GenClause4( p, tn_v2l(Tn_NodeVar(p, 1+i, m), ((m>>i)&1)==0), 0, 0, 0 ); + for ( i = 0; i < p->nOuts; i++ ) + Tn_GenClause4( p, tn_v2l(Tn_NodeVar(p, p->nNodes-p->nOuts+p->nOuts-1-i, m), ((mout>>i)&1)==0), 0, 0, 0 ); + //printf( "Functionality:\n" ); + for ( i = 0; i < p->nNodes; i++ ) + for ( j = i+1; j < p->nNodes; j++ ) + { + int iEdge = Tn_EdgeVar(p, i, j, m); + int iNodeI = Tn_NodeVar(p, i, m); + int iNodeJ = Tn_NodeVar(p, j, m); + Tn_GenClause4( p, tn_v2l(iEdge, 1), tn_v2l(iNodeI, 0), tn_v2l(iNodeJ, 1), 0 ); + Tn_GenClause4( p, tn_v2l(iEdge, 1), tn_v2l(iNodeI, 1), tn_v2l(iNodeJ, 0), 0 ); + } +*/ + //printf( "Edge variables:\n" ); + for ( i = 0; i < p->nNodes; i++ ) + for ( j = i+1; j < p->nNodes; j++ ) + { + tn_vi_resize( p->vTemp[0], 0 ); + tn_vi_resize( p->vTemp[1], 0 ); + for ( v = 0; v < p->nIns; v++ ) + tn_vi_push( p->vTemp[0], Tn_CtrlVar(p, i, j, v, ((m>>v)&1)==0) ); + Tn_GenAndOrGate( p, Tn_EdgeVar(p, i, j, m), p->vTemp[0], p->vTemp[1] ); + } + //printf( "Connectivity:\n" ); + for ( i = 0; i < p->nOuts; i++ ) + { + if ( (mout>>i)&1 ) { // p->pVecs[0] pos cut vars -> connected + tn_vi_for_each_set( p->pVecs[2*i+0], size, j ) { + assert( (size & 1) == 0 ); + tn_vi_resize( p->vTemp[0], 0 ); + for ( v = 0; v < size/2; v++ ) { + int start = tn_vi_read(p->pVecs[2*i+0], j+2*v+0); + int next = tn_vi_read(p->pVecs[2*i+0], j+2*v+1); + tn_vi_push( p->vTemp[0], tn_v2l(Tn_EdgeVar(p, start, next, m), 0) ); + } + Tn_GenClauseVec( p, p->vTemp[0] ); + } + if ( p->nLevelLimit == 0 ) + continue; + tn_vi_for_each_set( p->pVecs[2*i+1], size, j ) { // p->pVecs[1] neg path vars -> disconnected + if ( size <= p->nLevelLimit+1 ) + continue; + int next, start = tn_vi_read(p->pVecs[2*i+1], j); + tn_vi_resize( p->vTemp[0], 0 ); + for ( v = 1; v < size && (next = tn_vi_read(p->pVecs[2*i+1], j+v)); v++, start = next ) + tn_vi_push( p->vTemp[0], tn_v2l(Tn_EdgeVar(p, start, next, m), 1) ); + Tn_GenClauseVec( p, p->vTemp[0] ); + } + } + else { // p->pVecs[1] neg path vars -> disconnected + tn_vi_for_each_set( p->pVecs[2*i+1], size, j ) { + int next, start = tn_vi_read(p->pVecs[2*i+1], j); + tn_vi_resize( p->vTemp[0], 0 ); + for ( v = 1; v < size && (next = tn_vi_read(p->pVecs[2*i+1], j+v)); v++, start = next ) + tn_vi_push( p->vTemp[0], tn_v2l(Tn_EdgeVar(p, start, next, m), 1) ); + Tn_GenClauseVec( p, p->vTemp[0] ); + } + } + } +} +static inline void Tn_GenCnf( tn_gr * p, const char * pFileName ) +{ + int o, m, mout; + assert( p->pFile == NULL ); + p->pFile = fopen( pFileName, "wb" ); + if ( p->pFile == NULL ) { + printf( "Cannot open file \"%s\" for writing CNF.\n", pFileName ); + return; + } + fputs( "p cnf \n", p->pFile ); + tn_vi * vCard = Tn_GenCnfStart( p ); + for ( m = 0; m < (1<nIns); m++ ) { + for ( mout = o = 0; o < p->nOuts; o++ ) + if ( (p->pOuts[o] >> m) & 1 ) + mout |= 1 << o; + Tn_GenCnfMint( p, m, mout ); + } + if ( p->nEdgeLimit > 0 ) + Tn_AddCardinality( p, vCard ); + rewind( p->pFile ); + fprintf( p->pFile, "p cnf %d %d", p->nCnfVars, p->nCnfClas ); + fclose( p->pFile ); + p->pFile = NULL; + printf( "Dumped file \"%s\" with %d vars and %d clauses (%d out of %d: %d vars and %d clauses).\n", + pFileName, p->nCnfVars, p->nCnfClas, p->nEdgeLimit, tn_vi_size(vCard), + p->nCnfVars2 ? p->nCnfVars-p->nCnfVars2 : 0, + p->nCnfClas2 ? p->nCnfClas-p->nCnfClas2 : 0 ); + tn_vi_free( vCard ); +} +static inline void Tn_GenCnf2( tn_gr * p ) +{ + int o, m, mout; + assert( tn_vi_size(p->vCnf) == 0 ); + tn_vi * vCard = Tn_GenCnfStart( p ); + for ( m = 0; m < (1<nIns); m++ ) { + for ( mout = o = 0; o < p->nOuts; o++ ) + if ( (p->pOuts[o] >> m) & 1 ) + mout |= 1 << o; + Tn_GenCnfMint( p, m, mout ); + } + if ( p->nEdgeLimit > 0 ) + Tn_AddCardinality( p, vCard ); + printf( "Created CNF with %d vars and %d clauses (%d out of %d: %d vars and %d clauses).\n", + p->nCnfVars, p->nCnfClas, p->nEdgeLimit, tn_vi_size(vCard), + p->nCnfVars2 ? p->nCnfVars-p->nCnfVars2 : 0, + p->nCnfClas2 ? p->nCnfClas-p->nCnfClas2 : 0 ); + tn_vi_free( vCard ); +} + +/************************************************************* + Reading input data +**************************************************************/ + +// truth table size in 64-bit words +static inline int Tn_TruthWordNum( int n ) { return n <= 6 ? 1 : 1 << (n-6); } +static inline int Tn_HexDigitNum( int n ) { return n <= 2 ? 1 : 1 << (n-2); } + +static inline int Tn_Hex2Int( char c ) { + int Digit = 0; + if ( c >= '0' && c <= '9' ) + Digit = c - '0'; + else if ( c >= 'A' && c <= 'F' ) + Digit = c - 'A' + 10; + else if ( c >= 'a' && c <= 'f' ) + Digit = c - 'a' + 10; + else return -1; + assert( Digit >= 0 && Digit < 16 ); + return Digit; +} +static inline void Tn_PrintHexTruth( FILE * pFile, word * pTruth, int nVars ) { + int k, Digit, nDigits = Tn_HexDigitNum(nVars); + for ( k = nDigits-1; k >= 0; k-- ) { + Digit = (int)((pTruth[k/16] >> ((k%16) * 4)) & 15); + if ( Digit < 10 ) + fprintf( pFile, "%d", Digit ); + else + fprintf( pFile, "%c", 'A' + Digit-10 ); + } +} +int Tn_ReadHexTruth( char * pInput, word * pTruth ) +{ + int nChars = strlen(pInput), i; + int nVars = Tn_Base2Log(4*nChars); + if ( (1 << nVars) != 4*nChars ) { + printf( "The input string length (%d chars) does not match the size (%d bits) of the truth table of %d-var function.\n", + nChars, 1<= 0; i-- ) { + Num |= (word)Tn_Hex2Int(pInput[nChars-1-i]) << ((i & 0xF) * 4); + if ( (i & 0xF) == 0 ) + pTruth[i>>4] = Num, Num = 0; + } + assert( Num == 0 ); + printf( "Finished entring %d-input function: ", nVars ); + Tn_PrintHexTruth( stdout, pTruth, nVars ); + printf( "\n" ); + return nVars; +} + +/************************************************************* + dumping spice format +**************************************************************/ + +static inline void Tn_DumpNode( tn_gr * p, FILE * pFile, int i ) +{ + if ( i == 0 ) + fprintf( pFile, " VDD" ); + else if ( i >= p->nNodes - p->nOuts ) { + fprintf( pFile, " Y" ); + Tn_PrintHexTruth( pFile, p->pOuts+(i-(p->nNodes - p->nOuts)), p->nIns ); + } + else + fprintf( pFile, " net%d", i-p->nIns ); +} +static inline int Tn_DumpLabels( tn_gr * p, FILE * pFile ) +{ + int i, k, v, nLabels = 0; + if ( p->vSol == NULL ) + return 0; + for ( i = 0; i < p->nNodes-1; i++ ) + for ( k = i+1; k < p->nNodes; k++ ) + for ( v = 0; v < p->nIns; v++ ) + { + int ValP = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 0)) : 0; + int ValN = p->vSol ? tn_vi_read(p->vSol, Tn_CtrlVar(p, i, k, v, 1)) : 0; + assert( ValP + ValN < 2 ); + if ( ValP + ValN == 0 ) + continue; + // MM1 net10 B VDD VDD pmos_rvt w=xxxn l=yyyn nfin=2 + fprintf( pFile, "mm%d", nLabels ); + Tn_DumpNode( p, pFile, tn_max(i, k) ); + fprintf( pFile, " %c", 'A'+v ); + Tn_DumpNode( p, pFile, tn_min(i, k)); + fprintf( pFile, " VDD" ); + fprintf( pFile, " %cmos_rvt\n", ValP ? 'p' : 'n' ); + nLabels += ValP + ValN; + } + return nLabels; +} +static inline void Tn_DumpSpice( tn_gr * p ) +{ + const char * pFileName = "temp.sp"; int i; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) { + printf( "Cannot open file \"%s\" for writing SPICE format.\n", pFileName ); + return; + } + //.SUBCKT A VDD VSS Y + fprintf( pFile, ".SUBCKT tn" ); + for ( i = 0; i < p->nOuts; i++ ) { + fprintf( pFile, "_" ); + Tn_PrintHexTruth( pFile, p->pOuts+i, p->nIns ); + } + for ( i = 0; i < p->nIns; i++ ) + fprintf( pFile, " %c", 'A' + i ); + fprintf( pFile, " VDD VSS"); + for ( i = 0; i < p->nOuts; i++ ) { + fprintf( pFile, " Y" ); + Tn_PrintHexTruth( pFile, p->pOuts+i, p->nIns ); + } + fprintf( pFile, "\n"); + Tn_DumpLabels( p, pFile ); + fprintf( pFile, ".ENDS\n\n" ); + fclose( pFile ); + printf( "Finished dumping SPICE description into file \"%s\".\n", pFileName ); +} + +/************************************************************* + Solving the problem +**************************************************************/ + +tn_vi * Tn_ParseSolution( const char * pFileName ) +{ + tn_vi * vRes = NULL; + char * pToken, pBuffer[1000]; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\".\n", pFileName ); + return NULL; + } + while ( fgets( pBuffer, 1000, pFile ) != NULL ) + { + if ( pBuffer[0] == 's' ) + { + if ( strncmp(pBuffer+2, "SAT", 3) ) + break; + assert( vRes == NULL ); + vRes = tn_vi_alloc( 100 ); + } + else if ( pBuffer[0] == 'v' ) + { + pToken = strtok( pBuffer+1, " \n\r\t" ); + while ( pToken ) + { + int Token = atoi(pToken); + if ( Token == 0 ) + break; + int nSizeMax = tn_abs(Token) + 1; + while ( tn_vi_size(vRes) < nSizeMax ) + tn_vi_push( vRes, -1 ); + tn_vi_write( vRes, tn_abs(Token), Token > 0 ); + //Vec_IntSetEntryFull( vRes, Tn_AbsInt(Token), Token > 0 ); + pToken = strtok( NULL, " \n\r\t" ); + } + } + else if ( pBuffer[0] != 'c' ) + assert( 0 ); + } + fclose( pFile ); + unlink( pFileName ); + return vRes; +} +tn_vi * Tn_SolveSat( const char * pFileNameIn, const char * pFileNameOut, int Seed, int TimeOut, int fVerbose ) +{ + int fVerboseSolver = 0; + iword clkTotal = Tn_Clock(); + tn_vi * vRes = NULL; +#ifdef _WIN32 + const char * pKissat = "kissat.exe"; +#else + const char * pKissat = "kissat"; +#endif + char Command[1000], * pCommand = (char *)&Command; + if ( TimeOut ) + sprintf( pCommand, "%s --seed=%d --time=%d %s %s > %s", pKissat, Seed, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + else + sprintf( pCommand, "%s --seed=%d %s %s > %s", pKissat, Seed, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + //if ( fVerbose ) + // printf( "Running command line: %s\n", pCommand ); + if ( system( pCommand ) == -1 ) + { + printf( "Command \"%s\" did not succeed.\n", pCommand ); + return 0; + } + vRes = Tn_ParseSolution( pFileNameOut ); + if ( fVerbose ) + { + if ( vRes ) + printf( "The problem has a solution. " ); + else if ( vRes == NULL && TimeOut == 0 ) + printf( "The problem has no solution. " ); + else if ( vRes == NULL ) + printf( "The problem has no solution or timed out after %d sec. ", TimeOut ); + Tn_PrintTime( "SAT solver time", Tn_Clock() - clkTotal ); + } + return vRes; +} +static inline void Tn_AppendClause( tn_gr * p, tn_vi * vSol ) +{ + int v, k = 0, Limit = p->nIns * p->nNodes2; + for ( v = 1; v < Limit; v++ ) + if ( tn_vi_read(p->vSol, v) ) + tn_vi_write( p->vSol, k++, tn_v2l(v, 1) ); + tn_vi_resize( p->vSol, k ); + Tn_GenClauseVec( p, p->vSol ); + //printf("Finished adding clause: "); + //tn_vi_print( p->vSol ); +} +void Tn_SolveProblem( int nIns, int nOuts, word * pOuts, char * pTypes, int nEdgeLimit, int nLevelLimit, int nSolsMax, int Seed, int TimeOut, int fVerbose ) +{ + const char * pFileNameIn = "_temp_.cnf"; + const char * pFileNameOut = "_temp_.txt"; + tn_gr * p = Tn_Init( nIns, nOuts, pOuts, pTypes, nEdgeLimit, nLevelLimit, fVerbose ); + //Tn_PrintMapVar( p ); + Tn_GenCnf2( p ); + for ( int n = 0; n < nSolsMax; n++ ) { + printf( "\nIteration %d:\n", n ); + Tn_DumpFile( p, pFileNameIn ); + p->vSol = Tn_SolveSat( pFileNameIn, pFileNameOut, Seed, TimeOut, fVerbose ); + Tn_PrintStats( p ); + if ( p->vSol ) { + //Tn_PrintGraph( p ); + Tn_PrintGraph2( p ); + Tn_DumpSpice( p ); + Tn_AppendClause( p, p->vSol ); + tn_vi_free( p->vSol ); + p->vSol = NULL; + } + else { + printf( "Problem has no solution.\n" ); + break; + } + } + Tn_Free( p ); +} + +/************************************************************* + main() procedure +**************************************************************/ + +#if 0 + +int main(int argc, char ** argv) +{ + if ( argc == 1 ) + { + printf( "usage: %s -C [-ELNSTV ] ... \n", argv[0] ); + printf( " this program synthesizes networks for multi-output functions\n" ); + printf( "\n" ); + printf( " -C : the configuration string (no default)\n" ); + printf( " -E : the max number of edges (default = no limit)\n" ); + printf( " -L : the max number of levels (default = no limit)\n" ); + printf( " -N : the max number of solutions (default = 1)\n" ); + printf( " -S : the random seed (default = 0)\n" ); + printf( " -T : the timeout in seconds (default = no timeout)\n" ); + printf( " -V : the verbosiness levels (default = 1)\n" ); + printf( " : the truth table of the first output in the hexadecimal notation\n" ); + printf( " : the truth table of the last output in the hexadecimal notation\n" ); + printf( " the truth tables are assumed to depend on the same variables\n" ); + printf( " the strings should contain 2^(-2) hexadecimal digits\n" ); + printf( "\n" ); + printf( " Example 1: Synthesizing 3-node 2-edge 2-input and-gate:\n" ); + printf( " %s -C *11** -E 2 8\n", argv[0] ); + printf( " Example 2: Synthesizing 4-node 5-edge 3-input majority gate:\n" ); + printf( " %s -C *111*** -E 5 E8\n", argv[0] ); +// printf( " Example 3: Synthesizing 9-node 10-edge 3-input 2-output full-adder:\n" ); +// printf( " %s -C *111****1 -E 10 96 E8\n", argv[0] ); + return 1; + } + else + { + int nIns = 0, nOuts = 0, nEdgeLimit = 0, nLevelLimit = 0, nSolsMax = 1, Seed = 0, TimeOut = 0, fVerbose = 1; + char * pTypes = NULL; + word Truths[MSIZE] = {0}; + for ( int c = 1; c < argc; c++ ) { + if ( argv[c][0] == '-' && argv[c][1] == 'C' ) + pTypes = argv[++c]; + else if ( argv[c][0] == '-' && argv[c][1] == 'E' ) + nEdgeLimit = atoi(argv[++c]); + else if ( argv[c][0] == '-' && argv[c][1] == 'L' ) + nLevelLimit = atoi(argv[++c]); + else if ( argv[c][0] == '-' && argv[c][1] == 'N' ) + nSolsMax = atoi(argv[++c]); + else if ( argv[c][0] == '-' && argv[c][1] == 'S' ) + Seed = atoi(argv[++c]); + else if ( argv[c][0] == '-' && argv[c][1] == 'T' ) + TimeOut = atoi(argv[++c]); + else if ( argv[c][0] == '-' && argv[c][1] == 'V' ) + fVerbose = atoi(argv[++c]); + else if ( Tn_Hex2Int(argv[c][0]) != -1 ) { + int nVarsOut = Tn_ReadHexTruth( argv[c], Truths + nOuts++ ); + if ( nIns == 0 ) + nIns = nVarsOut; + else if ( nIns != nVarsOut ) { + printf( "The support size of output functions is not the same.\n" ); + break; + } + } + else { + printf( "String \"%s\" does not look like a truth table in the hexadecimal notation.\n", argv[c] ); + break; + } + } + printf( "Finished reading %d output%s\n\n", nOuts, nOuts == 1 ? "" : "s" ); + Tn_SolveProblem( nIns, nOuts, Truths, pTypes, nEdgeLimit, nLevelLimit, nSolsMax, Seed, TimeOut, fVerbose ); + return 1; + } +} + +#endif + +/************************************************************* + end of file +**************************************************************/ + +ABC_NAMESPACE_IMPL_END +