Skip to content

A
abc
Commit 48fce794 by Alan Mishchenko
Options

Updating 'sim3' to move the design into the last rare state.

parent 2c275b8c
Showing with 52 additions and 12 deletions
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,6 +6620,8 @@ int Abc_CommandDropSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
Abc_NtkDropSatOutputs( pNtk, pAbc->vCexVec, fVerbose );
if ( !fNoSweep )
{
pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 );
if ( pNtkRes == NULL )
{
......@@ -6623,11 +6629,13 @@ int Abc_CommandDropSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
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,7 +17905,7 @@ 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;
......@@ -17910,11 +17918,12 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
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");
......
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;
}
......
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 );
......
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;
......
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