summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c75
-rw-r--r--src/base/abci/abcDar.c5
-rw-r--r--src/proof/ssw/ssw.h2
-rw-r--r--src/proof/ssw/sswRarity.c16
4 files changed, 69 insertions, 29 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b913e04e..27792c98 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6581,12 +6581,16 @@ int Abc_CommandDropSat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes = NULL;
+ int fNoSweep = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
{
switch ( c )
{
+ case 's':
+ fNoSweep ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -6616,18 +6620,22 @@ int Abc_CommandDropSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
Abc_NtkDropSatOutputs( pNtk, pAbc->vCexVec, fVerbose );
- pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 );
- if ( pNtkRes == NULL )
+ if ( !fNoSweep )
{
- Abc_Print( -1, "Removing SAT outputs has failed.\n" );
- return 1;
+ pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 );
+ if ( pNtkRes == NULL )
+ {
+ Abc_Print( -1, "Removing SAT outputs has failed.\n" );
+ return 1;
+ }
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
- Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
- Abc_Print( -2, "usage: dropsat [-h]\n" );
+ Abc_Print( -2, "usage: dropsat [-sh]\n" );
Abc_Print( -2, "\t replaces satisfiable POs by constant 0 and cleans up the AIG\n" );
+ Abc_Print( -2, "\t-s : toggles skipping sequential sweep [default = %s]\n", fNoSweep? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -17897,24 +17905,25 @@ usage:
***********************************************************************/
int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, 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 TimeOutGap, int fSolveAll, int fSetLastState, int fVerbose, int fNotVerbose );
Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
Vec_Ptr_t * vSeqModelVec;
- int nFrames = 20;
- int nWords = 50;
- int nBinSize = 8;
- int nRounds = 0;
- int nRestart = 0;
- int nRandSeed = 0;
- int TimeOut = 0;
- int TimeOutGap = 0;
- int fSolveAll = 0;
- int fDropSatOuts = 0;
- int fVerbose = 0;
- int fNotVerbose = 0;
+ int nFrames = 20;
+ int nWords = 50;
+ int nBinSize = 8;
+ int nRounds = 0;
+ int nRestart = 0;
+ int nRandSeed = 0;
+ int TimeOut = 0;
+ int TimeOutGap = 0;
+ int fSolveAll = 0;
+ int fDropSatOuts = 0;
+ int fSetLastState = 0;
+ int fVerbose = 0;
+ int fNotVerbose = 0;
int c;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGadvzh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGadivzh" ) ) != EOF )
{
switch ( c )
{
@@ -18012,6 +18021,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDropSatOuts ^= 1;
break;
+ case 'i':
+ fSetLastState ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -18040,9 +18052,27 @@ 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, TimeOutGap, fSolveAll, fVerbose, fNotVerbose );
+ pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fSolveAll, fSetLastState, fVerbose, fNotVerbose );
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
vSeqModelVec = pNtk->vSeqModelVec; pNtk->vSeqModelVec = NULL;
+ if ( fSetLastState && pAbc->pNtkCur->pData )
+ {
+ Abc_Obj_t * pObj;
+ Vec_Int_t * vInit = (Vec_Int_t *)pAbc->pNtkCur->pData;
+ pAbc->pNtkCur->pData = NULL;
+ Abc_NtkForEachLatch( pAbc->pNtkCur, pObj, c )
+ if ( Vec_IntEntry(vInit, c) )
+ Abc_LatchSetInit1( pObj );
+ Vec_IntFree( vInit );
+ pNtkRes = Abc_NtkRestrashZero( pAbc->pNtkCur, 0 );
+ if ( pNtkRes == NULL )
+ {
+ Abc_Print( -1, "Removing SAT outputs has failed.\n" );
+ return 1;
+ }
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ pNtk = Abc_FrameReadNtk(pAbc);
+ }
if ( fSolveAll && fDropSatOuts )
{
if ( vSeqModelVec == NULL )
@@ -18082,6 +18112,7 @@ usage:
Abc_Print( -2, "\t-G num : approximate runtime gap in seconds since the last CEX [default = %d]\n", TimeOutGap );
Abc_Print( -2, "\t-a : toggle solving all outputs (do not stop when one is SAT) [default = %s]\n", fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dropping (replacing by 0) SAT outputs [default = %s]\n", fDropSatOuts? "yes": "no" );
+ Abc_Print( -2, "\t-i : toggle changing init state to a last rare state [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");
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 28b95b95..3f7771bf 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3299,7 +3299,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 TimeOutGap, int fSolveAll, int fVerbose, int fNotVerbose )
+int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fSolveAll, int fSetLastState, int fVerbose, int fNotVerbose )
{
Aig_Man_t * pMan;
int status, RetValue = -1;
@@ -3310,7 +3310,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, TimeOutGap, fSolveAll, fVerbose, fNotVerbose ) == 0 )
+ if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fSolveAll, fSetLastState, fVerbose, fNotVerbose ) == 0 )
{
if ( pMan->pSeqModel )
{
@@ -3334,6 +3334,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
// ABC_PRT( "Time", clock() - clk );
+ pNtk->pData = pMan->pData; pMan->pData = NULL;
Aig_ManStop( pMan );
return RetValue;
}
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index 8633835c..fd6fb13d 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 TimeOutGap, int fSolveAll, int fVerbose, int fNotVerbose );
+extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fSolveAll, int fSetLastState, int fVerbose, int fNotVerbose );
/*=== 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 85ba67d5..3a7a67bd 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -591,8 +591,8 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFr
(*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 );
+ assert( Vec_PtrEntry(p->vCexes, i) == NULL );
+ Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
// print final report
if ( !fNotVerbose )
{
@@ -657,6 +657,8 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
Flip1 = Aig_ObjFaninC1(pObj) ? ~(word)0 : 0;
for ( w = 0; w < p->nWords; w++ )
pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
+
+
if ( !fUpdate )
continue;
// check classes
@@ -941,7 +943,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 TimeOutGap, int fSolveAll, int fVerbose, int fNotVerbose )
+int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fSolveAll, int fSetLastState, int fVerbose, int fNotVerbose )
{
int fTryBmc = 0;
int fMiter = 1;
@@ -1059,6 +1061,12 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
}
finish:
+ if ( fSetLastState && p->vInits )
+ {
+ assert( Vec_IntSize(p->vInits) % Aig_ManRegNum(pAig) == 0 );
+ Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) );
+ pAig->pData = p->vInits; p->vInits = NULL;
+ }
if ( nSolved )
{
if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" );
@@ -1095,7 +1103,7 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, in
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
- RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fSolveAll, fVerbose, fNotVerbose );
+ RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fSolveAll, 0, fVerbose, fNotVerbose );
// 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-05 06:01:48 +0000