summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-07-30 02:04:54 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2011-07-30 02:04:54 +0700
commite4f15dd003abc8085c563c777f737d8219e26606 (patch)
tree93d52691cff9383577e6194b313529a35947de8b /src
parentbadf8e474215d145d43c08acba63e33b35b74f5f (diff)
downloadabc-e4f15dd003abc8085c563c777f737d8219e26606.tar.gz
abc-e4f15dd003abc8085c563c777f737d8219e26606.tar.bz2
abc-e4f15dd003abc8085c563c777f737d8219e26606.zip
Changes to enable smarter simulation.
Diffstat (limited to 'src')
-rw-r--r--src/aig/ssw/sswInt.h1
-rw-r--r--src/aig/ssw/sswRarity.c6
-rw-r--r--src/aig/ssw/sswRarity2.c196
-rw-r--r--src/base/abci/abc.c11
4 files changed, 184 insertions, 30 deletions
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 93e828a1..15756782 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -230,6 +230,7 @@ extern int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs,
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
+extern int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr );
/*=== sswCnf.c ===================================================*/
extern Ssw_Sat_t * Ssw_SatStart( int fPolarFlip );
extern void Ssw_SatStop( Ssw_Sat_t * p );
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c
index 5657908e..f24e2d85 100644
--- a/src/aig/ssw/sswRarity.c
+++ b/src/aig/ssw/sswRarity.c
@@ -210,11 +210,9 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] );
assert( Value > 0 );
p->pPatCosts[k] += 1.0/(Value*Value);
-// printf( "%d ", Value );
}
-// printf( "\n" );
// 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
@@ -239,7 +237,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
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 );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
}
diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c
index b8fefe65..c0305931 100644
--- a/src/aig/ssw/sswRarity2.c
+++ b/src/aig/ssw/sswRarity2.c
@@ -53,6 +53,8 @@ struct Ssw_RarMan_t_
double * pPatCosts; // pattern costs
// best patterns
Vec_Int_t * vPatBests; // best patterns
+ int iFailPo; // failed primary output
+ int iFailPat; // failed pattern
};
@@ -87,6 +89,81 @@ static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 6
/**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, iPatFinal );
+ 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 );
+ return pCex;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Transposing 32-bit matrix.]
Description [Borrowed from "Hacker's Delight", by Henry Warren.]
@@ -282,12 +359,7 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
for ( w = 0; w < p->nWords; w++ )
pSim[w] = ~(word)0;
// primary inputs
- 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);
- }
+ Ssw_RarManAssingRandomPis( p );
// flop outputs
if ( vInit )
{
@@ -296,7 +368,7 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
{
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 );
+ pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
}
}
else
@@ -322,6 +394,34 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
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 [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) );
@@ -358,6 +458,44 @@ int Ssw_RarManObjsAreEqual( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pOb
/**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 [Check if any of the POs becomes non-constant.]
Description []
@@ -371,12 +509,18 @@ 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;
}
@@ -392,7 +536,7 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
SeeAlso []
***********************************************************************/
-void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate )
+void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
{
Aig_Obj_t * pObj, * pRepr;
word * pSim, * pSim0, * pSim1;
@@ -460,8 +604,21 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate )
// refine classes
if ( fUpdate )
{
- Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
- Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
+ 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 );
+ }
}
}
@@ -565,11 +722,9 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
Value = Ssw_RarGetBinPat( p, i, pData[i] );
assert( Value > 0 );
p->pPatCosts[k] += 1.0/(Value*Value);
-// printf( "%d ", Value );
}
-// printf( "\n" );
// 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
@@ -592,7 +747,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
Vec_IntPush( vInits, Aig_InfoHasBit(pPattern, k) );
-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 );
@@ -688,11 +843,13 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
// simulate
for ( f = 0; f < nFrames; f++ )
{
- Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0 );
+ Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+ ABC_FREE( pAig->pSeqModel );
+ pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
RetValue = 0;
goto finish;
}
@@ -774,7 +931,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
else
p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
- Ssw_ClassesSetData( p->ppClasses, p, NULL, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
+ Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
// print the stats
if ( fVerbose )
{
@@ -793,11 +950,13 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
// simulate
for ( f = 0; f < nFrames; f++ )
{
- Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1 );
+ Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+ ABC_FREE( pAig->pSeqModel );
+ pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
RetValue = 0;
goto finish;
}
@@ -859,9 +1018,6 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz
}
-
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0f800d01..7756dbdc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25167,8 +25167,8 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
int TimeOut = 0;
int fUseCex = 0;
int fLatchOnly = 0;
- int fNewAlgo = 0;
- int fVerbose = 1;
+ int fNewAlgo = 1;
+ int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlavh" ) ) != EOF )
{
@@ -25266,7 +25266,6 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
}
-// pAbc->Status = Abc_NtkDarSeqEquiv2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
if ( fNewAlgo )
pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
else
@@ -25276,14 +25275,14 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &equiv3 [-FWBRT num] [-xlvh]\n" );
+ Abc_Print( -2, "usage: &equiv3 [-FWRT num] [-xlvh]\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-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-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeOut );
- 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-a : toggle using a new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );