diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-08-05 11:11:04 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-08-05 11:11:04 -0700 |
commit | 2ad79b94a5b67f5fee70a87f3d81f45dcc68a98a (patch) | |
tree | 5e2e18947a96141ad2061289150f96b6aa8fe1ab /src | |
parent | 2792979594ebe3dce8c7ffa11b03d024065a2b9b (diff) | |
parent | 46a1c816037e33a53a2ad147cd211d6f74acacec (diff) | |
download | abc-2ad79b94a5b67f5fee70a87f3d81f45dcc68a98a.tar.gz abc-2ad79b94a5b67f5fee70a87f3d81f45dcc68a98a.tar.bz2 abc-2ad79b94a5b67f5fee70a87f3d81f45dcc68a98a.zip |
Merged in msoeken/abc-exact (pull request #35)
Updates to delay-estimation API with exact synthesis
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 196 | ||||
-rw-r--r-- | src/base/abci/abcExact.c | 241 |
2 files changed, 383 insertions, 54 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d49db050..4dc50ed2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -136,6 +136,9 @@ static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDetect ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExact ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBmsStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBmsStop ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -777,6 +780,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "detect", Abc_CommandDetect, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 ); + Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 ); + Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_stop", Abc_CommandBmsStop, 0 ); + Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_ps", Abc_CommandBmsPs, 0 ); + Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 ); Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); @@ -7386,7 +7393,7 @@ usage: Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" ); Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" ); Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" ); - Abc_Print( -2, "\t-a : create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); + Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); Abc_Print( -2, "\t-t : run test suite\n" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); @@ -7407,6 +7414,185 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Abc_ExactIsRunning(); + extern void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char *pFilename ); + + int c, fMakeAIG = 0, fVerbose = 0, nBTLimit = 10000; + char * pFilename = NULL; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Cavh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'a': + fMakeAIG ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( argc > globalUtilOptind ) + { + pFilename = argv[globalUtilOptind++]; + } + + if ( Abc_ExactIsRunning() ) + { + Abc_Print( -1, "BMS manager is already started." ); + return 1; + } + + Abc_ExactStart( nBTLimit, fMakeAIG, fVerbose, pFilename ); + return 0; + +usage: + Abc_Print( -2, "usage: bms_start [-C <num>] [-avh] [<file>]\n" ); + Abc_Print( -2, "\t starts BMS manager for recording optimum networks\n" ); + Abc_Print( -2, "\t if <file> is specified, store entries are read from that file\n" ); + Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); + Abc_Print( -2, "\t-h : print the command usage\n" ); + Abc_Print( -2, "\t\n" ); + Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" ); + Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandBmsStop( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Abc_ExactIsRunning(); + extern void Abc_ExactStop( const char *pFilename ); + + int c; + char * pFilename = NULL; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( argc > globalUtilOptind ) + { + pFilename = argv[globalUtilOptind++]; + } + + if ( !Abc_ExactIsRunning() ) + { + Abc_Print( -1, "BMS manager is not started." ); + return 1; + } + + Abc_ExactStop( pFilename ); + return 0; + +usage: + Abc_Print( -2, "usage: bms_stop [-C <num>] [-vh] [<file>]\n" ); + Abc_Print( -2, "\t stops BMS manager for recording optimum networks\n" ); + Abc_Print( -2, "\t if <file> is specified, store entries are written to that file\n" ); + Abc_Print( -2, "\t-h : print the command usage\n" ); + Abc_Print( -2, "\t\n" ); + Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" ); + Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandBmsPs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Abc_ExactIsRunning(); + extern void Abc_ExactStats(); + + int c; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( !Abc_ExactIsRunning() ) + { + Abc_Print( -1, "BMS manager is not started." ); + return 1; + } + + Abc_ExactStats(); + return 0; + +usage: + Abc_Print( -2, "usage: bms_ps [-h]\n" ); + Abc_Print( -2, "\t shows statistics about BMS manager\n" ); + Abc_Print( -2, "\t-h : print the command usage\n" ); + Abc_Print( -2, "\t\n" ); + Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" ); + Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk, * pNtkRes; @@ -16928,7 +17114,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( Abc_NtkRecInputNum3() != pPars->nLutSize ) { - printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize ); + printf( "The number of library inputs (%d) is different from the K parameters (%d).\n", Abc_NtkRecInputNum3(), pPars->nLutSize ); return 0; } } @@ -16937,12 +17123,12 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( !Abc_ExactIsRunning() ) { - printf( "LMS manager is not running (use \"rec_start3\").\n" ); + printf( "BMS manager is not running (use \"bms_start\").\n" ); return 0; } - if ( Abc_ExactInputNum() != pPars->nLutSize ) + if ( Abc_ExactInputNum() < pPars->nLutSize ) { - printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize ); + printf( "The number of library inputs (%d) is smaller than the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize ); return 0; } } diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 94325f4a..d739118a 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -50,6 +50,10 @@ static word s_Truths8[32] = { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF) }; +#define ABC_EXACT_SOL_NVARS 0 +#define ABC_EXACT_SOL_NFUNC 1 +#define ABC_EXACT_SOL_NGATES 2 + typedef struct Ses_Man_t_ Ses_Man_t; struct Ses_Man_t_ { @@ -120,9 +124,15 @@ struct Ses_TruthEntry_t_ typedef struct Ses_Store_t_ Ses_Store_t; struct Ses_Store_t_ { + int fMakeAIG; /* create AIG instead of general network */ int fVerbose; /* be verbose */ int nBTLimit; /* conflict limit */ + int nEntriesCount; /* number of entries */ Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */ + + unsigned long nCutCount; + unsigned long pCutCount[9]; + unsigned long nCacheHit; }; static Ses_Store_t * s_pSesStore = NULL; @@ -155,13 +165,19 @@ static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * ma return delta; } -static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fVerbose ) +static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose ) { Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 ); - pStore->fVerbose = fVerbose; - pStore->nBTLimit = nBTLimit; + pStore->fMakeAIG = fMakeAIG; + pStore->fVerbose = fVerbose; + pStore->nBTLimit = nBTLimit; + pStore->nEntriesCount = 0; memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE ); + pStore->nCutCount = 0; + memset( pStore->pCutCount, 0, 9 ); + pStore->nCacheHit = 0; + return pStore; } @@ -294,6 +310,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr /* item has been added */ fAdded = 1; + pStore->nEntriesCount++; } else /* item was already present */ @@ -350,6 +367,85 @@ char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * return pTiEntry->pNetwork; } +static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) +{ + int i; + Ses_TruthEntry_t * pTEntry; + Ses_TimesEntry_t * pTiEntry; + FILE * pFile; + + pFile = fopen( pFilename, "wb" ); + if (pFile == NULL) + { + printf( "cannot open file \"%s\" for writing\n", pFilename ); + return; + } + + fwrite( &pStore->nEntriesCount, sizeof( int ), 1, pFile ); + + for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i ) + if ( pStore->pEntries[i] ) + { + pTEntry = pStore->pEntries[i]; + + while ( pTEntry ) + { + pTiEntry = pTEntry->head; + while ( pTiEntry ) + { + fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile ); + fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile ); + fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile ); + fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile ); + pTiEntry = pTiEntry->next; + } + pTEntry = pTEntry->next; + } + } + + + fclose( pFile ); +} + +static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename ) +{ + int i, nEntries; + word pTruth[4]; + int nVars; + int pArrTimeProfile[8]; + char pHeader[3]; + char * pNetwork; + FILE * pFile; + + pFile = fopen( pFilename, "rb" ); + if (pFile == NULL) + { + printf( "cannot open file \"%s\" for reading\n", pFilename ); + return; + } + + fread( &nEntries, sizeof( int ), 1, pFile ); + + for ( i = 0; i < nEntries; ++i ) + { + fread( pTruth, sizeof( word ), 4, pFile ); + fread( &nVars, sizeof( int ), 1, pFile ); + fread( pArrTimeProfile, sizeof( int ), 8, pFile ); + fread( pHeader, sizeof( char ), 3, pFile ); + + pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] ); + pNetwork[0] = pHeader[0]; + pNetwork[1] = pHeader[1]; + pNetwork[2] = pHeader[2]; + + fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile ); + + Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork ); + } + + fclose( pFile ); +} + static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int fVerbose ) { int h, i; @@ -524,7 +620,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int assert( value ); } -static void Ses_ManCreateClauses( Ses_Man_t * pSes ) +static int Ses_ManCreateClauses( Ses_Man_t * pSes ) { extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 ); @@ -731,10 +827,13 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) { pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 ); - assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ) + return 0; } } } + + return 1; } /**Function************************************************************* @@ -798,9 +897,6 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) // delay: maximum delay to output (taking arrival times into account, not normalized) or 0 if not specified // pin[i]: pin to pin delay to input i or 0 if not specified or if there is no connection to input i // NOTE: since outputs can only point to gates, delay and pin-to-pin times cannot be 0 -#define ABC_EXACT_SOL_NVARS 0 -#define ABC_EXACT_SOL_NFUNC 1 -#define ABC_EXACT_SOL_NGATES 2 static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) { int nSol, h, i, j, k, l, aj, ak, d, nOp; @@ -1129,7 +1225,8 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) return 0; Ses_ManCreateVars( pSes, nGates ); - Ses_ManCreateClauses( pSes ); + if ( !Ses_ManCreateClauses( pSes ) ) + return 0; /* proven UNSAT while creating clauses */ switch ( Ses_ManSolve( pSes ) ) { @@ -1350,59 +1447,106 @@ int Abc_ExactInputNum() return 8; } // start exact store manager -void Abc_ExactStart( int nBTLimit, int fVerbose ) +void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char * pFilename ) { if ( !s_pSesStore ) - s_pSesStore = Ses_StoreAlloc( nBTLimit, fVerbose ); + { + s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose ); + if ( pFilename ) + Ses_StoreRead( s_pSesStore, pFilename ); + } else - printf( "exact store manager already started\n" ); + printf( "BMS manager already started\n" ); } // stop exact store manager -void Abc_ExactStop() +void Abc_ExactStop( const char * pFilename ) { if ( s_pSesStore ) + { + if ( pFilename ) + Ses_StoreWrite( s_pSesStore, pFilename ); Ses_StoreClean( s_pSesStore ); + } else - printf( "exact store manager has not been started\n" ); + printf( "BMS manager has not been started\n" ); +} +// show statistics about store manager +void Abc_ExactStats() +{ + int i; + + if ( !s_pSesStore ) + { + printf( "BMS manager has not been started\n" ); + return; + } + + printf( "number of considered cuts :" ); + for ( i = 2; i < 9; ++i ) + printf( " %d = %lu ", i, s_pSesStore->pCutCount[i] ); + printf( " total = %lu\n", s_pSesStore->nCutCount ); + printf( "cache hits : %lu\n", s_pSesStore->nCacheHit ); + printf( "number of entries : %d\n", s_pSesStore->nEntriesCount ); } // this procedure takes TT and input arrival times (pArrTimeProfile) and return the smallest output arrival time; // it also returns the pin-to-pin delays (pPerm) between each cut leaf and the cut output and the cut area cost (Cost) // the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost, int AigLevel ) { - int i, l; - Ses_Man_t * pSes; + int i, l, fExists = 0; + Ses_Man_t * pSes = NULL; char * pSol = NULL, * p; int Delay = ABC_INFINITY, nMaxDepth; abctime timeStart; /* some checks */ - assert( nVars >= 2 && nVars <= 8 ); + if ( nVars < 2 || nVars > 8 ) + { + printf( "invalid truth table size %d\n", nVars ); + assert( 0 ); + } - nMaxDepth = pArrTimeProfile[0]; - for ( i = 1; i < nVars; ++i ) - nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] ); - nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 ); + /* statistics */ + s_pSesStore->nCutCount++; + s_pSesStore->pCutCount[nVars]++; - timeStart = Abc_Clock(); + pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile ); + if ( pSol ) + { + s_pSesStore->nCacheHit++; + fExists = 1; + } + else + { + nMaxDepth = pArrTimeProfile[0]; + for ( i = 1; i < nVars; ++i ) + nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] ); + nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 ); - *Cost = ABC_INFINITY; + timeStart = Abc_Clock(); - pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, s_pSesStore->fVerbose ); - pSes->nBTLimit = s_pSesStore->nBTLimit; + *Cost = ABC_INFINITY; - while ( 1 ) /* there is improvement */ - { - printf( "try with %d\n", pSes->nMaxDepth ); - if ( Ses_ManFindMinimumSize( pSes ) ) + pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose ); + pSes->nBTLimit = s_pSesStore->nBTLimit; + + while ( 1 ) /* there is improvement */ { - if ( pSol ) - ABC_FREE( pSol ); - pSol = Ses_ManExtractSolution( pSes ); - pSes->nMaxDepth--; + if ( Ses_ManFindMinimumSize( pSes ) ) + { + if ( pSol ) + ABC_FREE( pSol ); + pSol = Ses_ManExtractSolution( pSes ); + pSes->nMaxDepth--; + } + else + break; } - else - break; + + pSes->timeTotal = Abc_Clock() - timeStart; + + /* cleanup */ + Ses_ManClean( pSes ); } if ( pSol ) @@ -1414,15 +1558,10 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm[l] = *p++; /* store solution */ - if ( !Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ) ) - ABC_FREE( pSol ); /* store entry already exists, so free solution */ + if ( !fExists ) + Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ); } - pSes->timeTotal = Abc_Clock() - timeStart; - - /* cleanup */ - Ses_ManClean( pSes ); - return Delay; } // this procedure returns a new node whose output in terms of the given fanins @@ -1430,7 +1569,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins ) { char * pSol; - int i; + int i, j; char const * p; Abc_Obj_t * pObj; Vec_Ptr_t * pGates; @@ -1468,6 +1607,11 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, assert( *p == 2 ); /* binary gate */ ++p; + /* invert truth table if we are last gate and inverted */ + if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) ) + for ( j = 0; j < 4; ++j ) + pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0'; + pSopCover = Abc_SopFromTruthBin( pGateTruth ); pObj = Abc_NtkCreateNode( pNtk ); pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover ); @@ -1479,10 +1623,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, } /* output */ - if ( Abc_LitIsCompl( *p ) ) - pObj = Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ) ); - else - pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ); + pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ); Vec_PtrFree( pGates ); @@ -1513,7 +1654,7 @@ void Abc_ExactStoreTest( int fVerbose ) } Abc_NodeFreeNames( vNames ); - Abc_ExactStart( 10000, fVerbose ); + Abc_ExactStart( 10000, 1, fVerbose, NULL ); assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) ); @@ -1525,7 +1666,9 @@ void Abc_ExactStoreTest( int fVerbose ) assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) ); (*pArrTimeProfile)--; - Abc_ExactStop(); + Abc_ExactStop( NULL ); + + Abc_NtkDelete( pNtk ); } //////////////////////////////////////////////////////////////////////// |