From d080336bb5e4508274ed03940d6c8cb6ec3a1200 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 23 Sep 2011 22:35:03 -0700 Subject: Added new feature to bmc3. --- src/aig/saig/saig.h | 25 ++++++++++++++----------- src/aig/saig/saigBmc3.c | 30 ++++++++++++++++++++++++------ src/base/abci/abc.c | 30 +++++++++++++++++++++++++++--- src/map/if/ifDec10f.c | 37 ++++++++++++++++++++++--------------- 4 files changed, 87 insertions(+), 35 deletions(-) (limited to 'src') diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 4441b923..6b85a3df 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -58,18 +58,21 @@ struct Sec_MtrStatus_t_ typedef struct Saig_ParBmc_t_ Saig_ParBmc_t; struct Saig_ParBmc_t_ { - int nStart; // starting timeframe - int nFramesMax; // maximum number of timeframes - int nConfLimit; // maximum number of conflicts at a node - int nTimeOut; // approximate timeout in seconds - int nPisAbstract; // the number of PIs to abstract - int fSolveAll; // does not stop at the first SAT output - int fDropSatOuts; // replace sat outputs by constant 0 - int nFfToAddMax; // max number of flops to add during CBA - int fVerbose; // verbose - int iFrame; // explored up to this frame - int nFailOuts; // the number of failed outputs + int nStart; // starting timeframe + int nFramesMax; // maximum number of timeframes + int nConfLimit; // maximum number of conflicts at a node + int nConfLimitJump; // maximum number of conflicts after jumping + int nFramesJump; // the number of tiemframes to jump + int nTimeOut; // approximate timeout in seconds + int nPisAbstract; // the number of PIs to abstract + int fSolveAll; // does not stop at the first SAT output + int fDropSatOuts; // replace sat outputs by constant 0 + int nFfToAddMax; // max number of flops to add during CBA + int fVerbose; // verbose + int iFrame; // explored up to this frame + int nFailOuts; // the number of failed outputs }; + typedef struct Saig_ParBbr_t_ Saig_ParBbr_t; struct Saig_ParBbr_t_ diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index f5a6234e..7248ed1a 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1073,6 +1073,8 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) p->nStart = 0; // maximum number of timeframes p->nFramesMax = 2000; // maximum number of timeframes p->nConfLimit = 2000; // maximum number of conflicts at a node + p->nConfLimitJump = 0; // maximum number of conflicts after jumping + p->nFramesJump = 0; // the number of tiemframes to jump p->nTimeOut = 0; // approximate timeout in seconds p->nPisAbstract = 0; // the number of PIs to abstract p->fSolveAll = 0; // stops on the first SAT instance @@ -1097,7 +1099,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) { Gia_ManBmc_t * p; Aig_Obj_t * pObj; - int RetValue = -1, fFirst = 1; + int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0; int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock(); if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 ) @@ -1133,7 +1135,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) return 0; } // consider the next timeframe - if ( RetValue == -1 && pPars->nStart == 0 ) + if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame ) pPars->iFrame = f-1; // resize the array Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 ); @@ -1173,7 +1175,7 @@ clkOther += clock() - clk2; return 1; } } - if ( pPars->nStart && f < pPars->nStart ) + if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) ) continue; // solve SAT clk = clock(); @@ -1211,6 +1213,7 @@ clkOther += clock() - clk2; continue; } // solve this output + fUnfinished = 0; sat_solver_compress( p->pSat ); status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_False ) @@ -1232,7 +1235,7 @@ clkOther += clock() - clk2; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { - printf( "%3d : ", f ); + printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); printf( "Var =%8.0f. ", (double)p->nSatVars ); printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); @@ -1261,6 +1264,19 @@ clkOther += clock() - clk2; else { assert( status == l_Undef ); + if ( pPars->nTimeOut && ((float)pPars->nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) + { + printf( "Reached timeout (%d seconds).\n", pPars->nTimeOut ); + Saig_Bmc3ManStop( p ); + return RetValue; + } + if ( pPars->nFramesJump ) + { + pPars->nConfLimit = pPars->nConfLimitJump; + nJumpFrame = f + pPars->nFramesJump; + fUnfinished = 1; + break; + } Saig_Bmc3ManStop( p ); return RetValue; } @@ -1278,7 +1294,7 @@ clkOther += clock() - clk2; fFirst = 0; // printf( "Outputs of frames up to %d are trivially UNSAT.\n", f ); } - printf( "%3d : ", f ); + printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); printf( "Var =%8.0f. ", (double)p->nSatVars ); printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses ); printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); @@ -1293,7 +1309,9 @@ clkOther += clock() - clk2; } } // consider the next timeframe - if ( RetValue == -1 && pPars->nStart == 0 ) + if ( nJumpFrame && pPars->nStart == 0 ) + pPars->iFrame = nJumpFrame - pPars->nFramesJump; + else if ( RetValue == -1 && pPars->nStart == 0 ) pPars->iFrame = f; //ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4cbecb4e..cbbebd1f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19017,7 +19017,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Saig_ParBmcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCILsdrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILsdrvh" ) ) != EOF ) { switch ( c ) { @@ -19065,6 +19065,28 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nConfLimit < 0 ) goto usage; break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfLimitJump = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfLimitJump < 0 ) + goto usage; + break; + case 'J': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesJump = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesJump < 0 ) + goto usage; + break; case 'I': if ( globalUtilOptind >= argc ) { @@ -19144,12 +19166,14 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc3 [-SFTCI num] [-L file] [-sdvh]\n" ); + Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-sdvh]\n" ); Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" ); Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump ); + Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump ); Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-s : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" ); diff --git a/src/map/if/ifDec10f.c b/src/map/if/ifDec10f.c index 9f30cf96..9e2126e8 100644 --- a/src/map/if/ifDec10f.c +++ b/src/map/if/ifDec10f.c @@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define CLU_MAX 16 + // the bit count for the first 256 integer numbers static int BitCount8[256] = { 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5, @@ -55,18 +57,7 @@ static word Truth6[6] = { 0xFFFF0000FFFF0000, 0xFFFFFFFF00000000 }; -static word Truth10[10][16] = { - 0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA, - 0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC, - 0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0, - 0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00, - 0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000, - 0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000, - 0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF, - 0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF, - 0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF, - 0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF -}; +static word TruthAll[CLU_MAX][1 << (CLU_MAX-6)]; extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); @@ -76,10 +67,26 @@ extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); // moving up means moving from LSB -> MSB // groups list vars indices from MSB to LSB +// group representation +// nVars | nCofs | v5 | v4 | v3 | v2 | v1 | v0 +// if nCofs > 2, v0 is the shared variable + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +void If_CluInitTruthTables() +{ + int i, k; + assert( CLU_MAX <= 16 ); + for ( i = 0; i < 6; i++ ) + for ( k = 0; k < (1 << (CLU_MAX-6)); k++ ) + TruthAll[i][k] = Truth6[i]; + for ( i = 6; i < CLU_MAX; i++ ) + for ( k = 0; k < (1 << (CLU_MAX-6)); k++ ) + TruthAll[i][k] = ((k >> i) & 1) ? ~0 : 0; +} + // variable permutation for large functions static inline int If_CluWordNum( int nVars ) { @@ -131,7 +138,7 @@ static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nV // moves one var (v) to the given position (p) void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p ) { - word pG[16], * pIn = pF, * pOut = pG, * pTemp; + word pG[32], * pIn = pF, * pOut = pG, * pTemp; int iPlace0, iPlace1, Count = 0; assert( v >= 0 && v < nVars ); assert( Var2Pla[v] >= p ); @@ -156,7 +163,7 @@ void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int // moves one var (v) to the given position (p) void If_CluMoveVarOneDown( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p ) { - word pG[16], * pIn = pF, * pOut = pG, * pTemp; + word pG[32], * pIn = pF, * pOut = pG, * pTemp; int iPlace0, iPlace1, Count = 0; assert( v >= 0 && v < nVars ); assert( Var2Pla[v] <= p ); @@ -194,7 +201,7 @@ int If_CluCountCofs( word * pF, int * V2P, int * P2V, int nVars, int nBSsize ) word iCofs[16], iCof; int i, c, nMints = (1 << nBSsize), nCofs = 1; assert( nBSsize >= 3 && nBSsize <= 5 ); - assert( nVars - nBSsize >= 0 && nVars - nBSsize <= 6 ); + assert( nVars - nBSsize > 0 && nVars - nBSsize <= 6 ); if ( nVars - nBSsize == 6 ) Mask = ~0; iCofs[0] = pF[0] & Mask; -- cgit v1.2.3