diff options
Diffstat (limited to 'src/aig/ssw')
| -rw-r--r-- | src/aig/ssw/ssw.h | 20 | ||||
| -rw-r--r-- | src/aig/ssw/sswAig.c | 1 | ||||
| -rw-r--r-- | src/aig/ssw/sswClass.c | 6 | ||||
| -rw-r--r-- | src/aig/ssw/sswCore.c | 10 | ||||
| -rw-r--r-- | src/aig/ssw/sswDyn.c | 106 | ||||
| -rw-r--r-- | src/aig/ssw/sswInt.h | 18 | ||||
| -rw-r--r-- | src/aig/ssw/sswIslands.c | 543 | ||||
| -rw-r--r-- | src/aig/ssw/sswMan.c | 5 | ||||
| -rw-r--r-- | src/aig/ssw/sswPart.c | 2 | ||||
| -rw-r--r-- | src/aig/ssw/sswSim.c | 229 |
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************************************************************* |