From fd0ff0171eced62f11f9cbe67570d09e6dd22065 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 15 Feb 2013 16:47:18 -0800 Subject: Added 'gap timeout' to bmc3 and sim3. --- src/base/abci/abc.c | 78 +++++++++++++++++++++++++++++++++++------------ src/base/abci/abcDar.c | 4 +-- src/proof/ssw/ssw.h | 2 +- src/proof/ssw/sswRarity.c | 15 +++++++-- src/sat/bmc/bmc.h | 2 ++ src/sat/bmc/bmcBmc3.c | 10 ++++++ 6 files changed, 86 insertions(+), 25 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b35eab98..263de03c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17768,10 +17768,11 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) int nRestart; int nRandSeed; int TimeOut; + int TimeOutGap; int fSolveAll; int fVerbose; int fNotVerbose; - extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose ); + extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fSolveAll, int fVerbose, int fNotVerbose ); // set defaults nFrames = 20; nWords = 50; @@ -17780,12 +17781,13 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) nRestart = 100; nRandSeed = 0; TimeOut = 0; + TimeOutGap = 0; fSolveAll = 0; fVerbose = 0; fNotVerbose= 0; // parse command line Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGavzh" ) ) != EOF ) { switch ( c ) { @@ -17866,6 +17868,17 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( TimeOut < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + TimeOutGap = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOutGap < 0 ) + goto usage; + break; case 'a': fSolveAll ^= 1; break; @@ -17897,7 +17910,7 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } ABC_FREE( pNtk->pSeqModel ); - pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ); + pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fSolveAll, fVerbose, fNotVerbose ); // pAbc->nFrames = pAbc->pCex->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); if ( pNtk->vSeqModelVec ) @@ -17908,7 +17921,7 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-avzh]\n" ); + Abc_Print( -2, "usage: sim3 [-FWBRSNTG num] [-avzh]\n" ); Abc_Print( -2, "\t performs random simulation of the sequential miter\n" ); Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords ); @@ -17917,6 +17930,7 @@ usage: Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", nRestart ); Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut ); + Abc_Print( -2, "\t-G num : approximate runtime gap in seconds since the last CEX [default = %d]\n", TimeOutGap ); Abc_Print( -2, "\t-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", fNotVerbose? "yes": "no" ); @@ -20818,7 +20832,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, "SFTCDJILadruvzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTGCDJILadruvzh" ) ) != EOF ) { switch ( c ) { @@ -20855,6 +20869,17 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nTimeOut < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTimeOutGap = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOutGap < 0 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { @@ -20981,21 +21006,22 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-aduvzh]\n" ); + Abc_Print( -2, "usage: bmc3 [-SFTGCDJI num] [-L file] [-aduvzh]\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 (0 = unused) [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 : 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-F num : the max number of time frames (0 = unused) [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-G num : approximate runtime gap since the last CEX [default = %d]\n", pPars->nTimeOutGap ); + 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-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-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" ); - Abc_Print( -2, "\t-d : drops (replaces by 0) satisfiable outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" ); - Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" ); - Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); + Abc_Print( -2, "\t-d : drops (replaces by 0) satisfiable outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" ); + Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -24608,8 +24634,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) int nRestart; int nRandSeed; int TimeOut; + int TimeOutGap; int fVerbose; - extern int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fVerbose ); + extern int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fVerbose ); // set defaults nFrames = 20; nWords = 50; @@ -24618,10 +24645,11 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) nRestart = 100; nRandSeed = 0; TimeOut = 0; + TimeOutGap = 0; fVerbose = 0; // parse command line Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGvh" ) ) != EOF ) { switch ( c ) { @@ -24702,6 +24730,17 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( TimeOut < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + TimeOutGap = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOutGap < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -24716,7 +24755,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" ); return 1; } - pAbc->Status = Ssw_RarSimulateGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fVerbose ); + pAbc->Status = Ssw_RarSimulateGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fVerbose ); // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; @@ -24731,6 +24770,7 @@ usage: Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", nRestart ); Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut ); +// Abc_Print( -2, "\t-G num : approximate runtime gap in seconds since the last CEX [default = %d]\n", TimeOutGap ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 8ca40bc0..03df7fec 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3273,7 +3273,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in SeeAlso [] ***********************************************************************/ -int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose ) +int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fSolveAll, int fVerbose, int fNotVerbose ) { Aig_Man_t * pMan; int status, RetValue = -1; @@ -3284,7 +3284,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc); } pMan = Abc_NtkToDar( pNtk, 0, 1 ); - if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ) == 0 ) + if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fSolveAll, fVerbose, fNotVerbose ) == 0 ) { if ( pMan->pSeqModel ) { diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h index 4858ab89..8633835c 100644 --- a/src/proof/ssw/ssw.h +++ b/src/proof/ssw/ssw.h @@ -118,7 +118,7 @@ extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_P extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ); /*=== sswRarity.c ===================================================*/ extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); -extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose ); +extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fSolveAll, int fVerbose, int fNotVerbose ); /*=== sswSim.c ===================================================*/ extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 67501d97..1185e84d 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -941,7 +941,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose ) +int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fSolveAll, int fVerbose, int fNotVerbose ) { int fTryBmc = 0; int fMiter = 1; @@ -949,6 +949,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in int r, f = -1; clock_t clk, clkTotal = clock(); clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0; + clock_t timeLastSolved = 0; int nNumRestart = 0; int nSavedSeed = nRandSeed; int RetValue = -1; @@ -1005,6 +1006,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in Abc_PrintTime( 1, "Time", clock() - clkTotal ); goto finish; } + timeLastSolved = clock(); } // check timeout if ( TimeOut && clock() > nTimeToStop ) @@ -1014,6 +1016,13 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut ); goto finish; } + if ( TimeOutGap && timeLastSolved && clock() > timeLastSolved + TimeOutGap * CLOCKS_PER_SEC ) + { + if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); + Abc_Print( 1, "Reached gap timeout (%d sec).\n", TimeOutGap ); + goto finish; + } // check if all outputs are solved by now if ( fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 ) goto finish; @@ -1070,14 +1079,14 @@ finish: SeeAlso [] ***********************************************************************/ -int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fVerbose ) +int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fVerbose ) { int fSolveAll = 0; int fNotVerbose = 0; Aig_Man_t * pAig; int RetValue; pAig = Gia_ManToAigSimple( p ); - RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ); + RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fSolveAll, fVerbose, fNotVerbose ); // save counter-example Abc_CexFree( p->pCexSeq ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index bac4a2dd..e799bea9 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -48,6 +48,7 @@ struct Saig_ParBmc_t_ int nConfLimitJump; // maximum number of conflicts after jumping int nFramesJump; // the number of tiemframes to jump int nTimeOut; // approximate timeout in seconds + int nTimeOutGap; // approximate timeout in seconds since the last change 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 @@ -57,6 +58,7 @@ struct Saig_ParBmc_t_ int fNotVerbose; // skip line-by-line print-out int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs + clock_t timeLastSolved; // the time when the last output was solved }; diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index cd965c06..98689ff8 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1301,6 +1301,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) 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->nTimeOutGap = 0; // time since the last CEX found p->nPisAbstract = 0; // the number of PIs to abstract p->fSolveAll = 0; // stops on the first SAT instance p->fDropSatOuts = 0; // replace sat outputs by constant 0 @@ -1308,6 +1309,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) p->fNotVerbose = 0; // skip line-by-line print-out p->iFrame = -1; // explored up to this frame p->nFailOuts = 0; // the number of failed outputs + p->timeLastSolved = 0; // time when the last one was solved } /**Function************************************************************* @@ -1405,6 +1407,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Saig_Bmc3ManStop( p ); return RetValue; } + if ( pPars->nTimeOutGap && pPars->timeLastSolved && clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC ) + { + printf( "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap ); + Saig_Bmc3ManStop( p ); + return RetValue; + } // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) continue; @@ -1433,6 +1441,7 @@ clkOther += clock() - clk2; p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); RetValue = 0; + pPars->timeLastSolved = clock(); continue; } // solve th is output @@ -1507,6 +1516,7 @@ clkOther += clock() - clk2; p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); RetValue = 0; + pPars->timeLastSolved = clock(); } else { -- cgit v1.2.3