Skip to content

A
abc
Commit 68636887 by Alan Mishchenko
Options

Enabled detecting CEXes in multiple POs without stopping (sim3 -a).

parent ac1207ab
Showing with 103 additions and 44 deletions
src/base/abci/abc.c
...@@ -2301,10 +2301,24 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2301,10 +2301,24 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->vCexVec ) if ( pAbc->vCexVec )
{ {
Abc_Cex_t * pTemp; Abc_Cex_t * pTemp;
int nCexes = 0;
int Counter = 0;
printf( "\n" ); printf( "\n" );
Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c ) Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
{
if ( pTemp == (void *)(ABC_PTRINT_T)1 )
{
Counter++;
continue;
}
if ( pTemp ) if ( pTemp )
{
printf( "%4d : ", ++nCexes );
Abc_CexPrintStats( pTemp ); 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; return 0;
...@@ -17749,7 +17763,8 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17749,7 +17763,8 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
int TimeOut; int TimeOut;
int fSolveAll; int fSolveAll;
int fVerbose; 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 // set defaults
nFrames = 20; nFrames = 20;
nWords = 50; nWords = 50;
...@@ -17760,9 +17775,10 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17760,9 +17775,10 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
TimeOut = 0; TimeOut = 0;
fSolveAll = 0; fSolveAll = 0;
fVerbose = 0; fVerbose = 0;
fNotVerbose= 0;
// parse command line // parse command line
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavzh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -17849,6 +17865,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17849,6 +17865,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
case 'z':
fNotVerbose ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -17866,13 +17885,18 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -17866,13 +17885,18 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
ABC_FREE( pNtk->pSeqModel ); 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; // pAbc->nFrames = pAbc->pCex->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pNtk->vSeqModelVec )
{
Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
pAbc->nFrames = -1;
}
return 0; return 0;
usage: 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 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-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 ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
...@@ -17883,6 +17907,7 @@ usage: ...@@ -17883,6 +17907,7 @@ usage:
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut ); 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-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-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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -20781,7 +20806,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -20781,7 +20806,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Saig_ParBmcSetDefaultParams( pPars ); Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILadruvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILadruvzh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -20883,6 +20908,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -20883,6 +20908,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v': case 'v':
pPars->fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
case 'z':
pPars->fNotVerbose ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -20941,7 +20969,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -20941,7 +20969,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: 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 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-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-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
...@@ -20955,6 +20983,7 @@ usage: ...@@ -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-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-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-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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
...@@ -22337,7 +22366,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22337,7 +22366,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Pdr_ManSetDefaultParams( pPars ); Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwzh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -22433,6 +22462,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22433,6 +22462,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'w': case 'w':
pPars->fVeryVerbose ^= 1; pPars->fVeryVerbose ^= 1;
break; break;
case 'z':
pPars->fNotVerbose ^= 1;
break;
case 'h': case 'h':
default: default:
goto usage; goto usage;
...@@ -22465,7 +22497,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -22465,7 +22497,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwh]\n" ); Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" ); Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
...@@ -22483,6 +22515,7 @@ usage: ...@@ -22483,6 +22515,7 @@ usage:
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" ); Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "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-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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
......
src/base/abci/abcDar.c
...@@ -3273,7 +3273,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in ...@@ -3273,7 +3273,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
SeeAlso [] 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; Aig_Man_t * pMan;
int status, RetValue = -1; int status, RetValue = -1;
...@@ -3284,7 +3284,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, ...@@ -3284,7 +3284,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc); Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
} }
pMan = Abc_NtkToDar( pNtk, 0, 1 ); 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 ) if ( pMan->pSeqModel )
{ {
...@@ -3304,6 +3304,9 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, ...@@ -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. ", // Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
// nFrames, nWords ); // nFrames, nWords );
} }
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
// ABC_PRT( "Time", clock() - clk ); // ABC_PRT( "Time", clock() - clk );
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return RetValue; return RetValue;
......
src/misc/vec/vecPtr.h
...@@ -554,7 +554,8 @@ static inline void Vec_PtrFreeFree( Vec_Ptr_t * p ) ...@@ -554,7 +554,8 @@ static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
int i; int i;
if ( p == NULL ) return; if ( p == NULL ) return;
Vec_PtrForEachEntry( void *, p, pTemp, i ) Vec_PtrForEachEntry( void *, p, pTemp, i )
ABC_FREE( pTemp ); if ( pTemp != (void *)(ABC_PTRINT_T)1 && pTemp != (void *)(ABC_PTRINT_T)2 )
ABC_FREE( pTemp );
Vec_PtrFree( p ); Vec_PtrFree( p );
} }
......
src/proof/pdr/pdr.h
...@@ -53,6 +53,7 @@ struct Pdr_Par_t_ ...@@ -53,6 +53,7 @@ struct Pdr_Par_t_
int fSkipGeneral; // skips expensive generalization step int fSkipGeneral; // skips expensive generalization step
int fVerbose; // verbose output` int fVerbose; // verbose output`
int fVeryVerbose; // very verbose output int fVeryVerbose; // very verbose output
int fNotVerbose; // not printing line by line progress
int fSilent; // totally silent execution int fSilent; // totally silent execution
int fSolveAll; // do not stop when found a SAT output int fSolveAll; // do not stop when found a SAT output
int nFailOuts; // the number of failed outputs int nFailOuts; // the number of failed outputs
......
src/proof/pdr/pdrCore.c
...@@ -57,6 +57,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) ...@@ -57,6 +57,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->fShortest = 0; // forces bug traces to be shortest pPars->fShortest = 0; // forces bug traces to be shortest
pPars->fVerbose = 0; // verbose output pPars->fVerbose = 0; // verbose output
pPars->fVeryVerbose = 0; // very verbose output pPars->fVeryVerbose = 0; // very verbose output
pPars->fNotVerbose = 0; // not printing line-by-line progress
pPars->iFrame = -1; // explored up to this frame pPars->iFrame = -1; // explored up to this frame
} }
...@@ -645,8 +646,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) ...@@ -645,8 +646,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
pCex = Pdr_ManDeriveCex(p); pCex = Pdr_ManDeriveCex(p);
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex );
Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", if ( !p->pPars->fNotVerbose )
nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT return 0; // all SAT
Pdr_QueueClean( p ); Pdr_QueueClean( p );
......
src/proof/ssw/ssw.h
...@@ -118,7 +118,7 @@ extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_P ...@@ -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 ); extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
/*=== sswRarity.c ===================================================*/ /*=== 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_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 ); 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 );
/*=== sswSim.c ===================================================*/ /*=== sswSim.c ===================================================*/
extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); 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 ); extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
......
src/proof/ssw/sswRarity.c
...@@ -546,7 +546,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) ...@@ -546,7 +546,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p ) int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
...@@ -556,12 +556,33 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p ) ...@@ -556,12 +556,33 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
{ {
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs ) if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
return 0; return 0;
if ( Vec_PtrEntry(p->vCexes, i) ) if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue; continue;
if ( !Ssw_RarManObjIsConst(p, pObj) ) if ( !Ssw_RarManObjIsConst(p, pObj) )
{ {
p->iFailPo = i; p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj ); p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
// remember the one solved
if ( pnSolvedNow )
{
(*pnSolvedNow)++;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
// print final report
if ( !fNotVerbose )
{
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
nOutDigits, p->iFailPo, iFrame,
nOutDigits, *pnSolvedNow,
nOutDigits, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Time );
}
continue;
}
return 1; return 1;
} }
} }
...@@ -697,7 +718,6 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames ...@@ -697,7 +718,6 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
p->vUpdConst = Vec_PtrAlloc( 100 ); p->vUpdConst = Vec_PtrAlloc( 100 );
p->vUpdClass = Vec_PtrAlloc( 100 ); p->vUpdClass = Vec_PtrAlloc( 100 );
p->vPatBests = Vec_IntAlloc( 100 ); p->vPatBests = Vec_IntAlloc( 100 );
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
return p; return p;
} }
...@@ -714,7 +734,13 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames ...@@ -714,7 +734,13 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
***********************************************************************/ ***********************************************************************/
static void Ssw_RarManStop( Ssw_RarMan_t * p ) static void Ssw_RarManStop( Ssw_RarMan_t * p )
{ {
Vec_PtrFreeP( &p->vCexes ); // Vec_PtrFreeP( &p->vCexes );
if ( p->vCexes )
{
assert( p->pAig->vSeqModelVec == NULL );
p->pAig->vSeqModelVec = p->vCexes;
p->vCexes = NULL;
}
if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
Vec_IntFreeP( &p->vInits ); Vec_IntFreeP( &p->vInits );
Vec_IntFreeP( &p->vPatBests ); Vec_IntFreeP( &p->vPatBests );
...@@ -897,7 +923,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose ) ...@@ -897,7 +923,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
SeeAlso [] 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 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 fTryBmc = 0; int fTryBmc = 0;
int fMiter = 1; int fMiter = 1;
...@@ -905,7 +931,6 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in ...@@ -905,7 +931,6 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
int r, f = -1; int r, f = -1;
clock_t clk, clkTotal = clock(); clock_t clk, clkTotal = clock();
clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0; clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int nNumRestart = 0; int nNumRestart = 0;
int nSavedSeed = nRandSeed; int nSavedSeed = nRandSeed;
int RetValue = -1; int RetValue = -1;
...@@ -913,6 +938,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in ...@@ -913,6 +938,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
int nSolved = 0; int nSolved = 0;
assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 ); assert( Aig_ManConstrNum(pAig) == 0 );
ABC_FREE( pAig->pSeqModel );
// consider the case of empty AIG // consider the case of empty AIG
if ( Aig_ManNodeNum(pAig) == 0 ) if ( Aig_ManNodeNum(pAig) == 0 )
return -1; return -1;
...@@ -945,13 +971,13 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in ...@@ -945,13 +971,13 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
for ( f = 0; f < nFrames; f++ ) for ( f = 0; f < nFrames; f++ )
{ {
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 ); Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, fSolveAll ? &nSolved : NULL, r * p->nFrames + f, fNotVerbose, clock() - clkTotal) )
{ {
RetValue = 0;
if ( !fSolveAll ) if ( !fSolveAll )
{ {
if ( fVerbose ) Abc_Print( 1, "\n" ); 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_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 ); Ssw_RarManPrepareRandom( nSavedSeed );
if ( fVerbose ) if ( fVerbose )
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
...@@ -959,23 +985,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in ...@@ -959,23 +985,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// print final report // 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_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 ); Abc_PrintTime( 1, "Time", clock() - clkTotal );
RetValue = 0;
goto finish; 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 // check timeout
if ( TimeOut && clock() > nTimeToStop ) if ( TimeOut && clock() > nTimeToStop )
...@@ -985,6 +996,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in ...@@ -985,6 +996,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut ); Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut );
goto finish; goto finish;
} }
// check if all outputs are solved by now
if ( fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
goto finish;
} }
// get initialization patterns // get initialization patterns
if ( nRestart && r == nRestart ) if ( nRestart && r == nRestart )
...@@ -1012,7 +1026,7 @@ finish: ...@@ -1012,7 +1026,7 @@ finish:
if ( nSolved ) if ( nSolved )
{ {
if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" ); 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_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart, nSolved, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", clock() - clkTotal ); Abc_PrintTime( 1, "Time", clock() - clkTotal );
} }
else if ( r == nRounds && f == nFrames ) else if ( r == nRounds && f == nFrames )
...@@ -1041,10 +1055,11 @@ finish: ...@@ -1041,10 +1055,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 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; int fSolveAll = 0;
int fNotVerbose = 0;
Aig_Man_t * pAig; Aig_Man_t * pAig;
int RetValue; int RetValue;
pAig = Gia_ManToAigSimple( p ); pAig = Gia_ManToAigSimple( p );
RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose ); RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose );
// save counter-example // save counter-example
Abc_CexFree( p->pCexSeq ); Abc_CexFree( p->pCexSeq );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
...@@ -1128,7 +1143,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize ...@@ -1128,7 +1143,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
for ( f = 0; f < nFrames; f++ ) for ( f = 0; f < nFrames; f++ )
{ {
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f ); Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, NULL, -1, -1, 0) )
{ {
if ( !fVerbose ) if ( !fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
......
src/sat/bmc/bmc.h
...@@ -54,6 +54,7 @@ struct Saig_ParBmc_t_ ...@@ -54,6 +54,7 @@ struct Saig_ParBmc_t_
int nFfToAddMax; // max number of flops to add during CBA int nFfToAddMax; // max number of flops to add during CBA
int fSkipRand; // skip random decisions int fSkipRand; // skip random decisions
int fVerbose; // verbose int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
int iFrame; // explored up to this frame int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs int nFailOuts; // the number of failed outputs
}; };
......
src/sat/bmc/bmcBmc3.c
...@@ -1305,6 +1305,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) ...@@ -1305,6 +1305,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->fSolveAll = 0; // stops on the first SAT instance p->fSolveAll = 0; // stops on the first SAT instance
p->fDropSatOuts = 0; // replace sat outputs by constant 0 p->fDropSatOuts = 0; // replace sat outputs by constant 0
p->fVerbose = 0; // verbose p->fVerbose = 0; // verbose
p->fNotVerbose = 0; // skip line-by-line print-out
p->iFrame = -1; // explored up to this frame p->iFrame = -1; // explored up to this frame
p->nFailOuts = 0; // the number of failed outputs p->nFailOuts = 0; // the number of failed outputs
} }
...@@ -1425,8 +1426,9 @@ clkOther += clock() - clk2; ...@@ -1425,8 +1426,9 @@ clkOther += clock() - clk2;
return 0; return 0;
} }
pPars->nFailOuts++; pPars->nFailOuts++;
Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", if ( !pPars->fNotVerbose )
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL ) if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex ); Vec_PtrWriteEntry( p->vCexes, i, pCex );
...@@ -1498,8 +1500,9 @@ clkOther += clock() - clk2; ...@@ -1498,8 +1500,9 @@ clkOther += clock() - clk2;
return 0; return 0;
} }
pPars->nFailOuts++; pPars->nFailOuts++;
Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", if ( !pPars->fNotVerbose )
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL ) if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex ); Vec_PtrWriteEntry( p->vCexes, i, pCex );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment