From 68636887891036a2ebd77fa0397afd7da91a551a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 23 Jan 2013 12:37:44 +0700 Subject: Enabled detecting CEXes in multiple POs without stopping (sim3 -a). --- src/base/abci/abc.c | 49 +++++++++++++++++++++++++++++++++++++++++-------- src/base/abci/abcDar.c | 7 +++++-- 2 files changed, 46 insertions(+), 10 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c53133d1..56aaed9e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2301,10 +2301,24 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->vCexVec ) { Abc_Cex_t * pTemp; + int nCexes = 0; + int Counter = 0; printf( "\n" ); Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c ) + { + if ( pTemp == (void *)(ABC_PTRINT_T)1 ) + { + Counter++; + continue; + } if ( pTemp ) + { + printf( "%4d : ", ++nCexes ); Abc_CexPrintStats( pTemp ); + } + } + if ( Counter ) + printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) ); } } return 0; @@ -17749,7 +17763,8 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 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 ); // set defaults nFrames = 20; nWords = 50; @@ -17760,9 +17775,10 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) TimeOut = 0; fSolveAll = 0; fVerbose = 0; + fNotVerbose= 0; // parse command line Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavzh" ) ) != EOF ) { switch ( c ) { @@ -17849,6 +17865,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'z': + fNotVerbose ^= 1; + break; case 'h': goto usage; default: @@ -17866,13 +17885,18 @@ 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 ); + pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ); // pAbc->nFrames = pAbc->pCex->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + if ( pNtk->vSeqModelVec ) + { + Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + pAbc->nFrames = -1; + } return 0; usage: - Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-avh]\n" ); + Abc_Print( -2, "usage: sim3 [-FWBRSNT 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 ); @@ -17883,6 +17907,7 @@ usage: 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-z : toggle suppressing report about solved outputs [default = %s]\n", fNotVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -20781,7 +20806,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, "SFTCDJILadruvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILadruvzh" ) ) != EOF ) { switch ( c ) { @@ -20883,6 +20908,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': pPars->fVerbose ^= 1; break; + case 'z': + pPars->fNotVerbose ^= 1; + break; case 'h': goto usage; default: @@ -20941,7 +20969,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-aduvh]\n" ); + Abc_Print( -2, "usage: bmc3 [-SFTCDJI 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 ); @@ -20955,6 +20983,7 @@ usage: 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; } @@ -22337,7 +22366,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwzh" ) ) != EOF ) { switch ( c ) { @@ -22433,6 +22462,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'w': pPars->fVeryVerbose ^= 1; break; + case 'z': + pPars->fNotVerbose ^= 1; + break; case 'h': default: goto usage; @@ -22465,7 +22497,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCRTfSkipGeneral? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "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; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 424ab14c..8ca40bc0 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 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 ) { 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 ) == 0 ) + if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ) == 0 ) { if ( pMan->pSeqModel ) { @@ -3304,6 +3304,9 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, // Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ", // nFrames, nWords ); } + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; // ABC_PRT( "Time", clock() - clk ); Aig_ManStop( pMan ); return RetValue; -- cgit v1.2.3