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

Changes to enable smarter simulation.

This commit is contained in:
Alan Mishchenko 2011-07-30 13:30:04 +07:00
parent e4f15dd003
commit 2ea0ded0bc
5 changed files with 319 additions and 82 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/ssw/ssw.h
View File

@ -119,8 +119,8 @@ extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars
extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, 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 TimeOut, int fVerbose ); extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
/*=== sswRarity2.c ===================================================*/ /*=== sswRarity2.c ===================================================*/
extern int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); extern int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); extern int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
/*=== 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 );

10
src/aig/ssw/sswRarity.c
View File

@ -261,7 +261,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
int f, i, iBit; int f, i, iBit;
// assign register outputs // assign register outputs
Saig_ManForEachLi( pAig, pObj, i ) Saig_ManForEachLi( pAig, pObj, i )
pObj->fMarkB = 0; pObj->fMarkB = Aig_InfoHasBit( pCex->pData, i );
// simulate the timeframes // simulate the timeframes
iBit = pCex->nRegs; iBit = pCex->nRegs;
for ( f = 0; f <= pCex->iFrame; f++ ) for ( f = 0; f <= pCex->iFrame; f++ )
@ -304,7 +304,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
{ {
int fMiter = 1; int fMiter = 1;
Ssw_RarMan_t * p; Ssw_RarMan_t * p;
@ -381,7 +381,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, 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 TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{ {
int fMiter = 0; int fMiter = 0;
Ssw_RarMan_t * p; Ssw_RarMan_t * p;
@ -486,7 +486,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) 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 )
{ {
Aig_Man_t * pAig; Aig_Man_t * pAig;
int RetValue; int RetValue;
@ -497,7 +497,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, TimeOut, pCex, fLatchOnly, fVerbose ); RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
Gia_ManReprFromAigRepr( pAig, p ); Gia_ManReprFromAigRepr( pAig, p );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
return RetValue; return RetValue;

169
src/aig/ssw/sswRarity2.c
View File

@ -87,6 +87,25 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 6
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prepares random number generator.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManPrepareRandom( int nRandSeed )
{
int i;
Aig_ManRandom( 1 );
for ( i = 0; i < nRandSeed; i++ )
Aig_ManRandom( 0 );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Initializes random primary inputs.] Synopsis [Initializes random primary inputs.]
@ -133,7 +152,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
// compute the pattern sequence // compute the pattern sequence
iPatThis = iPatFinal; iPatThis = iPatFinal;
vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 ); vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 );
Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatFinal ); Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis );
for ( r = iFrame / p->nFrames - 1; r >= 0; r-- ) for ( r = iFrame / p->nFrames - 1; r >= 0; r-- )
{ {
iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 ); iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 );
@ -145,7 +164,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
pCex->iPo = iPo; pCex->iPo = iPo;
// insert the bits // insert the bits
iBit = Aig_ManRegNum(p->pAig); iBit = Aig_ManRegNum(p->pAig);
for ( f = 0; f < iFrame; f++ ) for ( f = 0; f <= iFrame; f++ )
{ {
Ssw_RarManAssingRandomPis( p ); Ssw_RarManAssingRandomPis( p );
iPatThis = Vec_IntEntry( vTrace, f / p->nFrames ); iPatThis = Vec_IntEntry( vTrace, f / p->nFrames );
@ -158,6 +177,19 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
} }
} }
Vec_IntFree( vTrace ); Vec_IntFree( vTrace );
assert( iBit == pCex->nBits );
// verify the counter example
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
else
{
// printf( "Counter-example verification is successful.\n" );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
}
return pCex; return pCex;
} }
@ -383,34 +415,6 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
} }
} }
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~0 : 0;
int w, i;
for ( w = 0; w < p->nWords; w++ )
if ( pSim[w] ^ Flip )
{
for ( i = 0; i < 64; i++ )
if ( ((pSim[w] ^ Flip) >> i) & 1 )
break;
assert( i < 64 );
return w * 64 + i;
}
return -1;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.] Synopsis [Returns 1 if simulation info is composed of all zeros.]
@ -494,6 +498,34 @@ unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
return uHash; return uHash;
} }
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~0 : 0;
int w, i;
for ( w = 0; w < p->nWords; w++ )
if ( pSim[w] ^ Flip )
{
for ( i = 0; i < 64; i++ )
if ( ((pSim[w] ^ Flip) >> i) & 1 )
break;
assert( i < 64 );
return w * 64 + i;
}
return -1;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Check if any of the POs becomes non-constant.] Synopsis [Check if any of the POs becomes non-constant.]
@ -772,7 +804,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
int f, i, iBit; int f, i, iBit;
// assign register outputs // assign register outputs
Saig_ManForEachLi( pAig, pObj, i ) Saig_ManForEachLi( pAig, pObj, i )
pObj->fMarkB = 0; pObj->fMarkB = Aig_InfoHasBit( pCex->pData, i );
// simulate the timeframes // simulate the timeframes
iBit = pCex->nRegs; iBit = pCex->nRegs;
for ( f = 0; f <= pCex->iFrame; f++ ) for ( f = 0; f <= pCex->iFrame; f++ )
@ -815,7 +847,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
{ {
int fMiter = 1; int fMiter = 1;
Ssw_RarMan_t * p; Ssw_RarMan_t * p;
@ -827,10 +859,10 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
if ( Aig_ManNodeNum(pAig) == 0 ) if ( Aig_ManNodeNum(pAig) == 0 )
return -1; return -1;
if ( fVerbose ) if ( fVerbose )
printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut ); nWords, nFrames, nRounds, nRandSeed, TimeOut );
// reset random numbers // reset random numbers
Aig_ManRandom( 1 ); Ssw_RarManPrepareRandom( nRandSeed );
// create manager // create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
@ -847,7 +879,8 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{ {
if ( fVerbose ) printf( "\n" ); if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); // printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
Ssw_RarManPrepareRandom( nRandSeed );
ABC_FREE( pAig->pSeqModel ); ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
RetValue = 0; RetValue = 0;
@ -872,7 +905,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
} }
} }
finish: finish:
if ( r == nRounds ) if ( r == nRounds && f == nFrames )
{ {
if ( fVerbose ) printf( "\n" ); if ( fVerbose ) printf( "\n" );
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
@ -884,6 +917,30 @@ finish:
} }
/**Function*************************************************************
Synopsis [Perform sequential simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
{
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
RetValue = Ssw_RarSimulate2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );
// save counter-example
Abc_CexFree( p->pCexSeq );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
return RetValue;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Filter equivalence classes of nodes.] Synopsis [Filter equivalence classes of nodes.]
@ -895,9 +952,8 @@ finish:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ) int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{ {
int fMiter = 0;
Ssw_RarMan_t * p; Ssw_RarMan_t * p;
int r, f, i, k, clkTotal = clock(); int r, f, i, k, clkTotal = clock();
int RetValue = -1; int RetValue = -1;
@ -907,10 +963,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
if ( Aig_ManNodeNum(pAig) == 0 ) if ( Aig_ManNodeNum(pAig) == 0 )
return -1; return -1;
if ( fVerbose ) if ( fVerbose )
printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut ); nWords, nFrames, nRounds, nRandSeed, TimeOut );
// reset random numbers // reset random numbers
Aig_ManRandom( 1 ); Ssw_RarManPrepareRandom( nRandSeed );
// create manager // create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
@ -953,9 +1009,11 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
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) ) if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{ {
if ( fVerbose ) printf( "\n" ); if ( !fVerbose )
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); printf( "\r" );
ABC_FREE( pAig->pSeqModel ); // printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
Ssw_RarManPrepareRandom( nRandSeed );
Abc_CexFree( pAig->pSeqModel );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
RetValue = 0; RetValue = 0;
goto finish; goto finish;
@ -968,25 +1026,31 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
goto finish; goto finish;
} }
} }
// get initialization patterns
Ssw_RarTransferPatterns( p, p->vInits );
// printout // printout
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Round %3d: ", r ); printf( "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 ); Ssw_ClassesPrint( p->ppClasses, 0 );
} }
// get initialization patterns else
Ssw_RarTransferPatterns( p, p->vInits ); {
printf( "." );
}
} }
finish: finish:
// report // report
if ( r == nRounds ) if ( r == nRounds && f == nFrames )
{ {
if ( !fVerbose )
printf( "\r" );
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal ); Abc_PrintTime( 1, "Time", clock() - clkTotal );
} }
// cleanup // cleanup
Ssw_RarManStop( p ); Ssw_RarManStop( p );
return -1; return RetValue;
} }
/**Function************************************************************* /**Function*************************************************************
@ -1000,7 +1064,7 @@ finish:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
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 ) int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{ {
Aig_Man_t * pAig; Aig_Man_t * pAig;
int RetValue; int RetValue;
@ -1011,8 +1075,11 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz
ABC_FREE( p->pReprs ); ABC_FREE( p->pReprs );
ABC_FREE( p->pNexts ); ABC_FREE( p->pNexts );
} }
RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ); RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose );
Gia_ManReprFromAigRepr( pAig, p ); Gia_ManReprFromAigRepr( pAig, p );
// save counter-example
Abc_CexFree( p->pCexSeq );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig ); Aig_ManStop( pAig );
return RetValue; return RetValue;
} }

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

@ -337,6 +337,7 @@ static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sim3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Resim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SpecI ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SpecI ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -758,6 +759,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&trim", Abc_CommandAbc9Trim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dfs", Abc_CommandAbc9Dfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim", Abc_CommandAbc9Sim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sim", Abc_CommandAbc9Sim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sim3", Abc_CommandAbc9Sim3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&resim", Abc_CommandAbc9Resim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&resim", Abc_CommandAbc9Resim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&speci", Abc_CommandAbc9SpecI, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&speci", Abc_CommandAbc9SpecI, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&equiv", Abc_CommandAbc9Equiv, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&equiv", Abc_CommandAbc9Equiv, 0 );
@ -15795,19 +15797,21 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
int nWords; int nWords;
int nBinSize; int nBinSize;
int nRounds; int nRounds;
int nRandSeed;
int TimeOut; int TimeOut;
int fVerbose; int fVerbose;
extern int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
// set defaults // set defaults
nFrames = 20; nFrames = 20;
nWords = 50; nWords = 50;
nBinSize = 8; nBinSize = 8;
nRounds = 80; nRounds = 80;
nRandSeed = 0;
TimeOut = 0; TimeOut = 0;
fVerbose = 1; fVerbose = 0;
// parse command line // parse command line
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -15855,6 +15859,17 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nRounds < 0 ) if ( nRounds < 0 )
goto usage; goto usage;
break; break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nRandSeed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRandSeed < 0 )
goto usage;
break;
case 'T': case 'T':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
@ -15886,17 +15901,19 @@ 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_NtkDarSeqSim2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fVerbose ); pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );
// pAbc->nFrames = pAbc->pCex->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: sim3 [-FWBRT 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", 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", 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", 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", nRounds );
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-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
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", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
@ -24644,7 +24661,7 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Gia_ManSimSetDefaultParams( pPars ); Gia_ManSimSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWRTmvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWNTmvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -24670,10 +24687,10 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nWords < 0 ) if ( pPars->nWords < 0 )
goto usage; goto usage;
break; break;
case 'R': case 'N':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
Abc_Print( -1, "Command line switch \"-R\" 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;
} }
pPars->RandSeed = atoi(argv[globalUtilOptind]); pPars->RandSeed = atoi(argv[globalUtilOptind]);
@ -24725,12 +24742,12 @@ int Abc_CommandAbc9Sim( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &sim [-FWRT num] [-mvh]\n" ); Abc_Print( -2, "usage: &sim [-FWNT num] [-mvh]\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 (if candidate equivalences are defined, performs refinement)\n" ); Abc_Print( -2, "\t (if candidate equivalences are defined, performs refinement)\n" );
Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nIters ); Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", pPars->nIters );
Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords );
Abc_Print( -2, "\t-R num : random number seed (1 <= num <= 10000) [default = %d]\n", pPars->RandSeed ); Abc_Print( -2, "\t-N num : random number seed (1 <= num <= 1000) [default = %d]\n", pPars->RandSeed );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
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", pPars->fVerbose? "yes": "no" );
@ -24738,6 +24755,142 @@ usage:
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c;
int nFrames;
int nWords;
int nBinSize;
int nRounds;
int nRandSeed;
int TimeOut;
int fVerbose;
extern int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
// set defaults
nFrames = 20;
nWords = 50;
nBinSize = 8;
nRounds = 80;
nRandSeed = 0;
TimeOut = 0;
fVerbose = 0;
// parse command line
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nWords < 0 )
goto usage;
break;
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
nBinSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBinSize < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
nRounds = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRounds < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nRandSeed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRandSeed < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
TimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOut < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" );
return 1;
}
pAbc->Status = Ssw_RarSimulate2Gia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );
// pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
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-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 );
Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize );
Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", nRounds );
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-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -25156,21 +25309,22 @@ 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 Abc_NtkDarSeqEquiv2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); // 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, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose ); extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
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 );
int c; int c;
int nFrames = 20; int nFrames = 20;
int nWords = 50; int nWords = 50;
int nBinSize = 8; int nBinSize = 8;
int nRounds = 80; int nRounds = 80;
int nRandSeed = 0;
int TimeOut = 0; int TimeOut = 0;
int fMiter = 0;
int fUseCex = 0; int fUseCex = 0;
int fLatchOnly = 0; int fLatchOnly = 0;
int fNewAlgo = 1; int fNewAlgo = 1;
int fVerbose = 0; int fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlavh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRNTmxlavh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -25218,6 +25372,17 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nRounds < 0 ) if ( nRounds < 0 )
goto usage; goto usage;
break; break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nRandSeed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRandSeed < 0 )
goto usage;
break;
case 'T': case 'T':
if ( globalUtilOptind >= argc ) if ( globalUtilOptind >= argc )
{ {
@ -25229,6 +25394,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( TimeOut < 0 ) if ( TimeOut < 0 )
goto usage; goto usage;
break; break;
case 'm':
fMiter ^= 1;
break;
case 'x': case 'x':
fUseCex ^= 1; fUseCex ^= 1;
break; break;
@ -25266,22 +25434,24 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
} }
if ( fNewAlgo ) // if ( fNewAlgo )
pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
else // else
pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); // pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
// pAbc->nFrames = pAbc->pCex->iFrame; // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
// Abc_FrameReplaceCex( pAbc, &pAbc->pCex ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &equiv3 [-FWRT num] [-xlvh]\n" ); Abc_Print( -2, "usage: &equiv3 [-FWRNT 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", 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", 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", nBinSize );
Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", nRounds ); Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", nRounds );
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", 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", fMiter? "miter": "circuit" );
Abc_Print( -2, "\t-x : toggle using the current CEX to perform refinement [default = %s]\n", 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", fLatchOnly? "yes": "no" ); Abc_Print( -2, "\t-l : toggle considering only latch output equivalences [default = %s]\n", fLatchOnly? "yes": "no" );
Abc_Print( -2, "\t-a : toggle using a new algorithm [default = %s]\n", fNewAlgo? "yes": "no" ); Abc_Print( -2, "\t-a : toggle using a new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );

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

@ -3017,7 +3017,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NtkDarSeqSim2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ) int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
{ {
Aig_Man_t * pMan; Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock(); int status, RetValue = -1, clk = clock();
@ -3027,7 +3027,7 @@ int Abc_NtkDarSeqSim2( 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, TimeOut, fVerbose ) == 0 ) if ( Ssw_RarSimulate2( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 )
{ {
if ( pMan->pSeqModel ) if ( pMan->pSeqModel )
{ {