summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/base/abci/abcDar.c4
-rw-r--r--src/proof/ssw/ssw.h2
-rw-r--r--src/proof/ssw/sswRarity.c66
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 19:31:34 +0000