luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding parameter structure for rarity simulation.

This commit is contained in:
Alan Mishchenko 2013-04-17 19:40:02 -07:00
parent 95d9aae3e7
commit 7808ee8e70
4 changed files with 233 additions and 228 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

261
src/base/abci/abc.c
View File

@ -17902,23 +17902,12 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 fSetLastState, int fVerbose, int fNotVerbose ); extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, Ssw_RarPars_t * pPars );
Ssw_RarPars_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc); Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
Vec_Ptr_t * vSeqModelVec; 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 fSetLastState = 0;
int fVerbose = 0;
int fNotVerbose = 0;
int c; int c;
Ssw_RarSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGadivzh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGadivzh" ) ) != EOF )
{ {
@ -17930,9 +17919,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nFrames = atoi(argv[globalUtilOptind]); pPars->nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nFrames < 0 ) if ( pPars->nFrames < 0 )
goto usage; goto usage;
break; break;
case 'W': case 'W':
@ -17941,9 +17930,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nWords = atoi(argv[globalUtilOptind]); pPars->nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nWords < 0 ) if ( pPars->nWords < 0 )
goto usage; goto usage;
break; break;
case 'B': case 'B':
@ -17952,9 +17941,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nBinSize = atoi(argv[globalUtilOptind]); pPars->nBinSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nBinSize < 0 ) if ( pPars->nBinSize < 0 )
goto usage; goto usage;
break; break;
case 'R': case 'R':
@ -17963,9 +17952,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRounds = atoi(argv[globalUtilOptind]); pPars->nRounds = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRounds < 0 ) if ( pPars->nRounds < 0 )
goto usage; goto usage;
break; break;
case 'S': case 'S':
@ -17974,9 +17963,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRestart = atoi(argv[globalUtilOptind]); pPars->nRestart = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRestart < 0 ) if ( pPars->nRestart < 0 )
goto usage; goto usage;
break; break;
case 'N': case 'N':
@ -17985,9 +17974,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRandSeed = atoi(argv[globalUtilOptind]); pPars->nRandSeed = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRandSeed < 0 ) if ( pPars->nRandSeed < 0 )
goto usage; goto usage;
break; break;
case 'T': case 'T':
@ -17996,9 +17985,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
TimeOut = atoi(argv[globalUtilOptind]); pPars->TimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( TimeOut < 0 ) if ( pPars->TimeOut < 0 )
goto usage; goto usage;
break; break;
case 'G': case 'G':
@ -18007,25 +17996,25 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
TimeOutGap = atoi(argv[globalUtilOptind]); pPars->TimeOutGap = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( TimeOutGap < 0 ) if ( pPars->TimeOutGap < 0 )
goto usage; goto usage;
break; break;
case 'a': case 'a':
fSolveAll ^= 1; pPars->fSolveAll ^= 1;
break; break;
case 'd': case 'd':
fDropSatOuts ^= 1; pPars->fDropSatOuts ^= 1;
break; break;
case 'i': case 'i':
fSetLastState ^= 1; pPars->fSetLastState ^= 1;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
case 'z': case 'z':
fNotVerbose ^= 1; pPars->fNotVerbose ^= 1;
break; break;
case 'h': case 'h':
goto usage; goto usage;
@ -18049,10 +18038,10 @@ 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, TimeOutGap, fSolveAll, fSetLastState, fVerbose, fNotVerbose ); pAbc->Status = Abc_NtkDarSeqSim3( pNtk, pPars );
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
vSeqModelVec = pNtk->vSeqModelVec; pNtk->vSeqModelVec = NULL; vSeqModelVec = pNtk->vSeqModelVec; pNtk->vSeqModelVec = NULL;
if ( fSetLastState && pAbc->pNtkCur->pData ) if ( pPars->fSetLastState && pAbc->pNtkCur->pData )
{ {
Abc_Obj_t * pObj; Abc_Obj_t * pObj;
Vec_Int_t * vInit = (Vec_Int_t *)pAbc->pNtkCur->pData; Vec_Int_t * vInit = (Vec_Int_t *)pAbc->pNtkCur->pData;
@ -18070,7 +18059,7 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
} }
if ( fSolveAll && fDropSatOuts ) if ( pPars->fSolveAll && pPars->fDropSatOuts )
{ {
if ( vSeqModelVec == NULL ) if ( vSeqModelVec == NULL )
Abc_Print( 1,"The array of counter-examples is not available.\n" ); Abc_Print( 1,"The array of counter-examples is not available.\n" );
@ -18079,7 +18068,7 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
else else
{ {
extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose ); extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose );
Abc_NtkDropSatOutputs( pNtk, vSeqModelVec, fVerbose ); Abc_NtkDropSatOutputs( pNtk, vSeqModelVec, pPars->fVerbose );
pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 ); pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 );
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
@ -18099,19 +18088,19 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
Abc_Print( -2, "usage: sim3 [-FWBRSNTG num] [-advzh]\n" ); Abc_Print( -2, "usage: sim3 [-FWBRSNTG num] [-advzh]\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", pPars->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", pPars->nWords );
Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize ); Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", pPars->nBinSize );
Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", nRounds ); Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", nRestart ); Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", pPars->nRestart );
Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", pPars->nRandSeed );
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", pPars->TimeOut );
Abc_Print( -2, "\t-G num : approximate runtime gap in seconds since the last CEX [default = %d]\n", TimeOutGap ); Abc_Print( -2, "\t-G num : approximate runtime gap in seconds since the last CEX [default = %d]\n", pPars->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-a : toggle solving all outputs (do not stop when one is SAT) [default = %s]\n", pPars->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-d : toggle dropping (replacing by 0) SAT outputs [default = %s]\n", pPars->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-i : toggle changing init state to a last rare state [default = %s]\n", pPars->fVerbose? "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", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", fNotVerbose? "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;
} }
@ -24906,27 +24895,10 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars );
Ssw_RarPars_t Pars, * pPars = &Pars;
int c; int c;
int nFrames; Ssw_RarSetDefaultParams( pPars );
int nWords;
int nBinSize;
int nRounds;
int nRestart;
int nRandSeed;
int TimeOut;
int TimeOutGap;
int fVerbose;
extern int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fVerbose );
// set defaults
nFrames = 20;
nWords = 50;
nBinSize = 8;
nRounds = 0;
nRestart = 0;
nRandSeed = 0;
TimeOut = 0;
TimeOutGap = 0;
fVerbose = 0;
// parse command line // parse command line
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTGvh" ) ) != EOF )
@ -24939,9 +24911,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nFrames = atoi(argv[globalUtilOptind]); pPars->nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nFrames < 0 ) if ( pPars->nFrames < 0 )
goto usage; goto usage;
break; break;
case 'W': case 'W':
@ -24950,9 +24922,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nWords = atoi(argv[globalUtilOptind]); pPars->nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nWords < 0 ) if ( pPars->nWords < 0 )
goto usage; goto usage;
break; break;
case 'B': case 'B':
@ -24961,9 +24933,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nBinSize = atoi(argv[globalUtilOptind]); pPars->nBinSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nBinSize < 0 ) if ( pPars->nBinSize < 0 )
goto usage; goto usage;
break; break;
case 'R': case 'R':
@ -24972,9 +24944,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRounds = atoi(argv[globalUtilOptind]); pPars->nRounds = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRounds < 0 ) if ( pPars->nRounds < 0 )
goto usage; goto usage;
break; break;
case 'S': case 'S':
@ -24983,9 +24955,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRestart = atoi(argv[globalUtilOptind]); pPars->nRestart = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRestart < 0 ) if ( pPars->nRestart < 0 )
goto usage; goto usage;
break; break;
case 'N': case 'N':
@ -24994,9 +24966,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRandSeed = atoi(argv[globalUtilOptind]); pPars->nRandSeed = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRandSeed < 0 ) if ( pPars->nRandSeed < 0 )
goto usage; goto usage;
break; break;
case 'T': case 'T':
@ -25005,9 +24977,9 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
TimeOut = atoi(argv[globalUtilOptind]); pPars->TimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( TimeOut < 0 ) if ( pPars->TimeOut < 0 )
goto usage; goto usage;
break; break;
case 'G': case 'G':
@ -25016,13 +24988,13 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
TimeOutGap = atoi(argv[globalUtilOptind]); pPars->TimeOutGap = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( TimeOutGap < 0 ) if ( pPars->TimeOutGap < 0 )
goto usage; goto usage;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
case 'h': case 'h':
goto usage; goto usage;
@ -25035,7 +25007,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" );
return 1; return 1;
} }
pAbc->Status = Ssw_RarSimulateGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, TimeOutGap, fVerbose ); pAbc->Status = Ssw_RarSimulateGia( pAbc->pGia, pPars );
// pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0; return 0;
@ -25043,15 +25015,14 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-vh]\n" ); Abc_Print( -2, "usage: &sim3 [-FWBRNT num] [-vh]\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", pPars->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", pPars->nWords );
Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize ); Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", pPars->nBinSize );
Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", nRounds ); Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", nRestart ); Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", pPars->nRestart );
Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", pPars->nRandSeed );
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", pPars->TimeOut );
// Abc_Print( -2, "\t-G num : approximate runtime gap in seconds since the last CEX [default = %d]\n", TimeOutGap ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
@ -25480,23 +25451,12 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
// extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, Ssw_RarPars_t * pPars );
extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); Ssw_RarPars_t Pars, * pPars = &Pars;
int c; int c;
int nFrames = 20; Ssw_RarSetDefaultParams( pPars );
int nWords = 50;
int nBinSize = 8;
int nRounds = 0;
int nRestart = 0;
int nRandSeed = 0;
int TimeOut = 0;
int fMiter = 0;
int fUseCex = 0;
int fLatchOnly = 0;
int fNewAlgo = 1;
int fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTmxlavh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTmxlvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -25506,9 +25466,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nFrames = atoi(argv[globalUtilOptind]); pPars->nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nFrames < 0 ) if ( pPars->nFrames < 0 )
goto usage; goto usage;
break; break;
case 'W': case 'W':
@ -25517,9 +25477,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nWords = atoi(argv[globalUtilOptind]); pPars->nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nWords < 0 ) if ( pPars->nWords < 0 )
goto usage; goto usage;
break; break;
case 'B': case 'B':
@ -25528,9 +25488,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nBinSize = atoi(argv[globalUtilOptind]); pPars->nBinSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nBinSize < 0 ) if ( pPars->nBinSize < 0 )
goto usage; goto usage;
break; break;
case 'R': case 'R':
@ -25539,9 +25499,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRounds = atoi(argv[globalUtilOptind]); pPars->nRounds = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRounds < 0 ) if ( pPars->nRounds < 0 )
goto usage; goto usage;
break; break;
case 'S': case 'S':
@ -25550,9 +25510,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRestart = atoi(argv[globalUtilOptind]); pPars->nRestart = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRestart < 0 ) if ( pPars->nRestart < 0 )
goto usage; goto usage;
break; break;
case 'N': case 'N':
@ -25561,9 +25521,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nRandSeed = atoi(argv[globalUtilOptind]); pPars->nRandSeed = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nRandSeed < 0 ) if ( pPars->nRandSeed < 0 )
goto usage; goto usage;
break; break;
case 'T': case 'T':
@ -25572,25 +25532,22 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
TimeOut = atoi(argv[globalUtilOptind]); pPars->TimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( TimeOut < 0 ) if ( pPars->TimeOut < 0 )
goto usage; goto usage;
break; break;
case 'm': case 'm':
fMiter ^= 1; pPars->fMiter ^= 1;
break; break;
case 'x': case 'x':
fUseCex ^= 1; pPars->fUseCex ^= 1;
break; break;
case 'l': case 'l':
fLatchOnly ^= 1; pPars->fLatchOnly ^= 1;
break;
case 'a':
fNewAlgo ^= 1;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
case 'h': case 'h':
goto usage; goto usage;
@ -25608,12 +25565,12 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "Abc_CommandAbc9Equiv3(): There is no flops. Nothing is done.\n" ); Abc_Print( 0, "Abc_CommandAbc9Equiv3(): There is no flops. Nothing is done.\n" );
return 0; return 0;
} }
if ( fUseCex ) if ( pPars->fUseCex )
{ {
if ( fMiter ) if ( pPars->fMiter )
{ {
Abc_Print( 0, "Abc_CommandAbc9Equiv3(): Considering the miter as a circuit because the CEX is given.\n" ); Abc_Print( 0, "Abc_CommandAbc9Equiv3(): Considering the miter as a circuit because the CEX is given.\n" );
fMiter = 0; pPars->fMiter = 0;
} }
if ( pAbc->pCex == NULL ) if ( pAbc->pCex == NULL )
{ {
@ -25626,11 +25583,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->pCex->nPis, Gia_ManPiNum(pAbc->pGia) ); pAbc->pCex->nPis, Gia_ManPiNum(pAbc->pGia) );
return 1; return 1;
} }
pPars->pCex = pAbc->pCex;
} }
// if ( fNewAlgo ) pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, pPars );
pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
// else
// pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
// pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0; return 0;
@ -25638,18 +25593,16 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
Abc_Print( -2, "usage: &equiv3 [-FWRSNT num] [-mxlvh]\n" ); Abc_Print( -2, "usage: &equiv3 [-FWRSNT num] [-mxlvh]\n" );
Abc_Print( -2, "\t computes candidate equivalence classes\n" ); Abc_Print( -2, "\t computes candidate equivalence classes\n" );
Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFrames ); Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", pPars->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", pPars->nWords );
// Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize ); Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", pPars->nRounds );
Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", nRounds ); Abc_Print( -2, "\t-S num : the number of rounds before a restart [default = %d]\n", pPars->nRestart );
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", pPars->nRandSeed );
Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", nRandSeed ); Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", pPars->TimeOut );
Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeOut ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fMiter? "miter": "circuit" );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", fMiter? "miter": "circuit" ); Abc_Print( -2, "\t-x : toggle using the current CEX to perform refinement [default = %s]\n", pPars->fUseCex? "yes": "no" );
Abc_Print( -2, "\t-x : toggle using the current CEX to perform refinement [default = %s]\n", fUseCex? "yes": "no" ); Abc_Print( -2, "\t-l : toggle considering only latch output equivalences [default = %s]\n", pPars->fLatchOnly? "yes": "no" );
Abc_Print( -2, "\t-l : toggle considering only latch output equivalences [default = %s]\n", fLatchOnly? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-a : toggle using a new algorithm [default = %s]\n", fNewAlgo? "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"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }

4
src/base/abci/abcDar.c
View File

@ -3299,7 +3299,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 TimeOutGap, int fSolveAll, int fSetLastState, int fVerbose, int fNotVerbose ) int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, Ssw_RarPars_t * pPars )
{ {
Aig_Man_t * pMan; Aig_Man_t * pMan;
int status, RetValue = -1; 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); 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, TimeOutGap, fSolveAll, fSetLastState, fVerbose, fNotVerbose ) == 0 ) if ( Ssw_RarSimulate( pMan, pPars ) == 0 )
{ {
if ( pMan->pSeqModel ) if ( pMan->pSeqModel )
{ {

27
src/proof/ssw/ssw.h
View File

@ -86,6 +86,28 @@ struct Ssw_Pars_t_
void * pFunc; void * pFunc;
}; };
typedef struct Ssw_RarPars_t_ Ssw_RarPars_t;
struct Ssw_RarPars_t_
{
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 fDropSatOuts;
int fMiter;
int fUseCex;
int fLatchOnly;
Abc_Cex_t * pCex;
};
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -117,8 +139,9 @@ extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec
extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
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 void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p );
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 ); extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars );
extern int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars );
/*=== 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 );

169
src/proof/ssw/sswRarity.c
View File

@ -91,6 +91,35 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 6
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p )
{
memset( p, 0, sizeof(Ssw_RarPars_t) );
p->nFrames = 20;
p->nWords = 50;
p->nBinSize = 8;
p->nRounds = 0;
p->nRestart = 0;
p->nRandSeed = 0;
p->TimeOut = 0;
p->TimeOutGap = 0;
p->fSolveAll = 0;
p->fDropSatOuts = 0;
p->fSetLastState = 0;
p->fVerbose = 0;
p->fNotVerbose = 0;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prepares random number generator.] Synopsis [Prepares random number generator.]
@ -943,17 +972,17 @@ 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 TimeOutGap, int fSolveAll, int fSetLastState, int fVerbose, int fNotVerbose ) int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
{ {
int fTryBmc = 0; int fTryBmc = 0;
int fMiter = 1; int fMiter = 1;
Ssw_RarMan_t * p; Ssw_RarMan_t * p;
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 = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + clock(): 0;
clock_t timeLastSolved = 0; clock_t timeLastSolved = 0;
int nNumRestart = 0; int nNumRestart = 0;
int nSavedSeed = nRandSeed; int nSavedSeed = pPars->nRandSeed;
int RetValue = -1; int RetValue = -1;
int iFrameFail = -1; int iFrameFail = -1;
int nSolved = 0; int nSolved = 0;
@ -966,19 +995,19 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// check trivially SAT miters // check trivially SAT miters
// if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) ) // if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
// return 0; // return 0;
if ( fVerbose ) if ( pPars->fVerbose )
Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n", Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRestart, nRandSeed, TimeOut ); pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRestart, pPars->nRandSeed, pPars->TimeOut );
// reset random numbers // reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed ); Ssw_RarManPrepareRandom( nSavedSeed );
// create manager // create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p = Ssw_RarManStart( pAig, pPars->nWords, pPars->nFrames, pPars->nBinSize, pPars->fVerbose );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * pPars->nWords );
// perform simulation rounds // perform simulation rounds
timeLastSolved = clock(); timeLastSolved = clock();
for ( r = 0; !nRounds || (nNumRestart * nRestart + r < nRounds); r++ ) for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
{ {
clk = clock(); clk = clock();
if ( fTryBmc ) if ( fTryBmc )
@ -990,20 +1019,20 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
Aig_ManStop( pNewAig ); Aig_ManStop( pNewAig );
} }
// simulate // simulate
for ( f = 0; f < nFrames; f++ ) for ( f = 0; f < pPars->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, fSolveAll ? &nSolved : NULL, r * p->nFrames + f, fNotVerbose, clock() - clkTotal) ) if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, pPars->fSolveAll ? &nSolved : NULL, r * p->nFrames + f, pPars->fNotVerbose, clock() - clkTotal) )
{ {
RetValue = 0; RetValue = 0;
if ( !fSolveAll ) if ( !pPars->fSolveAll )
{ {
if ( fVerbose ) Abc_Print( 1, "\n" ); if ( pPars->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 );
Ssw_RarManPrepareRandom( nSavedSeed ); Ssw_RarManPrepareRandom( nSavedSeed );
if ( fVerbose ) if ( pPars->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", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
// 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 );
@ -1012,31 +1041,31 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
timeLastSolved = clock(); timeLastSolved = clock();
} }
// check timeout // check timeout
if ( TimeOut && clock() > nTimeToStop ) if ( pPars->TimeOut && clock() > nTimeToStop )
{ {
if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" ); if ( pPars->fVerbose && !pPars->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, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut ); Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
goto finish; goto finish;
} }
if ( TimeOutGap && timeLastSolved && clock() > timeLastSolved + TimeOutGap * CLOCKS_PER_SEC ) if ( pPars->TimeOutGap && timeLastSolved && clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
{ {
if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" ); if ( pPars->fVerbose && !pPars->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, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached gap timeout (%d sec).\n", TimeOutGap ); Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap );
goto finish; goto finish;
} }
// check if all outputs are solved by now // check if all outputs are solved by now
if ( fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 ) if ( pPars->fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
goto finish; goto finish;
} }
// get initialization patterns // get initialization patterns
if ( nRestart && r == nRestart ) if ( pPars->nRestart && r == pPars->nRestart )
{ {
r = -1; r = -1;
nSavedSeed = (nSavedSeed + 1) % 1000; nSavedSeed = (nSavedSeed + 1) % 1000;
Ssw_RarManPrepareRandom( nSavedSeed ); Ssw_RarManPrepareRandom( nSavedSeed );
Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * nWords, 0 ); Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
nNumRestart++; nNumRestart++;
Vec_IntClear( p->vPatBests ); Vec_IntClear( p->vPatBests );
// clean rarity info // clean rarity info
@ -1045,13 +1074,13 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
else else
Ssw_RarTransferPatterns( p, p->vInits ); Ssw_RarTransferPatterns( p, p->vInits );
// printout // printout
if ( fVerbose ) if ( pPars->fVerbose )
{ {
if ( fSolveAll ) if ( pPars->fSolveAll )
{ {
Abc_Print( 1, "Starts =%6d ", nNumRestart ); Abc_Print( 1, "Starts =%6d ", nNumRestart );
Abc_Print( 1, "Rounds =%6d ", nNumRestart * nRestart + ((r==-1)?0:r) ); Abc_Print( 1, "Rounds =%6d ", nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
Abc_Print( 1, "Frames =%6d ", (nNumRestart * nRestart + r) * nFrames ); Abc_Print( 1, "Frames =%6d ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
Abc_Print( 1, "CEX =%6d (%6.2f %%) ", nSolved, 100.0*nSolved/Saig_ManPoNum(p->pAig) ); Abc_Print( 1, "CEX =%6d (%6.2f %%) ", nSolved, 100.0*nSolved/Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", clock() - clkTotal ); Abc_PrintTime( 1, "Time", clock() - clkTotal );
} }
@ -1061,7 +1090,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
} }
finish: finish:
if ( fSetLastState && p->vInits ) if ( pPars->fSetLastState && p->vInits )
{ {
assert( Vec_IntSize(p->vInits) % Aig_ManRegNum(pAig) == 0 ); assert( Vec_IntSize(p->vInits) % Aig_ManRegNum(pAig) == 0 );
Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) ); Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) );
@ -1069,14 +1098,14 @@ finish:
} }
if ( nSolved ) if ( nSolved )
{ {
if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" ); if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
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_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->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 == pPars->nRounds && f == pPars->nFrames )
{ {
if ( fVerbose ) Abc_Print( 1, "\n" ); if ( pPars->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 ); Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", clock() - clkTotal ); Abc_PrintTime( 1, "Time", clock() - clkTotal );
} }
// cleanup // cleanup
@ -1096,14 +1125,14 @@ finish:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int TimeOutGap, int fVerbose ) int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
{ {
int fSolveAll = 0; int fSolveAll = 0;
int fNotVerbose = 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, TimeOutGap, fSolveAll, 0, fVerbose, fNotVerbose ); RetValue = Ssw_RarSimulate( pAig, pPars );
// 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;
@ -1122,14 +1151,14 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, in
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
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 ) int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
{ {
Ssw_RarMan_t * p; Ssw_RarMan_t * p;
int r, f = -1, i, k; int r, f = -1, i, k;
clock_t clkTotal = clock(); clock_t clkTotal = clock();
clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0; clock_t nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + clock(): 0;
int nNumRestart = 0; int nNumRestart = 0;
int nSavedSeed = nRandSeed; int nSavedSeed = pPars->nRandSeed;
int RetValue = -1; int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 ); assert( Aig_ManConstrNum(pAig) == 0 );
@ -1137,45 +1166,45 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
if ( Aig_ManNodeNum(pAig) == 0 ) if ( Aig_ManNodeNum(pAig) == 0 )
return -1; return -1;
// check trivially SAT miters // check trivially SAT miters
if ( fMiter && Ssw_RarCheckTrivial( pAig, 1 ) ) if ( pPars->fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
return 0; return 0;
if ( fVerbose ) if ( pPars->fVerbose )
Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut ); pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRandSeed, pPars->TimeOut );
// reset random numbers // reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed ); Ssw_RarManPrepareRandom( nSavedSeed );
// create manager // create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p = Ssw_RarManStart( pAig, pPars->nWords, pPars->nFrames, pPars->nBinSize, pPars->fVerbose );
// compute starting state if needed // compute starting state if needed
assert( p->vInits == NULL ); assert( p->vInits == NULL );
if ( pCex ) if ( pPars->pCex )
{ {
p->vInits = Ssw_RarFindStartingState( pAig, pCex ); p->vInits = Ssw_RarFindStartingState( pAig, pPars->pCex );
Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" ); Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" );
} }
else else
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
// duplicate the array // duplicate the array
for ( i = 1; i < nWords; i++ ) for ( i = 1; i < pPars->nWords; i++ )
for ( k = 0; k < Aig_ManRegNum(pAig); k++ ) for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) ); Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords ); assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * pPars->nWords );
// create trivial equivalence classes with all nodes being candidates for constant 1 // create trivial equivalence classes with all nodes being candidates for constant 1
if ( pAig->pReprs == NULL ) if ( pAig->pReprs == NULL )
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 ); p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchOnly, 0 );
else else
p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig ); p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual ); Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
// print the stats // print the stats
if ( fVerbose ) if ( pPars->fVerbose )
{ {
Abc_Print( 1, "Initial : " ); Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 ); Ssw_ClassesPrint( p->ppClasses, 0 );
} }
// refine classes using BMC // refine classes using BMC
for ( r = 0; !nRounds || (nNumRestart * nRestart + r < nRounds); r++ ) for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
{ {
// start filtering equivalence classes // start filtering equivalence classes
if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 ) if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
@ -1184,16 +1213,16 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
break; break;
} }
// simulate // simulate
for ( f = 0; f < nFrames; f++ ) for ( f = 0; f < pPars->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, NULL, -1, -1, 0) ) if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, NULL, -1, -1, 0) )
{ {
if ( !fVerbose ) if ( !pPars->fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
// 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 * pPars->nFrames, (r+1) * pPars->nFrames );
if ( fVerbose ) if ( pPars->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", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Ssw_RarManPrepareRandom( nSavedSeed ); Ssw_RarManPrepareRandom( nSavedSeed );
Abc_CexFree( pAig->pSeqModel ); Abc_CexFree( pAig->pSeqModel );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 );
@ -1204,21 +1233,21 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
goto finish; goto finish;
} }
// check timeout // check timeout
if ( TimeOut && clock() > nTimeToStop ) if ( pPars->TimeOut && clock() > nTimeToStop )
{ {
if ( fVerbose ) Abc_Print( 1, "\n" ); if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut ); Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
goto finish; goto finish;
} }
} }
// get initialization patterns // get initialization patterns
if ( pCex == NULL && nRestart && r == nRestart ) if ( pPars->pCex == NULL && pPars->nRestart && r == pPars->nRestart )
{ {
r = -1; r = -1;
nSavedSeed = (nSavedSeed + 1) % 1000; nSavedSeed = (nSavedSeed + 1) % 1000;
Ssw_RarManPrepareRandom( nSavedSeed ); Ssw_RarManPrepareRandom( nSavedSeed );
Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * nWords, 0 ); Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
nNumRestart++; nNumRestart++;
Vec_IntClear( p->vPatBests ); Vec_IntClear( p->vPatBests );
// clean rarity info // clean rarity info
@ -1227,7 +1256,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
else else
Ssw_RarTransferPatterns( p, p->vInits ); Ssw_RarTransferPatterns( p, p->vInits );
// printout // printout
if ( fVerbose ) if ( pPars->fVerbose )
{ {
Abc_Print( 1, "Round %3d: ", r ); Abc_Print( 1, "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 ); Ssw_ClassesPrint( p->ppClasses, 0 );
@ -1239,11 +1268,11 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
} }
finish: finish:
// report // report
if ( r == nRounds && f == nFrames ) if ( r == pPars->nRounds && f == pPars->nFrames )
{ {
if ( !fVerbose ) if ( !pPars->fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart ); Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", clock() - clkTotal ); Abc_PrintTime( 1, "Time", clock() - clkTotal );
} }
// cleanup // cleanup
@ -1262,7 +1291,7 @@ finish:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) int Ssw_RarSignalFilterGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
{ {
Aig_Man_t * pAig; Aig_Man_t * pAig;
int RetValue; int RetValue;
@ -1273,7 +1302,7 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize
ABC_FREE( p->pReprs ); ABC_FREE( p->pReprs );
ABC_FREE( p->pNexts ); ABC_FREE( p->pNexts );
} }
RetValue = Ssw_RarSignalFilter( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose ); RetValue = Ssw_RarSignalFilter( pAig, pPars );
Gia_ManReprFromAigRepr( pAig, p ); Gia_ManReprFromAigRepr( pAig, p );
// save counter-example // save counter-example
Abc_CexFree( p->pCexSeq ); Abc_CexFree( p->pCexSeq );