Skip to content

A
abc
Commit ac1207ab by Alan Mishchenko
Options

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

parent 70655d5d
Showing with 62 additions and 24 deletions
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;
......
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 )
{
......
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 );
......
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;
......
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