summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/ssw.h20
-rw-r--r--src/aig/ssw/sswAig.c1
-rw-r--r--src/aig/ssw/sswClass.c6
-rw-r--r--src/aig/ssw/sswCore.c10
-rw-r--r--src/aig/ssw/sswDyn.c106
-rw-r--r--src/aig/ssw/sswInt.h18
-rw-r--r--src/aig/ssw/sswIslands.c543
-rw-r--r--src/aig/ssw/sswMan.c5
-rw-r--r--src/aig/ssw/sswPart.c2
-rw-r--r--src/aig/ssw/sswSim.c229
10 files changed, 732 insertions, 208 deletions
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 5d70812d..b3222fca 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -51,11 +51,16 @@ struct Ssw_Pars_t_
int nBTLimitGlobal;// conflict limit for multiple runs
int nMinDomSize; // min clock domain considered for optimization
int nItersStop; // stop after the given number of iterations
+ int fDumpSRInit; // dumps speculative reduction
+ int nResimDelta; // the number of nodes to resimulate
int fPolarFlip; // uses polarity adjustment
int fLatchCorr; // perform register correspondence
int fSemiFormal; // enable semiformal filtering
int fUniqueness; // enable uniqueness constraints
int fDynamic; // enable dynamic addition of constraints
+ int fLocalSim; // enable local simulation simulation
+ int fPartSigCorr; // uses partial signal correspondence
+ int nIsleDist; // extends islands by the given distance
int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops
// optimized latch correspondence
@@ -82,6 +87,8 @@ struct Ssw_Cex_t_
unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
};
+typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -97,8 +104,11 @@ extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
+/*=== sswIslands.c ==========================================================*/
+extern int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars );
+extern int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars );
/*=== sswMiter.c ===================================================*/
-extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose );
+extern int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbose );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
@@ -107,6 +117,14 @@ 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_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
/*=== sswSim.c ===================================================*/
+extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
+extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
+extern void Ssw_SmlUnnormalize( Ssw_Sml_t * p );
+extern void Ssw_SmlStop( Ssw_Sml_t * p );
+extern int Ssw_SmlNumFrames( Ssw_Sml_t * p );
+extern int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p );
+extern unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj );
+extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern Ssw_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex );
extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index fda05941..97f0a755 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -211,6 +211,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
+ pFrames->pName = Aig_UtilStrsav( p->pAig->pName );
// map constants and PIs
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 771fd530..3528ae27 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -585,7 +585,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
SeeAlso []
***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int nMaxLevs, int fVerbose )
{
// int nFrames = 4;
// int nWords = 1;
@@ -595,7 +595,7 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs,
// int nWords = 4;
// int nIters = 0;
- int nFrames = 4;
+ int nFrames = AIG_MAX( nFramesK, 4 );
int nWords = 2;
int nIters = 16;
Ssw_Cla_t * p;
@@ -836,7 +836,7 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
SeeAlso []
***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
+Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
{
Ssw_Cla_t * p;
Aig_Obj_t ** ppClassNew;
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 68c00a0e..38a36022 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -51,10 +51,13 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nBTLimitGlobal = 5000000; // conflict limit for all runs
p->nMinDomSize = 100; // min clock domain considered for optimization
p->nItersStop = 0; // stop after the given number of iterations
+ p->nResimDelta = 1000; // the internal of nodes to resimulate
p->fPolarFlip = 0; // uses polarity adjustment
p->fLatchCorr = 0; // performs register correspondence
p->fSemiFormal = 0; // enable semiformal filtering
p->fUniqueness = 0; // enable uniqueness constraints
+ p->fDynamic = 0; // dynamic partitioning
+ p->fLocalSim = 0; // local simulation
p->fVerbose = 0; // verbose stats
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
@@ -260,6 +263,9 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
if ( pPars->fLatchCorrOpt )
{
pPars->fLatchCorr = 1;
+ pPars->nFramesAddSim = 0;
+ if ( (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
+ return Ssw_SignalCorrespondencePart( pAig, pPars );
}
else
{
@@ -276,7 +282,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
if ( p->pPars->nConstrs == 0 )
{
// perform one round of seq simulation and generate candidate equivalence classes
- p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+ p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
// p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
if ( pPars->fLatchCorrOpt )
p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
@@ -292,6 +298,8 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
}
+ if ( p->pPars->fLocalSim )
+ p->pVisited = CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
if ( pPars->fUniqueness )
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
index d5559408..d9ac07a9 100644
--- a/src/aig/ssw/sswDyn.c
+++ b/src/aig/ssw/sswDyn.c
@@ -279,6 +279,83 @@ p->timeSimSat += clock() - clk;
/**Function*************************************************************
+ Synopsis [Performs one round of simulation with counter-examples.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
+{
+ Aig_Obj_t * pObj, * pRepr, ** ppClass;
+ int i, k, nSize, RetValue1, RetValue2, clk = clock();
+ p->nSimRounds++;
+ // transfer PI simulation information from storage
+// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
+ Ssw_ManSweepTransferDyn( p );
+ // determine const1 cands and classes to be simulated
+ Vec_PtrClear( p->vResimConsts );
+ Vec_PtrClear( p->vResimClasses );
+ Aig_ManIncrementTravId( p->pAig );
+ for ( i = p->iNodeStart; i < p->iNodeLast + p->pPars->nResimDelta; i++ )
+ {
+ if ( i >= Aig_ManObjNumMax( p->pAig ) )
+ break;
+ pObj = Aig_ManObj( p->pAig, i );
+ if ( pObj == NULL )
+ continue;
+ if ( Ssw_ObjIsConst1Cand(p->pAig, pObj) )
+ {
+ Vec_PtrPush( p->vResimConsts, pObj );
+ continue;
+ }
+ pRepr = Aig_ObjRepr(p->pAig, pObj);
+ if ( pRepr == NULL )
+ continue;
+ if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
+ continue;
+ Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
+ Vec_PtrPush( p->vResimClasses, pRepr );
+ }
+ // simulate internal nodes
+// Ssw_SmlSimulateOneFrame( p->pSml );
+// Ssw_SmlSimulateOne( p->pSml );
+ // resimulate dynamically
+// Aig_ManIncrementTravId( p->pAig );
+// Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
+ p->nVisCounter++;
+ Vec_PtrForEachEntry( p->vResimConsts, pObj, i )
+ Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter );
+ // resimulate the cone of influence of the cand classes
+ Vec_PtrForEachEntry( p->vResimClasses, pRepr, i )
+ {
+ ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize );
+ for ( k = 0; k < nSize; k++ )
+ Ssw_SmlSimulateOneDyn_rec( p->pSml, ppClass[k], p->nFrames-1, p->pVisited, p->nVisCounter );
+ }
+
+ // check equivalence classes
+// RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+// RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
+ // refine these nodes
+ RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 );
+ RetValue2 = 0;
+ Vec_PtrForEachEntry( p->vResimClasses, pRepr, i )
+ RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 );
+
+ // prepare simulation info for the next round
+ Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+ p->nPatterns = 0;
+ p->nSimRounds++;
+p->timeSimSat += clock() - clk;
+ return RetValue1 > 0 || RetValue2 > 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs fraiging for the internal nodes.]
Description []
@@ -321,8 +398,11 @@ p->timeReduce += clock() - clk;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+ p->iNodeStart = 0;
Aig_ManForEachObj( p->pAig, pObj, i )
{
+ if ( p->iNodeStart == 0 )
+ p->iNodeStart = i;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
@@ -341,7 +421,14 @@ p->timeReduce += clock() - clk;
{
// resimulate
if ( p->nPatterns > 0 )
- Ssw_ManSweepResimulateDyn( p, f );
+ {
+ p->iNodeLast = i;
+ if ( p->pPars->fLocalSim )
+ Ssw_ManSweepResimulateDynLocal( p, f );
+ else
+ Ssw_ManSweepResimulateDyn( p, f );
+ p->iNodeStart = i+1;
+ }
// printf( "Recycling SAT solver with %d vars and %d calls.\n",
// p->pMSat->nSatVars, p->nRecycleCalls );
// Aig_ManCleanMarkAB( p->pAig );
@@ -363,11 +450,24 @@ p->timeReduce += clock() - clk;
}
// resimulate
if ( p->nPatterns == 32 )
- Ssw_ManSweepResimulateDyn( p, f );
+ {
+ p->iNodeLast = i;
+ if ( p->pPars->fLocalSim )
+ Ssw_ManSweepResimulateDynLocal( p, f );
+ else
+ Ssw_ManSweepResimulateDyn( p, f );
+ p->iNodeStart = i+1;
+ }
}
// resimulate
if ( p->nPatterns > 0 )
- Ssw_ManSweepResimulateDyn( p, f );
+ {
+ p->iNodeLast = i;
+ if ( p->pPars->fLocalSim )
+ Ssw_ManSweepResimulateDynLocal( p, f );
+ else
+ Ssw_ManSweepResimulateDyn( p, f );
+ }
// collect stats
if ( p->pPars->fVerbose )
Bar_ProgressStop( pProgress );
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 90c1367f..930796fc 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -45,7 +45,6 @@ typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
typedef struct Ssw_Frm_t_ Ssw_Frm_t; // unrolled frames manager
typedef struct Ssw_Sat_t_ Ssw_Sat_t; // SAT solver manager
typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager
-typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
struct Ssw_Man_t_
{
@@ -86,8 +85,14 @@ struct Ssw_Man_t_
int nSRMiterMaxId; // max ID after which the last frame begins
Vec_Ptr_t * vNewLos; // new time frame LOs of to constrain
Vec_Int_t * vNewPos; // new time frame POs of to add constraints
- // sequential simulator
- Ssw_Sml_t * pSml;
+ int * pVisited; // flags to label visited nodes in each frame
+ int nVisCounter; // the traversal ID
+ // sequential simulation
+ Ssw_Sml_t * pSml; // the simulator
+ int iNodeStart; // the first node considered
+ int iNodeLast; // the last node considered
+ Vec_Ptr_t * vResimConsts; // resimulation constants
+ Vec_Ptr_t * vResimClasses; // resimulation classes
// counter example storage
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
@@ -201,11 +206,11 @@ extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr,
extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
-extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose );
+extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
-extern Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
+extern Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
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 );
@@ -242,13 +247,12 @@ extern void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj,
extern Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void Ssw_SmlClean( Ssw_Sml_t * p );
extern void Ssw_SmlStop( Ssw_Sml_t * p );
-extern int Ssw_SmlNumFrames( Ssw_Sml_t * p );
extern void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
extern void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
extern void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
-extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
+extern void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pVisited, int nVisCounter );
extern void Ssw_SmlResimulateSeq( Ssw_Sml_t * p );
/*=== sswSimSat.c ===================================================*/
extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c
index 5a5783f7..64515f3e 100644
--- a/src/aig/ssw/sswIslands.c
+++ b/src/aig/ssw/sswIslands.c
@@ -24,9 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline Aig_Obj_t * Aig_ObjChild0Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin0(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
-static inline Aig_Obj_t * Aig_ObjChild1Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -52,7 +49,7 @@ void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
/**Function*************************************************************
- Synopsis [Detects islands of common logic and returns them as pairs.]
+ Synopsis [Establishes relationship between nodes using pairing.]
Description []
@@ -61,48 +58,127 @@ void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Ssw_DetectIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose )
+void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
{
- Vec_Int_t * vPairs;
- Aig_Obj_t * pObj0, * pObj1, * pFanin0, * pFanin1;
+ Aig_Obj_t * pObj0, * pObj1;
int i;
- assert( Aig_ManRegNum(p0) > 0 );
- assert( Aig_ManRegNum(p1) > 0 );
- assert( Aig_ManRegNum(p0) >= nCommonFlops );
- assert( Aig_ManRegNum(p1) >= nCommonFlops );
- assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
- assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
+ // create matching
Aig_ManCleanData( p0 );
Aig_ManCleanData( p1 );
- // start structural equivalence
- vPairs = Vec_IntAlloc( 1000 );
- Ssw_CreatePair( vPairs, Aig_ManConst1(p0), Aig_ManConst1(p1) );
+ for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
+ {
+ pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
+ pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
+ assert( pObj0->pData == NULL );
+ assert( pObj1->pData == NULL );
+ pObj0->pData = pObj1;
+ pObj1->pData = pObj0;
+ }
+ // make sure constants are matched
+ pObj0 = Aig_ManConst1( p0 );
+ pObj1 = Aig_ManConst1( p1 );
+ assert( pObj0->pData == pObj1 );
+ assert( pObj1->pData == pObj0 );
+ // make sure PIs are matched
Saig_ManForEachPi( p0, pObj0, i )
- Ssw_CreatePair( vPairs, pObj0, Aig_ManPi(p1, i) );
+ {
+ pObj1 = Aig_ManPi( p1, i );
+ assert( pObj0->pData == pObj1 );
+ assert( pObj1->pData == pObj0 );
+ }
+ // make sure the POs are not matched
+ Aig_ManForEachPo( p0, pObj0, i )
+ {
+ pObj1 = Aig_ManPo( p1, i );
+ assert( pObj0->pData == NULL );
+ assert( pObj1->pData == NULL );
+ }
+
+ // check that LIs/LOs are matched in sync
Saig_ManForEachLo( p0, pObj0, i )
{
- if ( i == nCommonFlops )
- break;
- Ssw_CreatePair( vPairs, pObj0, Saig_ManLo(p1, i) );
+ if ( pObj0->pData == NULL )
+ continue;
+ pObj1 = pObj0->pData;
+ if ( !Saig_ObjIsLo(p1, pObj1) )
+ printf( "Mismatch between LO pairs.\n" );
}
- // find structurally equivalent nodes
- Aig_ManForEachNode( p0, pObj0, i )
+ Saig_ManForEachLo( p1, pObj1, i )
+ {
+ if ( pObj1->pData == NULL )
+ continue;
+ pObj0 = pObj1->pData;
+ if ( !Saig_ObjIsLo(p0, pObj0) )
+ printf( "Mismatch between LO pairs.\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Establishes relationship between nodes using pairing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+{
+ Aig_Obj_t * pNext, * pObj;
+ int i, k, iFan;
+ Vec_PtrClear( vNodes );
+ Aig_ManIncrementTravId( p );
+ Aig_ManForEachObj( p, pObj, i )
{
- pFanin0 = Aig_ObjChild0Copy2( pObj0 );
- pFanin1 = Aig_ObjChild1Copy2( pObj0 );
- if ( pFanin0 == NULL || pFanin1 == NULL )
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
- pObj1 = Aig_TableLookupTwo( p1, pFanin0, pFanin1 );
- if ( pObj1 == NULL )
+ if ( pObj->pData != NULL )
continue;
- Ssw_CreatePair( vPairs, pObj0, pObj1 );
+ if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pNext = Saig_ObjLoToLi(p, pObj);
+ pNext = Aig_ObjFanin0(pNext);
+ if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) && !Aig_ObjIsConst1(pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ }
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ pNext = Aig_ObjFanin0(pObj);
+ if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ pNext = Aig_ObjFanin1(pObj);
+ if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ }
+ Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
+ {
+ if ( Saig_ObjIsPo(p, pNext) )
+ continue;
+ if ( Saig_ObjIsLi(p, pNext) )
+ pNext = Saig_ObjLiToLo(p, pNext);
+ if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
+ {
+ Aig_ObjSetTravIdCurrent(p, pNext);
+ Vec_PtrPush( vNodes, pNext );
+ }
+ }
}
- return vPairs;
}
/**Function*************************************************************
- Synopsis [Collects additional Lis and Los.]
+ Synopsis [Establishes relationship between nodes using pairing.]
Description []
@@ -111,22 +187,24 @@ Vec_Int_t * Ssw_DetectIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops,
SeeAlso []
***********************************************************************/
-void Ssw_CollectExtraLiLo( Aig_Man_t * p, int nCommonFlops, Vec_Ptr_t * vLis, Vec_Ptr_t * vLos )
+int Ssw_MatchingCountUnmached( Aig_Man_t * p )
{
- Aig_Obj_t * pObjLo, * pObjLi;
- int i;
- Saig_ManForEachLiLo( p, pObjLo, pObjLi, i )
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ Aig_ManForEachObj( p, pObj, i )
{
- if ( i < nCommonFlops )
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ continue;
+ if ( pObj->pData != NULL )
continue;
- Vec_PtrPush( vLis, pObjLi );
- Vec_PtrPush( vLos, pObjLo );
+ Counter++;
}
+ return Counter;
}
/**Function*************************************************************
- Synopsis [Overlays and extends the pairs.]
+ Synopsis [Establishes relationship between nodes using pairing.]
Description []
@@ -135,80 +213,195 @@ void Ssw_CollectExtraLiLo( Aig_Man_t * p, int nCommonFlops, Vec_Ptr_t * vLis, Ve
SeeAlso []
***********************************************************************/
-void Ssw_OverlayIslands( Aig_Man_t * pTo, Aig_Man_t * pFrom, Vec_Ptr_t * vLisFrom, Vec_Ptr_t * vLosFrom, Vec_Int_t * vPairs, int nCommonFlops, int fToGoesFirst )
+void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose )
{
- Aig_Obj_t * pObjFrom, * pObjTo, * pFanin0To, * pFanin1To;
- int i;
- // create additional register outputs of From in To
- Vec_PtrForEachEntry( vLosFrom, pObjFrom, i )
+ Vec_Ptr_t * vNodes0, * vNodes1;
+ Aig_Obj_t * pNext0, * pNext1;
+ int d, k;
+ Aig_ManFanoutStart(p0);
+ Aig_ManFanoutStart(p1);
+ vNodes0 = Vec_PtrAlloc( 1000 );
+ vNodes1 = Vec_PtrAlloc( 1000 );
+ if ( fVerbose )
{
- pObjTo = Aig_ObjCreatePi( pTo );
- if( fToGoesFirst )
- Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
- else
- Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
+ int nUnmached = Ssw_MatchingCountUnmached(p0);
+ printf( "Extending islands by %d steps:\n", nDist );
+ printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ 0, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0),
+ nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
}
- // create additional nodes of From in To
- Aig_ManForEachNode( pFrom, pObjFrom, i )
+ for ( d = 0; d < nDist; d++ )
{
- if ( pObjFrom->pData != NULL )
+ Ssw_MatchingExtendOne( p0, vNodes0 );
+ Ssw_MatchingExtendOne( p1, vNodes1 );
+ Vec_PtrForEachEntry( vNodes0, pNext0, k )
+ {
+ pNext1 = pNext0->pData;
+ if ( pNext1 == NULL )
+ continue;
+ assert( pNext1->pData == pNext0 );
+ if ( Saig_ObjIsPi(p0, pNext1) )
+ continue;
+ pNext0->pData = NULL;
+ pNext1->pData = NULL;
+ }
+ Vec_PtrForEachEntry( vNodes1, pNext0, k )
+ {
+ pNext1 = pNext0->pData;
+ if ( pNext1 == NULL )
+ continue;
+ assert( pNext1->pData == pNext0 );
+ if ( Saig_ObjIsPi(p1, pNext1) )
+ continue;
+ pNext0->pData = NULL;
+ pNext1->pData = NULL;
+ }
+ if ( fVerbose )
+ {
+ int nUnmached = Ssw_MatchingCountUnmached(p0);
+ printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
+ d+1, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0),
+ nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
+ }
+ }
+ Vec_PtrFree( vNodes0 );
+ Vec_PtrFree( vNodes1 );
+ Aig_ManFanoutStop(p0);
+ Aig_ManFanoutStop(p1);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Used differences in p0 to complete p1.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Vec_Ptr_t * vNewLis;
+ Aig_Obj_t * pObj0, * pObj0Li, * pObj1;
+ int i;
+ // create register outputs in p0 that are absent in p1
+ vNewLis = Vec_PtrAlloc( 100 );
+ Saig_ManForEachLiLo( p0, pObj0Li, pObj0, i )
+ {
+ if ( pObj0->pData != NULL )
continue;
- pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
- pFanin1To = Aig_ObjChild1Copy2( pObjFrom );
- assert( pFanin0To != NULL && pFanin1To != NULL );
- pObjTo = Aig_And( pTo, pFanin0To, pFanin1To );
- if( fToGoesFirst )
- Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
- else
- Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
+ pObj1 = Aig_ObjCreatePi( p1 );
+ pObj0->pData = pObj1;
+ pObj1->pData = pObj0;
+ Vec_PtrPush( vNewLis, pObj0Li );
}
- // finally recreate additional register inputs
- Vec_PtrForEachEntry( vLisFrom, pObjFrom, i )
+ // add missing nodes in the topological order
+ Aig_ManForEachNode( p0, pObj0, i )
{
- pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
- Aig_ObjCreatePo( pTo, pFanin0To );
+ if ( pObj0->pData != NULL )
+ continue;
+ pObj1 = Aig_And( p1, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
+ pObj0->pData = pObj1;
+ pObj1->pData = pObj0;
}
- // update the number of registers
- Aig_ManSetRegNum( pTo, Aig_ManRegNum(pTo) + Vec_PtrSize(vLisFrom) );
+ // create register outputs in p0 that are absent in p1
+ Vec_PtrForEachEntry( vNewLis, pObj0Li, i )
+ Aig_ObjCreatePo( p1, Aig_ObjChild0Copy(pObj0Li) );
+ // increment the number of registers
+ Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
+ Vec_PtrFree( vNewLis );
}
+
/**Function*************************************************************
- Synopsis [Overlays and extends the pairs.]
+ Synopsis [Derives matching for all pairs.]
- Description []
+ Description [Modifies both AIGs.]
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Int_t * Saig_ManMiterWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, Aig_Man_t ** ppMiter, Vec_Int_t * vPairs )
+Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
{
- Aig_Man_t * pMiter;
Vec_Int_t * vPairsNew;
Aig_Obj_t * pObj0, * pObj1;
int i;
- vPairsNew = Vec_IntAlloc( 1000 );
- pMiter = Saig_ManCreateMiter( p0, p1, 0 );
- for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
+ // check correctness
+ assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) );
+ assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) );
+ assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) );
+ assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) );
+ // create complete pairs
+ vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
+ Aig_ManForEachObj( p0, pObj0, i )
{
- pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
- pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
+ if ( Aig_ObjIsPo(pObj0) )
+ continue;
+ pObj1 = pObj0->pData;
+ Vec_IntPush( vPairsNew, pObj0->Id );
+ Vec_IntPush( vPairsNew, pObj1->Id );
+ }
+ return vPairsNew;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Transfers the result of matching to miter.]
+
+ Description [The array of pairs should be complete.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairsAll )
+{
+ Vec_Int_t * vPairsMiter;
+ Aig_Obj_t * pObj0, * pObj1;
+ int i;
+ // create matching of nodes in the miter
+ vPairsMiter = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
+ for ( i = 0; i < Vec_IntSize(vPairsAll); i += 2 )
+ {
+ pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairsAll, i) );
+ pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairsAll, i+1) );
+ assert( pObj0->pData != NULL );
+ assert( pObj1->pData != NULL );
+ if ( pObj0->pData == pObj1->pData )
+ continue;
+ if ( Aig_ObjIsNone(pObj0->pData) || Aig_ObjIsNone(pObj1->pData) )
+ continue;
+ // get the miter nodes
pObj0 = pObj0->pData;
pObj1 = pObj1->pData;
assert( !Aig_IsComplement(pObj0) );
assert( !Aig_IsComplement(pObj1) );
- if ( pObj0 == pObj1 )
+ assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
+ if ( Aig_ObjIsPo(pObj0) )
continue;
+ assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
+ assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
assert( pObj0->Id < pObj1->Id );
- Vec_IntPush( vPairsNew, pObj0->Id );
- Vec_IntPush( vPairsNew, pObj1->Id );
+ Vec_IntPush( vPairsMiter, pObj0->Id );
+ Vec_IntPush( vPairsMiter, pObj1->Id );
}
- *ppMiter = pMiter;
- return vPairsNew;
+ return vPairsMiter;
}
+
+
+
+
/**Function*************************************************************
Synopsis [Solves SEC using structural similarity.]
@@ -220,72 +413,41 @@ Vec_Int_t * Saig_ManMiterWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, Aig_Man_t
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ssw_SecWithIslandsInternal( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
+Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
Ssw_Man_t * p;
- Ssw_Pars_t Pars;
- Vec_Int_t * vPairs, * vPairsMiter;
+ Vec_Int_t * vPairsAll, * vPairsMiter;
Aig_Man_t * pMiter, * pAigNew;
- Vec_Ptr_t * vLis0, * vLos0, * vLis1, * vLos1;
- int nNodes, nRegs;
- assert( Aig_ManRegNum(p0) > 0 );
- assert( Aig_ManRegNum(p1) > 0 );
- assert( Aig_ManRegNum(p0) >= nCommonFlops );
- assert( Aig_ManRegNum(p1) >= nCommonFlops );
- assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
- assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
- // derive pairs
- vPairs = Ssw_DetectIslands( p0, p1, nCommonFlops, fVerbose );
- if ( fVerbose )
- {
- printf( "Original managers:\n" );
- Aig_ManPrintStats( p0 );
- Aig_ManPrintStats( p1 );
- printf( "Detected %d PI pairs, %d LO pairs, and %d node pairs.\n",
- Saig_ManPiNum(p0), nCommonFlops, Vec_IntSize(vPairs)/2 - Saig_ManPiNum(p0) - nCommonFlops - 1 );
- }
- // complete the manager with islands
- vLis0 = Vec_PtrAlloc( 100 );
- vLos0 = Vec_PtrAlloc( 100 );
- vLis1 = Vec_PtrAlloc( 100 );
- vLos1 = Vec_PtrAlloc( 100 );
- Ssw_CollectExtraLiLo( p0, nCommonFlops, vLis0, vLos0 );
- Ssw_CollectExtraLiLo( p1, nCommonFlops, vLis1, vLos1 );
-
- nRegs = Saig_ManRegNum(p0);
- nNodes = Aig_ManNodeNum(p0);
- Ssw_OverlayIslands( p0, p1, vLis1, vLos1, vPairs, nCommonFlops, 1 );
- if ( fVerbose )
- printf( "Completed p0 with %d registers and %d nodes.\n",
- Saig_ManRegNum(p0) - nRegs, Aig_ManNodeNum(p0) - nNodes );
-
- nRegs = Saig_ManRegNum(p1);
- nNodes = Aig_ManNodeNum(p1);
- Ssw_OverlayIslands( p1, p0, vLis0, vLos0, vPairs, nCommonFlops, 0 );
- if ( fVerbose )
- printf( "Completed p1 with %d registers and %d nodes.\n",
- Saig_ManRegNum(p1) - nRegs, Aig_ManNodeNum(p1) - nNodes );
- if ( fVerbose )
- {
- printf( "Modified managers:\n" );
- Aig_ManPrintStats( p0 );
- Aig_ManPrintStats( p1 );
- }
-
- Vec_PtrFree( vLis0 );
- Vec_PtrFree( vLos0 );
- Vec_PtrFree( vLis1 );
- Vec_PtrFree( vLos1 );
- // create sequential miter
- vPairsMiter = Saig_ManMiterWithIslands( p0, p1, &pMiter, vPairs );
- Vec_IntFree( vPairs );
- // if parameters are not given, create them
- if ( pPars == NULL )
- Ssw_ManSetDefaultParams( pPars = &Pars );
+ // derive full matching
+ Ssw_MatchingStart( p0, p1, vPairs );
+ if ( pPars->nIsleDist )
+ Ssw_MatchingExtend( p0, p1, pPars->nIsleDist, pPars->fVerbose );
+ Ssw_MatchingComplete( p0, p1 );
+ Ssw_MatchingComplete( p1, p0 );
+ vPairsAll = Ssw_MatchingPairs( p0, p1 );
+ // create miter and transfer matching
+ pMiter = Saig_ManCreateMiter( p0, p1, 0 );
+ vPairsMiter = Ssw_MatchingMiter( pMiter, p0, p1, vPairsAll );
+ Vec_IntFree( vPairsAll );
// start the induction manager
p = Ssw_ManCreate( pMiter, pPars );
// create equivalence classes using these IDs
- p->ppClasses = Ssw_ClassesFromIslands( pMiter, vPairsMiter );
+ if ( p->pPars->fPartSigCorr )
+ p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
+ else
+ p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+ if ( p->pPars->fDumpSRInit )
+ {
+ if ( p->pPars->fPartSigCorr )
+ {
+ Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
+ Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL );
+ Aig_ManStop( pSRed );
+ printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
+ }
+ else
+ printf( "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
+ }
p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
// perform refinement of classes
@@ -299,28 +461,28 @@ Aig_Man_t * Ssw_SecWithIslandsInternal( Aig_Man_t * p0, Aig_Man_t * p1, int nCom
/**Function*************************************************************
- Synopsis [Solves SEC using structural similarity.]
+ Synopsis [Solves SEC with structural similarity.]
- Description []
+ Description [The first two arguments are pointers to the AIG managers.
+ The third argument is the array of pairs of IDs of structurally equivalent
+ nodes from the first and second managers, respectively.]
- SideEffects []
+ SideEffects [The managers will be updated by adding "islands of difference".]
SeeAlso []
***********************************************************************/
-int Ssw_SecWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
+int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
+ Ssw_Pars_t Pars;
Aig_Man_t * pAigRes;
- Aig_Man_t * p0New, * p1New;
int RetValue, clk = clock();
- // try the new AIGs
-// printf( "Performing verification using structural similarity.\n" );
- p0New = Aig_ManDupSimple( p0 );
- p1New = Aig_ManDupSimple( p1 );
- pAigRes = Ssw_SecWithIslandsInternal( p0New, p1New, nCommonFlops, fVerbose, pPars );
- Aig_ManStop( p0New );
- Aig_ManStop( p1New );
- // report the results
+ // derive parameters if not given
+ if ( pPars == NULL )
+ Ssw_ManSetDefaultParams( pPars = &Pars );
+ // reduce the AIG with pairs
+ pAigRes = Ssw_SecWithSimilaritySweep( p0, p1, vPairs, pPars );
+ // report the result of verification
RetValue = Ssw_MiterStatus( pAigRes, 1 );
if ( RetValue == 1 )
printf( "Verification successful. " );
@@ -328,17 +490,43 @@ int Ssw_SecWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fV
printf( "Verification failed with a counter-example. " );
else
printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
- Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0New)+Aig_ManRegNum(p1New) );
+ Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
PRT( "Time", clock() - clk );
- // cleanup
Aig_ManStop( pAigRes );
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis [Dummy procedure to detect structural similarity.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 )
+{
+ Vec_Int_t * vPairs;
+ Aig_Obj_t * pObj;
+ int i;
+ // create array of pairs
+ vPairs = Vec_IntAlloc( 100 );
+ Aig_ManForEachObj( p0, pObj, i )
+ {
+ if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+ continue;
+ Vec_IntPush( vPairs, i );
+ Vec_IntPush( vPairs, i );
+ }
+ return vPairs;
+}
/**Function*************************************************************
- Synopsis [Solves SEC using structural similarity for the miter.]
+ Synopsis [Solves SEC with structural similarity.]
Description []
@@ -347,34 +535,57 @@ int Ssw_SecWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fV
SeeAlso []
***********************************************************************/
-int Ssw_SecWithIslandsMiter( Aig_Man_t * pMiter, int nCommonFlops, int fVerbose )
+int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
{
+ Vec_Int_t * vPairs;
Aig_Man_t * pPart0, * pPart1;
int RetValue;
- if ( fVerbose )
- Aig_ManPrintStats( pMiter );
- // demiter the miter
- if ( !Saig_ManDemiterSimpleDiff( pMiter, &pPart0, &pPart1 ) )
+ if ( pPars->fVerbose )
+ printf( "Performing sequential verification using structural similarity.\n" );
+ // consider the case when a miter is given
+ if ( p1 == NULL )
{
- printf( "Demitering has failed.\n" );
- return -1;
+ if ( pPars->fVerbose )
+ {
+ Aig_ManPrintStats( p0 );
+ }
+ // demiter the miter
+ if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
+ {
+ printf( "Demitering has failed.\n" );
+ return -1;
+ }
}
- if ( fVerbose )
+ else
+ {
+ pPart0 = Aig_ManDupSimple( p0 );
+ pPart1 = Aig_ManDupSimple( p1 );
+ }
+ if ( pPars->fVerbose )
{
// Aig_ManPrintStats( pPart0 );
// Aig_ManPrintStats( pPart1 );
+ if ( p1 == NULL )
+ {
// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
+ }
}
- RetValue = Ssw_SecWithIslands( pPart0, pPart1, nCommonFlops, fVerbose, NULL );
+ assert( Aig_ManRegNum(pPart0) > 0 );
+ assert( Aig_ManRegNum(pPart1) > 0 );
+ assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
+ assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
+ // derive pairs
+// vPairs = Saig_StrSimPerformMatching_hack( pPart0, pPart1 );
+ vPairs = Saig_StrSimPerformMatching( pPart0, pPart1, 0, pPars->fVerbose, NULL );
+ RetValue = Ssw_SecWithSimilarityPairs( pPart0, pPart1, vPairs, pPars );
Aig_ManStop( pPart0 );
Aig_ManStop( pPart1 );
+ Vec_IntFree( vPairs );
return RetValue;
}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 913f7518..7e6e4473 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -61,6 +61,8 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// other
p->vNewLos = Vec_PtrAlloc( 100 );
p->vNewPos = Vec_IntAlloc( 100 );
+ p->vResimConsts = Vec_PtrAlloc( 100 );
+ p->vResimClasses = Vec_PtrAlloc( 100 );
// p->pPars->fVerbose = 1;
return p;
@@ -171,6 +173,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManStop( Ssw_Man_t * p )
{
+ FREE( p->pVisited );
if ( p->pPars->fVerbose )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
@@ -179,6 +182,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
Ssw_SmlStop( p->pSml );
if ( p->vDiffPairs )
Vec_IntFree( p->vDiffPairs );
+ Vec_PtrFree( p->vResimConsts );
+ Vec_PtrFree( p->vResimClasses );
Vec_PtrFree( p->vNewLos );
Vec_IntFree( p->vNewPos );
Vec_PtrFree( p->vCommon );
diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c
index 983a2022..9d2ec34e 100644
--- a/src/aig/ssw/sswPart.c
+++ b/src/aig/ssw/sswPart.c
@@ -30,7 +30,7 @@
/**Function*************************************************************
- Synopsis [Performs partitioned sequential SAT sweepingG.]
+ Synopsis [Performs partitioned sequential SAT sweeping.]
Description []
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 836b75e3..a860199e 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -200,19 +200,21 @@ int Ssw_SmlCheckXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
{
unsigned * pSimLi, * pSimLo, * pSimCand;
int k;
+ assert( pObjLo->fPhase == 0 );
+ // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
pSimLi = Ssw_ObjSim( p, pObjLi->Id );
pSimLo = Ssw_ObjSim( p, pObjLo->Id );
- if ( !Aig_IsComplement(pCand) )
+ if ( Aig_Regular(pCand)->fPhase ^ Aig_IsComplement(pCand) )
{
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
- if ( pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
+ if ( ~pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
return 0;
}
else
{
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
- if ( ~pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
+ if ( pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
return 0;
}
return 1;
@@ -233,24 +235,50 @@ int Ssw_SmlCountXorImplication( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * p
{
unsigned * pSimLi, * pSimLo, * pSimCand;
int k, Counter = 0;
+ assert( pObjLo->fPhase == 0 );
+ // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
pSimLi = Ssw_ObjSim( p, pObjLi->Id );
pSimLo = Ssw_ObjSim( p, pObjLo->Id );
- if ( !Aig_IsComplement(pCand) )
+ if ( Aig_Regular(pCand)->fPhase ^ Aig_IsComplement(pCand) )
{
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
- Counter += Aig_WordCountOnes(pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
+ Counter += Aig_WordCountOnes(~pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
}
else
{
for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
- Counter += Aig_WordCountOnes(~pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
+ Counter += Aig_WordCountOnes(pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
}
return Counter;
}
/**Function*************************************************************
+ Synopsis [Counts the number of 1s in the implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlCountEqual( Ssw_Sml_t * p, Aig_Obj_t * pObjLi, Aig_Obj_t * pObjLo )
+{
+ unsigned * pSimLi, * pSimLo;
+ int k, Counter = 0;
+ assert( pObjLo->fPhase == 0 );
+ // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
+ pSimLi = Ssw_ObjSim( p, pObjLi->Id );
+ pSimLo = Ssw_ObjSim( p, pObjLo->Id );
+ for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+ Counter += Aig_WordCountOnes( ~(pSimLi[k] ^ pSimLo[k]) );
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
@@ -273,7 +301,7 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
/**Function*************************************************************
- Synopsis [Counts the number of one's in the patten of the output.]
+ Synopsis [Counts the number of one's in the patten the object.]
Description []
@@ -282,13 +310,55 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ssw_SmlNodeCountOnes( Ssw_Sml_t * p, Aig_Obj_t * pObj )
+int Ssw_SmlNodeCountOnesReal( Ssw_Sml_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i, Counter = 0;
- pSims = Ssw_ObjSim(p, pObj->Id);
+ pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id);
+ if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) )
+ {
+ for ( i = 0; i < p->nWordsTotal; i++ )
+ Counter += Aig_WordCountOnes( ~pSims[i] );
+ }
+ else
+ {
+ for ( i = 0; i < p->nWordsTotal; i++ )
+ Counter += Aig_WordCountOnes( pSims[i] );
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of one's in the patten the object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs )
+{
+ Aig_Obj_t * pObj;
+ unsigned * pSims, uWord;
+ int i, k, Counter = 0;
+ if ( Vec_PtrSize(vObjs) == 0 )
+ return 0;
for ( i = 0; i < p->nWordsTotal; i++ )
- Counter += Aig_WordCountOnes( pSims[i] );
+ {
+ uWord = 0;
+ Vec_PtrForEachEntry( vObjs, pObj, k )
+ {
+ pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id);
+ if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) )
+ uWord |= ~pSims[i];
+ else
+ uWord |= pSims[i];
+ }
+ Counter += Aig_WordCountOnes( uWord );
+ }
return Counter;
}
@@ -889,6 +959,79 @@ p->nSimRounds++;
/**Function*************************************************************
+ Synopsis [Converts simulation information to be not normallized.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlUnnormalize( Ssw_Sml_t * p )
+{
+ Aig_Obj_t * pObj;
+ unsigned * pSims;
+ int i, k;
+ // convert constant 1
+ pSims = Ssw_ObjSim( p, 0 );
+ for ( i = 0; i < p->nWordsFrame; i++ )
+ pSims[i] = ~pSims[i];
+ // convert internal nodes
+ Aig_ManForEachNode( p->pAig, pObj, k )
+ {
+ if ( pObj->fPhase == 0 )
+ continue;
+ pSims = Ssw_ObjSim( p, pObj->Id );
+ for ( i = 0; i < p->nWordsFrame; i++ )
+ pSims[i] = ~pSims[i];
+ }
+ // PIs/POs are always stored in their natural state
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates AIG manager.]
+
+ Description [Assumes that the PI simulation info is attached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pVisited, int nVisCounter )
+{
+// if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
+// return;
+// Aig_ObjSetTravIdCurrent(p->pAig, pObj);
+ if ( pVisited[p->nFrames*pObj->Id+f] == nVisCounter )
+ return;
+ pVisited[p->nFrames*pObj->Id+f] = nVisCounter;
+ if ( Saig_ObjIsPi( p->pAig, pObj ) || Aig_ObjIsConst1(pObj) )
+ return;
+ if ( Saig_ObjIsLo( p->pAig, pObj ) )
+ {
+ if ( f == 0 )
+ return;
+ Ssw_SmlSimulateOneDyn_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1, pVisited, nVisCounter );
+ Ssw_SmlNodeTransferNext( p, Saig_ObjLoToLi(p->pAig, pObj), pObj, f-1 );
+ return;
+ }
+ if ( Saig_ObjIsLi( p->pAig, pObj ) )
+ {
+ Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
+ Ssw_SmlNodeCopyFanin( p, pObj, f );
+ return;
+ }
+ assert( Aig_ObjIsNode(pObj) );
+ Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
+ Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin1(pObj), f, pVisited, nVisCounter );
+ Ssw_SmlNodeSimulate( p, pObj, f );
+}
+
+/**Function*************************************************************
+
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
@@ -974,22 +1117,6 @@ void Ssw_SmlStop( Ssw_Sml_t * p )
free( p );
}
-/**Function*************************************************************
-
- Synopsis [Deallocates simulation manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_SmlNumFrames( Ssw_Sml_t * p )
-{
- return p->nFrames;
-}
-
/**Function*************************************************************
@@ -1051,6 +1178,56 @@ void Ssw_SmlResimulateSeq( Ssw_Sml_t * p )
}
+/**Function*************************************************************
+
+ Synopsis [Returns the number of frames simulated in the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlNumFrames( Ssw_Sml_t * p )
+{
+ return p->nFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the total number of simulation words.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlNumWordsTotal( Ssw_Sml_t * p )
+{
+ return p->nWordsTotal;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the pointer to the simulation info of the node.]
+
+ Description [The simulation info is normalized unless procedure
+ Ssw_SmlUnnormalize() is called in advance.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Ssw_SmlSimInfo( Ssw_Sml_t * p, Aig_Obj_t * pObj )
+{
+ assert( !Aig_IsComplement(pObj) );
+ return Ssw_ObjSim( p, pObj->Id );
+}
+
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-17 16:16:04 +0000