Skip to content

A
abc
Commit c60852f4 by Alan Mishchenko
Options

Changes to enable smarter simulation.

parent 2ea0ded0
Showing with 834 additions and 883 deletions
src/aig/ssw/ssw.h
...@@ -116,11 +116,8 @@ extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec ...@@ -116,11 +116,8 @@ 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 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 nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose ); extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
/*=== sswRarity2.c ===================================================*/
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 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 );
......
src/aig/ssw/sswRarity.c
...@@ -37,19 +37,27 @@ struct Ssw_RarMan_t_ ...@@ -37,19 +37,27 @@ struct Ssw_RarMan_t_
int nBinSize; // the number of flops in one group int nBinSize; // the number of flops in one group
int fVerbose; // the verbosiness flag int fVerbose; // the verbosiness flag
int nGroups; // the number of flop groups int nGroups; // the number of flop groups
int nWordsReg; // the number of words in the registers
// internal data // internal data
Aig_Man_t * pAig; // AIG with equivalence classes Aig_Man_t * pAig; // AIG with equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes
Ssw_Sml_t * pSml; // simulation manager
Vec_Ptr_t * vSimInfo; // simulation info from pSml manager
Vec_Int_t * vInits; // initial state Vec_Int_t * vInits; // initial state
// simulation data
word * pObjData; // simulation info for each obj
word * pPatData; // pattern data for each reg
// candidates to update
Vec_Ptr_t * vUpdConst; // constant 1 candidates
Vec_Ptr_t * vUpdClass; // class representatives
// rarity data // rarity data
int * pRarity; // occur counts for patterns in groups int * pRarity; // occur counts for patterns in groups
int * pGroupValues; // occur counts in each group
double * pPatCosts; // pattern costs double * pPatCosts; // pattern costs
// best patterns
Vec_Int_t * vPatBests; // best patterns
int iFailPo; // failed primary output
int iFailPat; // failed pattern
}; };
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{ {
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
...@@ -69,13 +77,19 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) ...@@ -69,13 +77,19 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
p->pRarity[iBin * (1 << p->nBinSize) + iPat]++; p->pRarity[iBin * (1 << p->nBinSize) + iPat]++;
} }
static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); }
static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id; }
static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->nWords ); return p->pPatData + p->nWordsReg * Id; }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Prepares random number generator.]
Description [] Description []
...@@ -84,29 +98,17 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) ...@@ -84,29 +98,17 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose ) void Ssw_RarManPrepareRandom( int nRandSeed )
{ {
Ssw_RarMan_t * p; int i;
if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 ) Aig_ManRandom( 1 );
return NULL; for ( i = 0; i < nRandSeed; i++ )
p = ABC_CALLOC( Ssw_RarMan_t, 1 ); Aig_ManRandom( 0 );
p->pAig = pAig;
p->nWords = nWords;
p->nFrames = nFrames;
p->nBinSize = nBinSize;
p->fVerbose = fVerbose;
p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
p->pGroupValues = ABC_CALLOC( int, p->nGroups );
p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 );
p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml );
return p;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Initializes random primary inputs.]
Description [] Description []
...@@ -115,22 +117,23 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames ...@@ -115,22 +117,23 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static void Ssw_RarManStop( Ssw_RarMan_t * p ) void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
{ {
if ( p->pSml ) Ssw_SmlStop( p->pSml ); word * pSim;
if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses ); Aig_Obj_t * pObj;
Vec_PtrFreeP( &p->vSimInfo ); int w, i;
Vec_IntFreeP( &p->vInits ); Saig_ManForEachPi( p->pAig, pObj, i )
ABC_FREE( p->pGroupValues ); {
ABC_FREE( p->pPatCosts ); pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
ABC_FREE( p->pRarity ); for ( w = 0; w < p->nWords; w++ )
ABC_FREE( p ); pSim[w] = Aig_ManRandom64(0);
pSim[0] <<= 1;
}
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Updates rarity counters.] Synopsis [Derives the counter-example.]
Description [] Description []
...@@ -139,41 +142,578 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p ) ...@@ -139,41 +142,578 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal )
{ {
Abc_Cex_t * pCex;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
unsigned * pData; Vec_Int_t * vTrace;
int i, k; word * pSim;
/* int i, r, f, iBit, iPatThis;
Saig_ManForEachLi( p->pAig, pObj, i ) // compute the pattern sequence
iPatThis = iPatFinal;
vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 );
Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis );
for ( r = iFrame / p->nFrames - 1; r >= 0; r-- )
{
iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 );
Vec_IntWriteEntry( vTrace, r, iPatThis );
}
// create counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 );
pCex->iFrame = iFrame;
pCex->iPo = iPo;
// insert the bits
iBit = Aig_ManRegNum(p->pAig);
for ( f = 0; f <= iFrame; f++ )
{
Ssw_RarManAssingRandomPis( p );
iPatThis = Vec_IntEntry( vTrace, f / p->nFrames );
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
if ( Aig_InfoHasBit( (unsigned *)pSim, iPatThis ) )
Aig_InfoSetBit( pCex->pData, iBit );
iBit++;
}
}
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;
}
/**Function*************************************************************
Synopsis [Transposing 32-bit matrix.]
Description [Borrowed from "Hacker's Delight", by Henry Warren.]
SideEffects []
SeeAlso []
***********************************************************************/
void transpose32( unsigned A[32] )
{
int j, k;
unsigned t, m = 0x0000FFFF;
for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
{ {
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); for ( k = 0; k < 32; k = (k + j + 1) & ~j )
Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" ); {
t = (A[k] ^ (A[k+j] >> j)) & m;
A[k] = A[k] ^ t;
A[k+j] = A[k+j] ^ (t << j);
}
} }
}
/**Function*************************************************************
Synopsis [Transposing 64-bit matrix.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void transpose64( word A[64] )
{
int j, k;
word t, m = 0x00000000FFFFFFFF;
for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 64; k = (k + j + 1) & ~j )
{
t = (A[k] ^ (A[k+j] >> j)) & m;
A[k] = A[k] ^ t;
A[k+j] = A[k+j] ^ (t << j);
}
}
}
/**Function*************************************************************
Synopsis [Transposing 64-bit matrix.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void transpose64Simple( word A[64], word B[64] )
{
int i, k;
for ( i = 0; i < 64; i++ )
B[i] = 0;
for ( i = 0; i < 64; i++ )
for ( k = 0; k < 64; k++ )
if ( (A[i] >> k) & 1 )
B[k] |= ((word)1 << (63-i));
}
/**Function*************************************************************
Synopsis [Testing the transposing code.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void TransposeTest()
{
word M[64], N[64];
int i, clk;
Aig_ManRandom64( 1 );
// for ( i = 0; i < 64; i++ )
// M[i] = Aig_ManRandom64( 0 );
for ( i = 0; i < 64; i++ )
M[i] = i? (word)0 : ~(word)0;
// for ( i = 0; i < 64; i++ )
// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
clk = clock();
for ( i = 0; i < 100001; i++ )
transpose64Simple( M, N );
Abc_PrintTime( 1, "Time", clock() - clk );
clk = clock();
for ( i = 0; i < 100001; i++ )
transpose64( M );
Abc_PrintTime( 1, "Time", clock() - clk );
for ( i = 0; i < 64; i++ )
if ( M[i] != N[i] )
printf( "Mismatch\n" );
/*
printf( "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
printf( "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" );
*/ */
for ( k = 0; k < p->nWords * 32; k++ ) }
/**Function*************************************************************
Synopsis [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarTranspose( Ssw_RarMan_t * p )
{
Aig_Obj_t * pObj;
word M[64];
int w, r, i;
for ( w = 0; w < p->nWords; w++ )
for ( r = 0; r < p->nWordsReg; r++ )
{ {
for ( i = 0; i < p->nGroups; i++ ) // save input
p->pGroupValues[i] = 0; for ( i = 0; i < 64; i++ )
Saig_ManForEachLi( p->pAig, pObj, i )
{ {
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) )
if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups ) {
p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize)); pObj = Saig_ManLi( p->pAig, r*64 + 63-i );
M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w];
} }
for ( i = 0; i < p->nGroups; i++ ) else
Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] ); M[i] = 0;
}
// transpose
transpose64( M );
// save output
for ( i = 0; i < 64; i++ )
Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i];
} }
/* /*
for ( i = 0; i < p->nGroups; i++ ) Saig_ManForEachLi( p->pAig, pObj, i )
{ {
for ( k = 0; k < (1 << p->nBinSize); k++ ) word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
printf( "%d ", Ssw_RarGetBinPat(p, i, k) ); Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" );
}
printf( "\n" ); printf( "\n" );
for ( i = 0; i < p->nWords*64; i++ )
{
word * pBitData = Ssw_RarPatSim( p, i );
Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" );
} }
printf( "\n" );
*/ */
} }
/**Function*************************************************************
Synopsis [Sets random inputs and specialied flop outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
{
Aig_Obj_t * pObj, * pObjLi;
word * pSim, * pSimLi;
int w, i;
// constant
pObj = Aig_ManConst1( p->pAig );
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = ~(word)0;
// primary inputs
Ssw_RarManAssingRandomPis( p );
// flop outputs
if ( vInit )
{
assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords );
Saig_ManForEachLo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
}
}
else
{
Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
{
pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) );
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = pSimLi[w];
}
}
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~0 : 0;
int w;
for ( w = 0; w < p->nWords; w++ )
if ( pSim[w] ^ Flip )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjsAreEqual( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~0 : 0;
int w;
for ( w = 0; w < p->nWords; w++ )
if ( pSim0[w] ^ pSim1[w] ^ Flip )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
unsigned uHash;
int i;
uHash = 0;
pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
for ( i = 0; i < 2 * p->nWords; i++ )
uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
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*************************************************************
Synopsis [Check if any of the POs becomes non-constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
{
Aig_Obj_t * pObj;
int i;
p->iFailPo = -1;
p->iFailPat = -1;
Saig_ManForEachPo( p->pAig, pObj, i )
{
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
return 0;
if ( !Ssw_RarManObjIsConst(p, pObj) )
{
p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
return 1;
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Performs one round of simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
{
Aig_Obj_t * pObj, * pRepr;
word * pSim, * pSim0, * pSim1;
word Flip, Flip0, Flip1;
int w, i;
// initialize
Ssw_RarManInitialize( p, vInit );
Vec_PtrClear( p->vUpdConst );
Vec_PtrClear( p->vUpdClass );
Aig_ManIncrementTravId( p->pAig );
// check comb inputs
if ( fUpdate )
Aig_ManForEachPi( p->pAig, pObj, i )
{
pRepr = Aig_ObjRepr(p->pAig, pObj);
if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
continue;
if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
continue;
// save for update
if ( pRepr == Aig_ManConst1(p->pAig) )
Vec_PtrPush( p->vUpdConst, pObj );
else
{
Vec_PtrPush( p->vUpdClass, pRepr );
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
// simulate
Aig_ManForEachNode( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
Flip0 = Aig_ObjFaninC0(pObj) ? ~0 : 0;
Flip1 = Aig_ObjFaninC1(pObj) ? ~0 : 0;
for ( w = 0; w < p->nWords; w++ )
pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
if ( !fUpdate )
continue;
// check classes
pRepr = Aig_ObjRepr(p->pAig, pObj);
if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
continue;
if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
continue;
// save for update
if ( pRepr == Aig_ManConst1(p->pAig) )
Vec_PtrPush( p->vUpdConst, pObj );
else
{
Vec_PtrPush( p->vUpdClass, pRepr );
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
// transfer to POs
Aig_ManForEachPo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
Flip = Aig_ObjFaninC0(pObj) ? ~0 : 0;
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Flip ^ pSim0[w];
}
// refine classes
if ( fUpdate )
{
if ( fFirst )
{
Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 );
Aig_ManForEachObj( p->pAig, pObj, i )
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
Vec_PtrPush( vCands, pObj );
assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) );
Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 );
Vec_PtrFree( vCands );
}
else
{
Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
{
Ssw_RarMan_t * p;
if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
return NULL;
p = ABC_CALLOC( Ssw_RarMan_t, 1 );
p->pAig = pAig;
p->nWords = nWords;
p->nFrames = nFrames;
p->nBinSize = nBinSize;
p->fVerbose = fVerbose;
p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 );
p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords );
p->pPatData = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg );
p->vUpdConst = Vec_PtrAlloc( 100 );
p->vUpdClass = Vec_PtrAlloc( 100 );
p->vPatBests = Vec_IntAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ssw_RarManStop( Ssw_RarMan_t * p )
{
if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
Vec_IntFreeP( &p->vInits );
Vec_IntFreeP( &p->vPatBests );
Vec_PtrFreeP( &p->vUpdConst );
Vec_PtrFreeP( &p->vUpdClass );
ABC_FREE( p->pObjData );
ABC_FREE( p->pPatData );
ABC_FREE( p->pPatCosts );
ABC_FREE( p->pRarity );
ABC_FREE( p );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Select best patterns.] Synopsis [Select best patterns.]
...@@ -187,32 +727,36 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p ) ...@@ -187,32 +727,36 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
***********************************************************************/ ***********************************************************************/
static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
{ {
Aig_Obj_t * pObj; // Aig_Obj_t * pObj;
unsigned * pData; unsigned char * pData;
unsigned * pPattern;
int i, k, Value; int i, k, Value;
// for each pattern // more data from regs to pats
for ( k = 0; k < p->nWords * 32; k++ ) Ssw_RarTranspose( p );
// update counters
for ( k = 0; k < p->nWords * 64; k++ )
{ {
pData = (unsigned char *)Ssw_RarPatSim( p, k );
for ( i = 0; i < p->nGroups; i++ ) for ( i = 0; i < p->nGroups; i++ )
p->pGroupValues[i] = 0; Ssw_RarAddToBinPat( p, i, pData[i] );
// compute its group values
Saig_ManForEachLi( p->pAig, pObj, i )
{
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
} }
// for each pattern
for ( k = 0; k < p->nWords * 64; k++ )
{
pData = (unsigned char *)Ssw_RarPatSim( p, k );
// find the cost of its values // find the cost of its values
p->pPatCosts[k] = 0.0; p->pPatCosts[k] = 0.0;
for ( i = 0; i < p->nGroups; i++ ) for ( i = 0; i < p->nGroups; i++ )
{ {
Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] ); Value = Ssw_RarGetBinPat( p, i, pData[i] );
assert( Value > 0 ); assert( Value > 0 );
p->pPatCosts[k] += 1.0/(Value*Value); p->pPatCosts[k] += 1.0/(Value*Value);
} }
// print the result // print the result
// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); //printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
} }
// choose as many as there are words // choose as many as there are words
...@@ -222,7 +766,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) ...@@ -222,7 +766,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
// select the best // select the best
int iPatBest = -1; int iPatBest = -1;
double iCostBest = -ABC_INFINITY; double iCostBest = -ABC_INFINITY;
for ( k = 0; k < p->nWords * 32; k++ ) for ( k = 0; k < p->nWords * 64; k++ )
if ( iCostBest < p->pPatCosts[k] ) if ( iCostBest < p->pPatCosts[k] )
{ {
iCostBest = p->pPatCosts[k]; iCostBest = p->pPatCosts[k];
...@@ -232,12 +776,11 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) ...@@ -232,12 +776,11 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
assert( iPatBest >= 0 ); assert( iPatBest >= 0 );
p->pPatCosts[iPatBest] = -ABC_INFINITY; p->pPatCosts[iPatBest] = -ABC_INFINITY;
// set the flops // set the flops
Saig_ManForEachLi( p->pAig, pObj, k ) pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
{ for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1); Vec_IntPush( vInits, Aig_InfoHasBit(pPattern, k) );
Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) );
}
//printf( "Best pattern %5d\n", iPatBest ); //printf( "Best pattern %5d\n", iPatBest );
Vec_IntPush( p->vPatBests, iPatBest );
} }
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
} }
...@@ -304,11 +847,11 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ...@@ -304,11 +847,11 @@ 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_RarSimulate( 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;
int r, clk, clkTotal = clock(); int r, f, clk, clkTotal = clock();
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 );
...@@ -316,33 +859,43 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i ...@@ -316,33 +859,43 @@ 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 );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// perform simulation rounds // perform simulation rounds
for ( r = 0; r < nRounds; r++ ) for ( r = 0; r < nRounds; r++ )
{ {
clk = clock(); clk = clock();
// simulate // simulate
Ssw_SmlSimulateOne( p->pSml ); for ( f = 0; f < nFrames; f++ )
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) ) {
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
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 );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
RetValue = 0; RetValue = 0;
break; goto finish;
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
goto finish;
}
} }
// get initialization patterns // get initialization patterns
Ssw_RarUpdateCounters( p );
Ssw_RarTransferPatterns( p, p->vInits ); Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// printout // printout
if ( fVerbose ) if ( fVerbose )
{ {
...@@ -350,15 +903,9 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i ...@@ -350,15 +903,9 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
// Abc_PrintTime( 1, "Time", clock() - clk ); // Abc_PrintTime( 1, "Time", clock() - clk );
printf( "." ); printf( "." );
} }
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
break;
}
} }
if ( r == nRounds ) finish:
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 );
...@@ -372,6 +919,30 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i ...@@ -372,6 +919,30 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
/**Function************************************************************* /**Function*************************************************************
Synopsis [Perform sequential simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSimulateGia( 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_RarSimulate( 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*************************************************************
Synopsis [Filter equivalence classes of nodes.] Synopsis [Filter equivalence classes of nodes.]
Description [] Description []
...@@ -381,11 +952,10 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i ...@@ -381,11 +952,10 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
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_RarSignalFilter( 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, i, k, clkTotal = clock(); int r, f, i, k, clkTotal = clock();
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 );
...@@ -393,10 +963,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ...@@ -393,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 );
...@@ -411,15 +981,13 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ...@@ -411,15 +981,13 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
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) * nWords );
// initialize simulation manager
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// 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, fLatchOnly, 0 );
else else
p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig ); p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
Ssw_ClassesSetData( p->ppClasses, p->pSml, NULL, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
// print the stats // print the stats
if ( fVerbose ) if ( fVerbose )
{ {
...@@ -436,43 +1004,53 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ...@@ -436,43 +1004,53 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
break; break;
} }
// simulate // simulate
Ssw_SmlSimulateOne( p->pSml ); for ( f = 0; f < nFrames; f++ )
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
{ {
if ( fVerbose ) printf( "\n" ); Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( !fVerbose )
printf( "\r" );
// 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 );
RetValue = 0; RetValue = 0;
break; goto finish;
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
goto finish;
}
} }
// check equivalence classes // get initialization patterns
Ssw_ClassesRefineConst1( p->ppClasses, 1 ); Ssw_RarTransferPatterns( p, p->vInits );
Ssw_ClassesRefine( p->ppClasses, 1 );
// 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_RarUpdateCounters( p );
Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{ {
if ( fVerbose ) printf( "\n" ); printf( "." );
printf( "Reached timeout (%d seconds).\n", TimeOut );
break;
} }
} }
if ( r == nRounds ) finish:
// report
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*************************************************************
...@@ -486,7 +1064,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ...@@ -486,7 +1064,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
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_RarSignalFilterGia( 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;
...@@ -497,15 +1075,16 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz ...@@ -497,15 +1075,16 @@ 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_RarSignalFilter( 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;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/ssw/sswRarity2.c
...@@ -37,26 +37,18 @@ struct Ssw_RarMan_t_ ...@@ -37,26 +37,18 @@ struct Ssw_RarMan_t_
int nBinSize; // the number of flops in one group int nBinSize; // the number of flops in one group
int fVerbose; // the verbosiness flag int fVerbose; // the verbosiness flag
int nGroups; // the number of flop groups int nGroups; // the number of flop groups
int nWordsReg; // the number of words in the registers
// internal data // internal data
Aig_Man_t * pAig; // AIG with equivalence classes Aig_Man_t * pAig; // AIG with equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes
Ssw_Sml_t * pSml; // simulation manager
Vec_Ptr_t * vSimInfo; // simulation info from pSml manager
Vec_Int_t * vInits; // initial state Vec_Int_t * vInits; // initial state
// simulation data
word * pObjData; // simulation info for each obj
word * pPatData; // pattern data for each reg
// candidates to update
Vec_Ptr_t * vUpdConst; // constant 1 candidates
Vec_Ptr_t * vUpdClass; // class representatives
// rarity data // rarity data
int * pRarity; // occur counts for patterns in groups int * pRarity; // occur counts for patterns in groups
int * pGroupValues; // occur counts in each group
double * pPatCosts; // pattern costs double * pPatCosts; // pattern costs
// best patterns
Vec_Int_t * vPatBests; // best patterns
int iFailPo; // failed primary output
int iFailPat; // failed pattern
};
};
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{ {
...@@ -77,152 +69,13 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) ...@@ -77,152 +69,13 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
p->pRarity[iBin * (1 << p->nBinSize) + iPat]++; p->pRarity[iBin * (1 << p->nBinSize) + iPat]++;
} }
static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); }
static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id; }
static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->nWords ); return p->pPatData + p->nWordsReg * Id; }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function************************************************************* /**Function*************************************************************
Synopsis [Prepares random number generator.] Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManPrepareRandom( int nRandSeed )
{
int i;
Aig_ManRandom( 1 );
for ( i = 0; i < nRandSeed; i++ )
Aig_ManRandom( 0 );
}
/**Function*************************************************************
Synopsis [Initializes random primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
{
word * pSim;
Aig_Obj_t * pObj;
int w, i;
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Aig_ManRandom64(0);
pSim[0] <<= 1;
}
}
/**Function*************************************************************
Synopsis [Derives the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
Vec_Int_t * vTrace;
word * pSim;
int i, r, f, iBit, iPatThis;
// compute the pattern sequence
iPatThis = iPatFinal;
vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 );
Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis );
for ( r = iFrame / p->nFrames - 1; r >= 0; r-- )
{
iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 );
Vec_IntWriteEntry( vTrace, r, iPatThis );
}
// create counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 );
pCex->iFrame = iFrame;
pCex->iPo = iPo;
// insert the bits
iBit = Aig_ManRegNum(p->pAig);
for ( f = 0; f <= iFrame; f++ )
{
Ssw_RarManAssingRandomPis( p );
iPatThis = Vec_IntEntry( vTrace, f / p->nFrames );
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
if ( Aig_InfoHasBit( (unsigned *)pSim, iPatThis ) )
Aig_InfoSetBit( pCex->pData, iBit );
iBit++;
}
}
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;
}
/**Function*************************************************************
Synopsis [Transposing 32-bit matrix.]
Description [Borrowed from "Hacker's Delight", by Henry Warren.]
SideEffects []
SeeAlso []
***********************************************************************/
void transpose32( unsigned A[32] )
{
int j, k;
unsigned t, m = 0x0000FFFF;
for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 32; k = (k + j + 1) & ~j )
{
t = (A[k] ^ (A[k+j] >> j)) & m;
A[k] = A[k] ^ t;
A[k+j] = A[k+j] ^ (t << j);
}
}
}
/**Function*************************************************************
Synopsis [Transposing 64-bit matrix.]
Description [] Description []
...@@ -231,24 +84,29 @@ void transpose32( unsigned A[32] ) ...@@ -231,24 +84,29 @@ void transpose32( unsigned A[32] )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void transpose64( word A[64] ) static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
{ {
int j, k; Ssw_RarMan_t * p;
word t, m = 0x00000000FFFFFFFF; if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) return NULL;
{ p = ABC_CALLOC( Ssw_RarMan_t, 1 );
for ( k = 0; k < 64; k = (k + j + 1) & ~j ) p->pAig = pAig;
{ p->nWords = nWords;
t = (A[k] ^ (A[k+j] >> j)) & m; p->nFrames = nFrames;
A[k] = A[k] ^ t; p->nBinSize = nBinSize;
A[k+j] = A[k+j] ^ (t << j); p->fVerbose = fVerbose;
} p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
} p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
p->pGroupValues = ABC_CALLOC( int, p->nGroups );
p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 );
p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml );
return p;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Transposing 64-bit matrix.] Synopsis []
Description [] Description []
...@@ -257,66 +115,22 @@ void transpose64( word A[64] ) ...@@ -257,66 +115,22 @@ void transpose64( word A[64] )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void transpose64Simple( word A[64], word B[64] ) static void Ssw_RarManStop( Ssw_RarMan_t * p )
{ {
int i, k; if ( p->pSml ) Ssw_SmlStop( p->pSml );
for ( i = 0; i < 64; i++ ) if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
B[i] = 0; Vec_PtrFreeP( &p->vSimInfo );
for ( i = 0; i < 64; i++ ) Vec_IntFreeP( &p->vInits );
for ( k = 0; k < 64; k++ ) ABC_FREE( p->pGroupValues );
if ( (A[i] >> k) & 1 ) ABC_FREE( p->pPatCosts );
B[k] |= ((word)1 << (63-i)); ABC_FREE( p->pRarity );
ABC_FREE( p );
} }
/**Function*************************************************************
Synopsis [Testing the transposing code.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void TransposeTest()
{
word M[64], N[64];
int i, clk;
Aig_ManRandom64( 1 );
// for ( i = 0; i < 64; i++ )
// M[i] = Aig_ManRandom64( 0 );
for ( i = 0; i < 64; i++ )
M[i] = i? (word)0 : ~(word)0;
// for ( i = 0; i < 64; i++ )
// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
clk = clock();
for ( i = 0; i < 100001; i++ )
transpose64Simple( M, N );
Abc_PrintTime( 1, "Time", clock() - clk );
clk = clock();
for ( i = 0; i < 100001; i++ )
transpose64( M );
Abc_PrintTime( 1, "Time", clock() - clk );
for ( i = 0; i < 64; i++ )
if ( M[i] != N[i] )
printf( "Mismatch\n" );
/*
printf( "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
printf( "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" );
*/
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].] Synopsis [Updates rarity counters.]
Description [] Description []
...@@ -325,393 +139,39 @@ void TransposeTest() ...@@ -325,393 +139,39 @@ void TransposeTest()
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Ssw_RarTranspose( Ssw_RarMan_t * p ) static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
{ {
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
word M[64]; unsigned * pData;
int w, r, i; int i, k;
for ( w = 0; w < p->nWords; w++ )
for ( r = 0; r < p->nWordsReg; r++ )
{
// save input
for ( i = 0; i < 64; i++ )
{
if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) )
{
pObj = Saig_ManLi( p->pAig, r*64 + 63-i );
M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w];
}
else
M[i] = 0;
}
// transpose
transpose64( M );
// save output
for ( i = 0; i < 64; i++ )
Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i];
}
/* /*
Saig_ManForEachLi( p->pAig, pObj, i ) Saig_ManForEachLi( p->pAig, pObj, i )
{ {
word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" ); Extra_PrintBinary( stdout, pData, 32 ); printf( "\n" );
}
printf( "\n" );
for ( i = 0; i < p->nWords*64; i++ )
{
word * pBitData = Ssw_RarPatSim( p, i );
Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" );
} }
printf( "\n" );
*/ */
} for ( k = 0; k < p->nWords * 32; k++ )
/**Function*************************************************************
Synopsis [Sets random inputs and specialied flop outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
{
Aig_Obj_t * pObj, * pObjLi;
word * pSim, * pSimLi;
int w, i;
// constant
pObj = Aig_ManConst1( p->pAig );
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = ~(word)0;
// primary inputs
Ssw_RarManAssingRandomPis( p );
// flop outputs
if ( vInit )
{
assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords );
Saig_ManForEachLo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
}
}
else
{
Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
{ {
pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) ); for ( i = 0; i < p->nGroups; i++ )
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); p->pGroupValues[i] = 0;
for ( w = 0; w < p->nWords; w++ ) Saig_ManForEachLi( p->pAig, pObj, i )
pSim[w] = pSimLi[w];
}
}
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~0 : 0;
int w;
for ( w = 0; w < p->nWords; w++ )
if ( pSim[w] ^ Flip )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjsAreEqual( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~0 : 0;
int w;
for ( w = 0; w < p->nWords; w++ )
if ( pSim0[w] ^ pSim1[w] ^ Flip )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
unsigned uHash;
int i;
uHash = 0;
pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
for ( i = 0; i < 2 * p->nWords; i++ )
uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
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*************************************************************
Synopsis [Check if any of the POs becomes non-constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
{
Aig_Obj_t * pObj;
int i;
p->iFailPo = -1;
p->iFailPat = -1;
Saig_ManForEachPo( p->pAig, pObj, i )
{
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
return 0;
if ( !Ssw_RarManObjIsConst(p, pObj) )
{
p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
return 1;
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Performs one round of simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
{
Aig_Obj_t * pObj, * pRepr;
word * pSim, * pSim0, * pSim1;
word Flip, Flip0, Flip1;
int w, i;
// initialize
Ssw_RarManInitialize( p, vInit );
Vec_PtrClear( p->vUpdConst );
Vec_PtrClear( p->vUpdClass );
Aig_ManIncrementTravId( p->pAig );
// check comb inputs
if ( fUpdate )
Aig_ManForEachPi( p->pAig, pObj, i )
{
pRepr = Aig_ObjRepr(p->pAig, pObj);
if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
continue;
if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
continue;
// save for update
if ( pRepr == Aig_ManConst1(p->pAig) )
Vec_PtrPush( p->vUpdConst, pObj );
else
{
Vec_PtrPush( p->vUpdClass, pRepr );
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
// simulate
Aig_ManForEachNode( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
Flip0 = Aig_ObjFaninC0(pObj) ? ~0 : 0;
Flip1 = Aig_ObjFaninC1(pObj) ? ~0 : 0;
for ( w = 0; w < p->nWords; w++ )
pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
if ( !fUpdate )
continue;
// check classes
pRepr = Aig_ObjRepr(p->pAig, pObj);
if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
continue;
if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
continue;
// save for update
if ( pRepr == Aig_ManConst1(p->pAig) )
Vec_PtrPush( p->vUpdConst, pObj );
else
{
Vec_PtrPush( p->vUpdClass, pRepr );
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
// transfer to POs
Aig_ManForEachPo( p->pAig, pObj, i )
{ {
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) ); if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
Flip = Aig_ObjFaninC0(pObj) ? ~0 : 0; p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Flip ^ pSim0[w];
} }
// refine classes for ( i = 0; i < p->nGroups; i++ )
if ( fUpdate ) Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] );
{
if ( fFirst )
{
Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 );
Aig_ManForEachObj( p->pAig, pObj, i )
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
Vec_PtrPush( vCands, pObj );
assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) );
Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 );
Vec_PtrFree( vCands );
} }
else /*
for ( i = 0; i < p->nGroups; i++ )
{ {
Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 ); for ( k = 0; k < (1 << p->nBinSize); k++ )
Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 ); printf( "%d ", Ssw_RarGetBinPat(p, i, k) );
} printf( "\n" );
} }
} */
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
{
Ssw_RarMan_t * p;
if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
return NULL;
p = ABC_CALLOC( Ssw_RarMan_t, 1 );
p->pAig = pAig;
p->nWords = nWords;
p->nFrames = nFrames;
p->nBinSize = nBinSize;
p->fVerbose = fVerbose;
p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 );
p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords );
p->pPatData = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg );
p->vUpdConst = Vec_PtrAlloc( 100 );
p->vUpdClass = Vec_PtrAlloc( 100 );
p->vPatBests = Vec_IntAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ssw_RarManStop( Ssw_RarMan_t * p )
{
if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
Vec_IntFreeP( &p->vInits );
Vec_IntFreeP( &p->vPatBests );
Vec_PtrFreeP( &p->vUpdConst );
Vec_PtrFreeP( &p->vUpdClass );
ABC_FREE( p->pObjData );
ABC_FREE( p->pPatData );
ABC_FREE( p->pPatCosts );
ABC_FREE( p->pRarity );
ABC_FREE( p );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -727,36 +187,32 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p ) ...@@ -727,36 +187,32 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p )
***********************************************************************/ ***********************************************************************/
static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
{ {
// Aig_Obj_t * pObj; Aig_Obj_t * pObj;
unsigned char * pData; unsigned * pData;
unsigned * pPattern;
int i, k, Value; int i, k, Value;
// more data from regs to pats // for each pattern
Ssw_RarTranspose( p ); for ( k = 0; k < p->nWords * 32; k++ )
// update counters
for ( k = 0; k < p->nWords * 64; k++ )
{ {
pData = (unsigned char *)Ssw_RarPatSim( p, k );
for ( i = 0; i < p->nGroups; i++ ) for ( i = 0; i < p->nGroups; i++ )
Ssw_RarAddToBinPat( p, i, pData[i] ); p->pGroupValues[i] = 0;
} // compute its group values
Saig_ManForEachLi( p->pAig, pObj, i )
// for each pattern
for ( k = 0; k < p->nWords * 64; k++ )
{ {
pData = (unsigned char *)Ssw_RarPatSim( p, k ); pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
}
// find the cost of its values // find the cost of its values
p->pPatCosts[k] = 0.0; p->pPatCosts[k] = 0.0;
for ( i = 0; i < p->nGroups; i++ ) for ( i = 0; i < p->nGroups; i++ )
{ {
Value = Ssw_RarGetBinPat( p, i, pData[i] ); Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] );
assert( Value > 0 ); assert( Value > 0 );
p->pPatCosts[k] += 1.0/(Value*Value); p->pPatCosts[k] += 1.0/(Value*Value);
} }
// print the result // print the result
//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] ); // printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
} }
// choose as many as there are words // choose as many as there are words
...@@ -766,7 +222,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) ...@@ -766,7 +222,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
// select the best // select the best
int iPatBest = -1; int iPatBest = -1;
double iCostBest = -ABC_INFINITY; double iCostBest = -ABC_INFINITY;
for ( k = 0; k < p->nWords * 64; k++ ) for ( k = 0; k < p->nWords * 32; k++ )
if ( iCostBest < p->pPatCosts[k] ) if ( iCostBest < p->pPatCosts[k] )
{ {
iCostBest = p->pPatCosts[k]; iCostBest = p->pPatCosts[k];
...@@ -776,11 +232,12 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) ...@@ -776,11 +232,12 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
assert( iPatBest >= 0 ); assert( iPatBest >= 0 );
p->pPatCosts[iPatBest] = -ABC_INFINITY; p->pPatCosts[iPatBest] = -ABC_INFINITY;
// set the flops // set the flops
pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest ); Saig_ManForEachLi( p->pAig, pObj, k )
for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ ) {
Vec_IntPush( vInits, Aig_InfoHasBit(pPattern, k) ); pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) );
}
//printf( "Best pattern %5d\n", iPatBest ); //printf( "Best pattern %5d\n", iPatBest );
Vec_IntPush( p->vPatBests, iPatBest );
} }
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
} }
...@@ -847,11 +304,11 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex ...@@ -847,11 +304,11 @@ 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 nRandSeed, 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;
int r, f, clk, clkTotal = clock(); int r, clk, clkTotal = clock();
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 );
...@@ -859,43 +316,33 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i ...@@ -859,43 +316,33 @@ 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( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut ); nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers // reset random numbers
Ssw_RarManPrepareRandom( nRandSeed ); Aig_ManRandom( 1 );
// create manager // create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// perform simulation rounds // perform simulation rounds
for ( r = 0; r < nRounds; r++ ) for ( r = 0; r < nRounds; r++ )
{ {
clk = clock(); clk = clock();
// simulate // simulate
for ( f = 0; f < nFrames; f++ ) Ssw_SmlSimulateOne( p->pSml );
{ if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
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 );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
RetValue = 0; RetValue = 0;
goto finish; break;
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
goto finish;
}
} }
// get initialization patterns // get initialization patterns
Ssw_RarUpdateCounters( p );
Ssw_RarTransferPatterns( p, p->vInits ); Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// printout // printout
if ( fVerbose ) if ( fVerbose )
{ {
...@@ -903,9 +350,15 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i ...@@ -903,9 +350,15 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
// Abc_PrintTime( 1, "Time", clock() - clk ); // Abc_PrintTime( 1, "Time", clock() - clk );
printf( "." ); printf( "." );
} }
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
break;
}
} }
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 );
...@@ -919,30 +372,6 @@ finish: ...@@ -919,30 +372,6 @@ finish:
/**Function************************************************************* /**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*************************************************************
Synopsis [Filter equivalence classes of nodes.] Synopsis [Filter equivalence classes of nodes.]
Description [] Description []
...@@ -952,10 +381,11 @@ int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, i ...@@ -952,10 +381,11 @@ int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, i
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
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 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;
Ssw_RarMan_t * p; Ssw_RarMan_t * p;
int r, f, i, k, clkTotal = clock(); int r, i, k, clkTotal = clock();
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 );
...@@ -963,10 +393,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ...@@ -963,10 +393,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( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nRounds, nRandSeed, TimeOut ); nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers // reset random numbers
Ssw_RarManPrepareRandom( nRandSeed ); Aig_ManRandom( 1 );
// create manager // create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose ); p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
...@@ -981,13 +411,15 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ...@@ -981,13 +411,15 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
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) * nWords );
// initialize simulation manager
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// 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, 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->pSml, NULL, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
// print the stats // print the stats
if ( fVerbose ) if ( fVerbose )
{ {
...@@ -1004,53 +436,43 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz ...@@ -1004,53 +436,43 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
break; break;
} }
// simulate // simulate
for ( f = 0; f < nFrames; f++ ) Ssw_SmlSimulateOne( p->pSml );
{ if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( !fVerbose )
printf( "\r" );
// 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 );
RetValue = 0;
goto finish;
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{ {
if ( fVerbose ) printf( "\n" ); if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut ); printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
goto finish; RetValue = 0;
} break;
} }
// get initialization patterns // check equivalence classes
Ssw_RarTransferPatterns( p, p->vInits ); Ssw_ClassesRefineConst1( p->ppClasses, 1 );
Ssw_ClassesRefine( p->ppClasses, 1 );
// printout // printout
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Round %3d: ", r ); printf( "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 ); Ssw_ClassesPrint( p->ppClasses, 0 );
} }
else // get initialization patterns
Ssw_RarUpdateCounters( p );
Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{ {
printf( "." ); if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
break;
} }
} }
finish: if ( r == nRounds )
// report
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 RetValue; return -1;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1064,7 +486,7 @@ finish: ...@@ -1064,7 +486,7 @@ finish:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
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 ) 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;
...@@ -1075,16 +497,15 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz ...@@ -1075,16 +497,15 @@ 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, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose ); RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, 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;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
...@@ -24776,7 +24776,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -24776,7 +24776,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
int nRandSeed; int nRandSeed;
int TimeOut; int TimeOut;
int fVerbose; int fVerbose;
extern int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose ); extern int Ssw_RarSimulateGia( Gia_Man_t * p, 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;
...@@ -24871,7 +24871,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -24871,7 +24871,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_RarSimulate2Gia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ); pAbc->Status = Ssw_RarSimulateGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, 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;
...@@ -25310,7 +25310,7 @@ usage: ...@@ -25310,7 +25310,7 @@ 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_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_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_RarSignalFilterGia( 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 );
int c; int c;
int nFrames = 20; int nFrames = 20;
int nWords = 50; int nWords = 50;
...@@ -25435,7 +25435,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -25435,7 +25435,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
} }
// if ( fNewAlgo ) // if ( fNewAlgo )
pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose ); pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
// else // else
// 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, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
// pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame; // pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
......
src/base/abci/abcDar.c
...@@ -3027,53 +3027,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, ...@@ -3027,53 +3027,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_RarSimulate2( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 ) if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 )
{
if ( pMan->pSeqModel )
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame );
status = Saig_ManVerifyCex( pMan, pMan->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
RetValue = 0;
}
else
{
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
nFrames, nWords );
}
ABC_PRT( "Time", clock() - clk );
Aig_ManStop( pMan );
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs random simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 )
{
Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock();
if ( Abc_NtkGetChoiceNum(pNtk) )
{
printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
}
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( Ssw_RarSignalFilter( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ) == 0 )
{ {
if ( pMan->pSeqModel ) if ( pMan->pSeqModel )
{ {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment