From ac1207abea41ad9d3dd304cdc9a10a899eb8cbcc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 23 Jan 2013 02:07:50 +0700 Subject: Enabled detecting CEXes in multiple POs without stopping (sim3 -a). --- src/base/abci/abc.c | 14 +++++++--- src/base/abci/abcDar.c | 4 +-- src/proof/ssw/ssw.h | 2 +- src/proof/ssw/sswRarity.c | 66 +++++++++++++++++++++++++++++++++++------------ 4 files changed, 62 insertions(+), 24 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0be55670..c53133d1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17747,8 +17747,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) int nRestart; int nRandSeed; int TimeOut; + int fSolveAll; int fVerbose; - extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fVerbose ); + 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 ); // set defaults nFrames = 20; nWords = 50; @@ -17757,10 +17758,11 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) nRestart = 100; nRandSeed = 0; TimeOut = 0; + fSolveAll = 0; fVerbose = 0; // parse command line Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavh" ) ) != EOF ) { switch ( c ) { @@ -17841,6 +17843,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( TimeOut < 0 ) goto usage; break; + case 'a': + fSolveAll ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -17861,13 +17866,13 @@ 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, fVerbose ); + pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose ); // pAbc->nFrames = pAbc->pCex->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); return 0; usage: - Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-vh]\n" ); + Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-avh]\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 ); @@ -17876,6 +17881,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-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-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 6e8edc99..424ab14c 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 fVerbose ) +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 ) { 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, fVerbose ) == 0 ) + if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose ) == 0 ) { if ( pMan->pSeqModel ) { diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h index df73c357..3ddcff37 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 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 ); /*=== 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 2abd9682..19dc3192 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -57,6 +57,8 @@ struct Ssw_RarMan_t_ Vec_Int_t * vPatBests; // best patterns int iFailPo; // failed primary output int iFailPat; // failed pattern + // counter-examples + Vec_Ptr_t * vCexes; }; @@ -554,6 +556,8 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p ) { if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs ) return 0; + if ( Vec_PtrEntry(p->vCexes, i) ) + continue; if ( !Ssw_RarManObjIsConst(p, pObj) ) { p->iFailPo = i; @@ -693,6 +697,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames p->vUpdConst = Vec_PtrAlloc( 100 ); p->vUpdClass = Vec_PtrAlloc( 100 ); p->vPatBests = Vec_IntAlloc( 100 ); + p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); return p; } @@ -709,6 +714,7 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames ***********************************************************************/ static void Ssw_RarManStop( Ssw_RarMan_t * p ) { + Vec_PtrFreeP( &p->vCexes ); if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); Vec_IntFreeP( &p->vInits ); Vec_IntFreeP( &p->vPatBests ); @@ -891,7 +897,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 fVerbose ) +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 fTryBmc = 0; int fMiter = 1; @@ -899,10 +905,12 @@ 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; + int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) ); int nNumRestart = 0; int nSavedSeed = nRandSeed; int RetValue = -1; int iFrameFail = -1; + int nSolved = 0; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); // consider the case of empty AIG @@ -939,23 +947,40 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 ); if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) { - if ( fVerbose ) Abc_Print( 1, "\n" ); -// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); - Ssw_RarManPrepareRandom( nSavedSeed ); - ABC_FREE( pAig->pSeqModel ); - if ( fVerbose ) - Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); - pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose ); - // print final report - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); - Abc_PrintTime( 1, "Time", clock() - clkTotal ); - RetValue = 0; - goto finish; + if ( !fSolveAll ) + { + if ( fVerbose ) Abc_Print( 1, "\n" ); + // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + ABC_FREE( pAig->pSeqModel ); + Ssw_RarManPrepareRandom( nSavedSeed ); + if ( fVerbose ) + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); + pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose ); + // print final report + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + RetValue = 0; + goto finish; + } + else + { + nSolved++; + assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL ); + Vec_PtrWriteEntry( p->vCexes, p->iFailPo, p->vCexes ); + // print final report + ABC_FREE( pAig->pSeqModel ); + Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ", + nOutDigits, p->iFailPo, r * p->nFrames + f, + nOutDigits, nSolved, nOutDigits, Saig_ManPoNum(p->pAig) ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + RetValue = 0; + } + } // check timeout if ( TimeOut && clock() > nTimeToStop ) { - if ( fVerbose ) Abc_Print( 1, "\n" ); + 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 timeout (%d sec).\n", TimeOut ); goto finish; @@ -976,7 +1001,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in else Ssw_RarTransferPatterns( p, p->vInits ); // printout - if ( fVerbose ) + if ( fVerbose && !fSolveAll ) { // Abc_Print( 1, "Round %3d: ", r ); // Abc_PrintTime( 1, "Time", clock() - clk ); @@ -984,7 +1009,13 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in } } finish: - if ( r == nRounds && f == nFrames ) + if ( nSolved ) + { + if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" ); + Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart, nSolved ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + } + else if ( r == nRounds && f == nFrames ) { if ( fVerbose ) Abc_Print( 1, "\n" ); Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); @@ -1009,10 +1040,11 @@ finish: ***********************************************************************/ int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fVerbose ) { + int fSolveAll = 0; Aig_Man_t * pAig; int RetValue; pAig = Gia_ManToAigSimple( p ); - RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fVerbose ); + RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose ); // save counter-example Abc_CexFree( p->pCexSeq ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; -- cgit v1.2.3