From 4d71c114a3405f0a2c59a8467c82a8da3f785262 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 21 Sep 2008 08:01:00 -0700 Subject: Version abc80921 --- src/aig/aig/aig.h | 1 + src/aig/aig/aigDfs.c | 27 ++++++ src/aig/dch/dchSat.c | 4 +- src/aig/dch/dchSimSat.c | 11 ++- src/aig/fra/fraSec.c | 19 +++-- src/aig/int/intCtrex.c | 5 +- src/aig/ntl/ntlFraig.c | 8 +- src/aig/ssw/ssw.h | 9 +- src/aig/ssw/sswAig.c | 18 ++-- src/aig/ssw/sswClass.c | 42 ++-------- src/aig/ssw/sswCore.c | 86 +++++++++++++++---- src/aig/ssw/sswInt.h | 50 ++++++----- src/aig/ssw/sswLcorr.c | 172 +++++++++++++++++++++++++++----------- src/aig/ssw/sswMan.c | 23 +++--- src/aig/ssw/sswPairs.c | 2 +- src/aig/ssw/sswSim.c | 215 ++++++++++++++++++++++-------------------------- src/aig/ssw/sswSimSat.c | 210 ++-------------------------------------------- src/aig/ssw/sswSweep.c | 60 ++++++++++---- 18 files changed, 475 insertions(+), 487 deletions(-) (limited to 'src/aig') diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 093912c3..fcaf41fa 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -471,6 +471,7 @@ extern int Aig_ManChoiceLevel( Aig_Man_t * p ); extern int Aig_DagSize( Aig_Obj_t * pObj ); extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj ); extern Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj ); +extern void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp ); extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj ); extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars ); extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 3c6658d9..568d6a68 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -732,6 +732,33 @@ Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj ) return vSupp; } +/**Function************************************************************* + + Synopsis [Counts the support size of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp ) +{ + int i; + Vec_PtrClear( vSupp ); + Aig_ManIncrementTravId( p ); + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + for ( i = 0; i < nObjs; i++ ) + { + assert( !Aig_IsComplement(ppObjs[i]) ); + if ( Aig_ObjIsPo(ppObjs[i]) ) + Aig_Support_rec( p, Aig_ObjFanin0(ppObjs[i]), vSupp ); + else + Aig_Support_rec( p, ppObjs[i], vSupp ); + } +} + /**Function************************************************************* Synopsis [Transfers the AIG from one manager into another.] diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c index 66c7f7b9..07196259 100644 --- a/src/aig/dch/dchSat.c +++ b/src/aig/dch/dchSat.c @@ -50,13 +50,13 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) assert( !Aig_IsComplement(pOld) ); assert( pNew != pOld ); -// p->nCallsSince++; // experiment with this!!! + p->nCallsSince++; // experiment with this!!! // check if SAT solver needs recycling if ( p->pSat == NULL || (p->pPars->nSatVarMax && p->nSatVars > p->pPars->nSatVarMax && - ++p->nCallsSince > p->pPars->nCallsRecycle) ) + p->nCallsSince > p->pPars->nCallsRecycle) ) Dch_ManSatSolverRecycle( p ); // if the nodes do not have SAT variables, allocate them diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c index 7a6865bd..61d2ab93 100644 --- a/src/aig/dch/dchSimSat.c +++ b/src/aig/dch/dchSimSat.c @@ -60,10 +60,10 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) Vec_PtrPush( p->vSimRoots, pObj ); return; } - // pRepr is the representative of the equivalence class - if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pRepr) ) + // pRepr is the representative of an equivalence class + if ( pRepr->fMarkA ) return; - Aig_ObjSetTravIdCurrent(p->pAigTotal, pRepr); + pRepr->fMarkA = 1; Vec_PtrPush( p->vSimClasses, pRepr ); } @@ -80,6 +80,8 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) ***********************************************************************/ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ) { + Aig_Obj_t * pObj; + int i; Vec_PtrClear( p->vSimRoots ); Vec_PtrClear( p->vSimClasses ); Aig_ManIncrementTravId( p->pAigTotal ); @@ -88,6 +90,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 Dch_ManCollectTfoCands_rec( p, pObj2 ); Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease ); Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease ); + Vec_PtrForEachEntry( p->vSimClasses, pObj, i ) + pObj->fMarkA = 0; } /**Function************************************************************* @@ -116,6 +120,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) // get the value from the SAT solver // (account for the fact that some vars may be minimized away) pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum ); +// pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum ); return; } Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) ); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 677123d8..232a789e 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -92,8 +92,6 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ) if ( RetValue >= 0 ) goto finish; - // prepare parameters - Ssw_ManSetDefaultParams( pPars2 ); // prepare parameters memset( pPars, 0, sizeof(Fra_Ssw_t) ); pPars->fLatchCorr = fLatchCorr; @@ -142,7 +140,8 @@ PRT( "Time", clock() - clk ); if ( pParSec->fRetimeFirst && pNew->nRegs ) { clk = clock(); - pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); +// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); + pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 ); Aig_ManStop( pTemp ); if ( pParSec->fVerbose ) { @@ -172,11 +171,21 @@ clk = clock(); goto finish; } } - pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); + + +// pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); +//Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL ); + Ssw_ManSetDefaultParamsLcorr( pPars2 ); + pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 ); + nIter = pPars2->nIters; + + // prepare parameters for scorr + Ssw_ManSetDefaultParams( pPars2 ); + if ( pTemp->pSeqModel ) { if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) ) - printf( "Fra_FraigLatchCorrespondence(): Counter-example verification has FAILED.\n" ); + printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" ); if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) ) printf( "The counter-example is invalid because of phase abstraction.\n" ); else diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c index 5e417ce0..4cbe2007 100644 --- a/src/aig/int/intCtrex.c +++ b/src/aig/int/intCtrex.c @@ -66,7 +66,10 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) break; // transfer to register outputs Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData = Aig_ObjChild0Copy(pObjLi); + pObjLi->pData = Aig_ObjChild0Copy(pObjLi); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; } // create POs for the output of the last frame pObj = Aig_ManPo( pAig, 0 ); diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index b1239e47..27d863af 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -435,6 +435,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe ***********************************************************************/ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) { + Ssw_Pars_t Pars, * pPars = &Pars; Ntl_Man_t * pNew, * pAux; Aig_Man_t * pAig, * pAigCol, * pTemp; @@ -444,7 +445,12 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose ) pAigCol = Ntl_ManCollapseSeq( pNew, 0 ); // perform SCL for the given design - pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 ); +// pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 ); + Ssw_ManSetDefaultParamsLcorr( pPars ); + pPars->nBTLimit = nConfMax; + pPars->fVerbose = fVerbose; + pTemp = Ssw_LatchCorrespondence( pAigCol, pPars ); + Aig_ManStop( pTemp ); if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs ) Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose ); diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 2917f6d4..8d74f16b 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -50,11 +50,12 @@ struct Ssw_Pars_t_ int nBTLimit; // conflict limit at a node int nMinDomSize; // min clock domain considered for optimization int fPolarFlip; // uses polarity adjustment + int fSkipCheck; // do not run equivalence check for unaffected cones int fLatchCorr; // perform register correspondence + // optimized latch correspondence int fLatchCorrOpt; // perform register correspondence (optimized) int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only) - int nCallsRecycle; // calls to perform before recycling SAT solver (optimized latch corr only) - int fSkipCheck; // does not run equivalence check for unaffected cones + int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only) int fVerbose; // verbose stats // internal parameters int nIters; // the number of iterations performed @@ -82,7 +83,9 @@ struct Ssw_Cex_t_ /*=== sswCore.c ==========================================================*/ extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); -extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars ); +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 ); /*=== sswPart.c ==========================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); /*=== sswPairs.c ===================================================*/ diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c index 854a0e12..5a47ba5f 100644 --- a/src/aig/ssw/sswAig.c +++ b/src/aig/ssw/sswAig.c @@ -49,9 +49,9 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, p->nConstrTotal++; assert( pObjRepr->Id < pObj->Id ); // get the new node - pObjNew = Ssw_ObjFraig( p, pObj, iFrame ); + pObjNew = Ssw_ObjFrame( p, pObj, iFrame ); // get the new node of the representative - pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame ); + pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame ); // if this is the same node, no need to add constraints if ( pObj->fPhase == pObjRepr->fPhase ) { @@ -69,7 +69,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, // these are different nodes - perform speculative reduction pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase ); // set the new node - Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 ); + Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 ); // add the constraint Aig_ObjCreatePo( pFrames, pObjNew2 ); Aig_ObjCreatePo( pFrames, pObjNew ); @@ -99,15 +99,15 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames ); // create latches for the first frame Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); // add timeframes p->nConstrTotal = p->nConstrReduced = 0; for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs - Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); Aig_ManForEachPiSeq( p->pAig, pObj, i ) - Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) ); + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) ); // set the constraints on the latch outputs Aig_ManForEachLoSeq( p->pAig, pObj, i ) Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); @@ -115,16 +115,16 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Aig_ManForEachNode( p->pAig, pObj, i ) { pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); - Ssw_ObjSetFraig( p, pObj, f, pObjNew ); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f ); } // transfer latch input to the latch outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) - Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) ); + Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) ); } // add the POs for the latch outputs of the last frame Saig_ManForEachLo( p->pAig, pObj, i ) - Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) ); + Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) ); // remove dangling nodes Aig_ManCleanup( pFrames ); diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index 81e8de8b..db593311 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -286,6 +286,8 @@ int Ssw_ClassesLitNum( Ssw_Cla_t * p ) ***********************************************************************/ Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ) { + if ( p->pId2Class[pRepr->Id] == NULL ) + return NULL; assert( p->pId2Class[pRepr->Id] != NULL ); assert( p->pClassSizes[pRepr->Id] > 1 ); *pnSize = p->pClassSizes[pRepr->Id]; @@ -333,6 +335,7 @@ void Ssw_ClassesCheck( Ssw_Cla_t * p ) Ssw_ManForEachClass( p, ppClass, k ) { pPrev = NULL; + assert( p->pClassSizes[ppClass[0]->Id] >= 2 ); Ssw_ClassForEachNode( p, ppClass[0], pObj, i ) { if ( i == 0 ) @@ -423,12 +426,15 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ) void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t * pRepr, * pTemp; + assert( p->pClassSizes[pObj->Id] == 0 ); assert( p->pId2Class[pObj->Id] == NULL ); pRepr = Aig_ObjRepr( p->pAig, pObj ); assert( pRepr != NULL ); Vec_PtrPush( p->vRefined, pObj ); if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) { + assert( p->pClassSizes[pRepr->Id] == 0 ); + assert( p->pId2Class[pRepr->Id] == NULL ); Aig_ObjSetRepr( p->pAig, pObj, NULL ); p->nCands1--; return; @@ -439,7 +445,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ) assert( p->pClassSizes[pRepr->Id] >= 2 ); if ( p->pClassSizes[pRepr->Id] == 2 ) { - p->pId2Class[pObj->Id] = NULL; + p->pId2Class[pRepr->Id] = NULL; p->nClasses--; p->pClassSizes[pRepr->Id] = 0; p->nLits--; @@ -491,7 +497,7 @@ PRT( "Simulation of 32 frames with 4 words", clock() - clk ); // set comparison procedures clk = clock(); - Ssw_ClassesSetData( p, pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); + Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); // allocate the hash table hashing simulation info into nodes nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 ); @@ -591,38 +597,6 @@ PRT( "Collecting candidate equival classes", clock() - clk ); return p; } -/**Function************************************************************* - - Synopsis [Returns 1 if the node appears to be constant 1 candidate.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj ) -{ - return pObj->fPhase == pObj->fMarkB; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the nodes appear equal.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) -{ - return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB); -} - /**Function************************************************************* Synopsis [Creates initial simulation classes.] diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 6a3e9264..fc9f5672 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -50,16 +50,35 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->nBTLimit = 1000; // conflict limit at a node p->nMinDomSize = 100; // min clock domain considered for optimization p->fPolarFlip = 0; // uses polarity adjustment + p->fSkipCheck = 0; // do not run equivalence check for unaffected cones p->fLatchCorr = 0; // performs register correspondence p->fVerbose = 0; // verbose stats // latch correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence - p->nSatVarMax = 5000; // the max number of SAT variables - p->nCallsRecycle = 100; // calls to perform before recycling SAT solver + p->nSatVarMax = 1000; // the max number of SAT variables + p->nRecycleCalls = 50; // calls to perform before recycling SAT solver // return values p->nIters = 0; // the number of iterations performed } +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p ) +{ + Ssw_ManSetDefaultParams( p ); + p->fLatchCorrOpt = 1; + p->nBTLimit = 10000; +} + /**Function************************************************************* Synopsis [Performs computation of signal correspondence with constraints.] @@ -73,6 +92,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) ***********************************************************************/ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) { + int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal; Aig_Man_t * pAigNew; int RetValue, nIter; int clk, clkTotal = clock(); @@ -97,23 +117,40 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) Ssw_ClassesPrint( p->ppClasses, 0 ); } // refine classes using induction + nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0; for ( nIter = 0; ; nIter++ ) { clk = clock(); if ( p->pPars->fLatchCorrOpt ) + { RetValue = Ssw_ManSweepLatch( p ); + if ( p->pPars->fVerbose ) + { + printf( "%3d : Const = %6d. Cl = %6d. Pr = %5d. Cex = %5d. Rcl = %3d. F = %3d. ", + nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), + p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, + p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal ); + PRT( "T", clock() - clk ); + nSatProof = p->nSatProof; + nSatCallsSat = p->nSatCallsSat; + nRecycles = p->nRecycles; + nSatFailsReal = p->nSatFailsReal; + } + } else - RetValue = Ssw_ManSweep( p ); - if ( p->pPars->fVerbose ) { - printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", - nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), - p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal ); - if ( p->pPars->fSkipCheck ) - printf( "Use = %5d. Skip = %5d. ", - p->nRefUse, p->nRefSkip ); - PRT( "T", clock() - clk ); - } + RetValue = Ssw_ManSweep( p ); + if ( p->pPars->fVerbose ) + { + printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", + nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), + p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal ); + if ( p->pPars->fSkipCheck ) + printf( "Use = %5d. Skip = %5d. ", + p->nRefUse, p->nRefSkip ); + PRT( "T", clock() - clk ); + } + } Ssw_ManCleanup( p ); if ( !RetValue ) break; @@ -161,7 +198,10 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) } // check and update parameters if ( pPars->fLatchCorrOpt ) + { pPars->fLatchCorr = 1; + pPars->nFramesAddSim = 0; + } else { assert( pPars->nFramesK > 0 ); @@ -181,13 +221,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // perform one round of seq simulation and generate candidate equivalence classes p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); } else { // create trivial equivalence classes with all nodes being candidates for constant 1 p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); - Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); + Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit ); } // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); @@ -196,6 +236,24 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) return pAigNew; } +/**Function************************************************************* + + Synopsis [Performs computation of latch correspondence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +{ + Ssw_Pars_t Pars; + if ( pPars == NULL ) + Ssw_ManSetDefaultParamsLcorr( pPars = &Pars ); + return Ssw_SignalCorrespondence( pAig, pPars ); +} //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 5b4377c7..faa3a87d 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -53,25 +53,31 @@ struct Ssw_Man_t_ // AIGs used in the package Aig_Man_t * pAig; // user-given AIG Aig_Man_t * pFrames; // final AIG - Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes + Aig_Obj_t ** pNodeToFrames; // mapping of AIG nodes into FRAIG nodes // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes of nodes int fRefined; // is set to 1 when refinement happens - int nRefUse; - int nRefSkip; + int nRefUse; // the number of equivalences used + int nRefSkip; // the number of equivalences skipped // SAT solving sat_solver * pSat; // recyclable SAT solver int nSatVars; // the counter of SAT variables int * pSatVars; // mapping of each node into its SAT var int nSatVarsTotal; // the total number of SAT vars created Vec_Ptr_t * vFanins; // fanins of the CNF node - Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate - Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate // SAT solving (latch corr only) - int nCallsSince; // the number of calls since last recycling - int nRecycles; // the number of time SAT solver was recycled Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables Vec_Ptr_t * vUsedPis; // the PIs with SAT variables + Vec_Ptr_t * vSimInfo; // simulation information for the framed PIs + int nPatterns; // the number of patterns saved + int nSimRounds; // the number of simulation rounds performed + int nCallsCount; // the number of calls in this round + int nCallsDelta; // the number of calls to skip + int nCallsSat; // the number of SAT calls in this round + int nCallsUnsat; // the number of UNSAT calls in this round + int nRecycleCalls; // the number of calls since last recycling + int nRecycles; // the number of time SAT solver was recycled + int nConeMax; // the maximum cone size // sequential simulator Ssw_Sml_t * pSml; // counter example storage @@ -125,11 +131,11 @@ static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); } -static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFraig[p->nFrames*pObj->Id + i]; } -static inline void Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; } +static inline Aig_Obj_t * Ssw_ObjFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFrames[p->nFrames*pObj->Id + i]; } +static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFrames[p->nFrames*pObj->Id + i] = pNode; } -static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } -static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; } +static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -161,8 +167,6 @@ 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 ); extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ); -extern int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj ); -extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); /*=== sswCnf.c ===================================================*/ extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); /*=== sswCore.c ===================================================*/ @@ -178,19 +182,23 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p ); extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== sswSim.c ===================================================*/ +extern unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ); +extern int Ssw_SmlObjIsConstWord( 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 int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj ); +extern int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); 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 Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); -extern unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj ); -extern int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj ); -extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +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 ); /*=== sswSimSat.c ===================================================*/ -extern int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ); -extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); -extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); -extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ); +extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ); +extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c index dcc4f245..cde9b0c9 100644 --- a/src/aig/ssw/sswLcorr.c +++ b/src/aig/ssw/sswLcorr.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "sswInt.h" -#include "bar.h" +//#include "bar.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -67,12 +67,13 @@ void Ssw_ManSatSolverRecycle( Ssw_Man_t * p ) Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ ); p->nRecycles++; - p->nCallsSince = 0; + p->nRecycleCalls = 0; } + /**Function************************************************************* - Synopsis [Copy pattern from the solver into the internal storage.] + Synopsis [Tranfers simulation information from FRAIG to AIG.] Description [] @@ -81,19 +82,30 @@ void Ssw_ManSatSolverRecycle( Ssw_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Ssw_SmlSavePatternLatch( Ssw_Man_t * p ) +void Ssw_ManSweepTransfer( Ssw_Man_t * p ) { - Aig_Obj_t * pObj; + Aig_Obj_t * pObj, * pObjFraig; + unsigned * pInfo; int i; - memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + // transfer simulation information Aig_ManForEachPi( p->pAig, pObj, i ) - if ( Ssw_ManOriginalPiValue( p, pObj, 0 ) ) - Aig_InfoSetBit( p->pPatWords, i ); + { + pObjFraig = Ssw_ObjFrame( p, pObj, 0 ); + if ( pObjFraig == Aig_ManConst0(p->pFrames) ) + { + Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 ); + continue; + } + assert( !Aig_IsComplement(pObjFraig) ); + assert( Aig_ObjIsPi(pObjFraig) ); + pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); + } } /**Function************************************************************* - Synopsis [Copy pattern from the solver into the internal storage.] + Synopsis [Performs one round of simulation with counter-examples.] Description [] @@ -102,14 +114,50 @@ void Ssw_SmlSavePatternLatch( Ssw_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Ssw_SmlSavePatternLatchPhase( Ssw_Man_t * p, int f ) +int Ssw_ManSweepResimulate( Ssw_Man_t * p ) +{ + int RetValue1, RetValue2, clk = clock(); + // transfer PI simulation information from storage + Ssw_ManSweepTransfer( p ); + // simulate internal nodes + Ssw_SmlSimulateOneFrame( p->pSml ); + // check equivalence classes + RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 ); + RetValue2 = Ssw_ClassesRefine( p->ppClasses, 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 [Saves one counter-example into internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand ) { Aig_Obj_t * pObj; - int i; - memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Aig_ManForEachPi( p->pAig, pObj, i ) - if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) ) - Aig_InfoSetBit( p->pPatWords, i ); + unsigned * pInfo; + int i, nVarNum, Value; + Vec_PtrForEachEntry( p->vUsedPis, pObj, i ) + { + nVarNum = Ssw_ObjSatNum( p, pObj ); + assert( nVarNum > 0 ); + Value = sat_solver_var_value( p->pSat, nVarNum ); + if ( Value == 0 ) + continue; + pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); + Aig_InfoSetBit( pInfo, p->nPatterns ); + } } /**Function************************************************************* @@ -127,13 +175,13 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t * pObjNew; assert( !Aig_IsComplement(pObj) ); - if ( Ssw_ObjFraig( p, pObj, 0 ) ) + if ( Ssw_ObjFrame( p, pObj, 0 ) ) return; assert( Aig_ObjIsNode(pObj) ); Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObj) ); Ssw_ManBuildCone_rec( p, Aig_ObjFanin1(pObj) ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) ); - Ssw_ObjSetFraig( p, pObj, 0, pObjNew ); + Ssw_ObjSetFrame( p, pObj, 0, pObjNew ); } /**Function************************************************************* @@ -149,10 +197,18 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) ***********************************************************************/ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj ) { - Aig_Obj_t * pObjFraig, * pObjFraig2, * pObjReprFraig, * pObjLi; - int RetValue; + Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi; + int RetValue, clk; assert( Aig_ObjIsPi(pObj) ); assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) ); + // check if it makes sense to skip some calls + if ( p->nCallsCount > 100 && p->nCallsUnsat < p->nCallsSat ) + { + if ( ++p->nCallsDelta < 0 ) + return; + } + p->nCallsDelta = 0; +clk = clock(); // get the fraiged node pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) ); @@ -165,43 +221,44 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 ); } else - pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, 0 ); + pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 ); +p->timeReduce += clock() - clk; // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) return; - p->nCallsSince++; + p->nRecycleCalls++; + p->nCallsCount++; + // check equivalence of the two nodes if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ) { + p->nPatterns++; p->nStrangers++; - Ssw_SmlSavePatternLatchPhase( p, 0 ); + p->fRefined = 1; } else { RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); - if ( RetValue == 1 ) // proved equivalent + if ( RetValue == 1 ) // proved equivalence { - pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); - Ssw_ObjSetFraig( p, pObj, 0, pObjFraig2 ); + p->nCallsUnsat++; return; } - else if ( RetValue == -1 ) // timed out + if ( RetValue == -1 ) // timed out { Ssw_ClassesRemoveNode( p->ppClasses, pObj ); + p->nCallsUnsat++; p->fRefined = 1; return; } - else // disproved the equivalence + else // disproved equivalence { - Ssw_SmlSavePatternLatch( p ); + Ssw_SmlAddPattern( p, pObjRepr, pObj ); + p->nPatterns++; + p->nCallsSat++; + p->fRefined = 1; } } - if ( p->pPars->nConstrs == 0 ) - Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, 0 ); - else - Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, 0 ); - assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); - p->fRefined = 1; } /**Function************************************************************* @@ -217,7 +274,7 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj ***********************************************************************/ int Ssw_ManSweepLatch( Ssw_Man_t * p ) { - Bar_Progress_t * pProgress = NULL; +// Bar_Progress_t * pProgress = NULL; Vec_Ptr_t * vClass; Aig_Obj_t * pObj, * pRepr, * pTemp; int i, k; @@ -225,30 +282,40 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) // start the timeframe p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) ); // map constants and PIs - Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) ); + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) ); // implement equivalence classes Saig_ManForEachLo( p->pAig, pObj, i ) { pRepr = Aig_ObjRepr( p->pAig, pObj ); if ( pRepr == NULL ) + { pTemp = Aig_ObjCreatePi(p->pFrames); + pTemp->pData = pObj; + } else - pTemp = Aig_NotCond( Ssw_ObjFraig(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase ); - Ssw_ObjSetFraig( p, pObj, 0, pTemp ); + pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase ); + Ssw_ObjSetFrame( p, pObj, 0, pTemp ); } + Aig_ManSetPioNumbers( p->pFrames ); + + // prepare simulation info + assert( p->vSimInfo == NULL ); + p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 ); + Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 ); // go through the registers - if ( p->pPars->fVerbose ) - pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) ); +// if ( p->pPars->fVerbose ) +// pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) ); vClass = Vec_PtrAlloc( 100 ); p->fRefined = 0; + p->nCallsCount = p->nCallsSat = p->nCallsUnsat = 0; Saig_ManForEachLo( p->pAig, pObj, i ) { - if ( p->pPars->fVerbose ) - Bar_ProgressUpdate( pProgress, i, NULL ); +// if ( p->pPars->fVerbose ) +// Bar_ProgressUpdate( pProgress, i, NULL ); // consider the case of constant candidate if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj ); @@ -261,21 +328,32 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) // try to prove equivalences in this class Vec_PtrForEachEntry( vClass, pTemp, k ) if ( Aig_ObjRepr(p->pAig, pTemp) == pObj ) + { Ssw_ManSweepLatchOne( p, pObj, pTemp ); + if ( p->nPatterns == 32 ) + break; + } } + // resimulate + if ( p->nPatterns == 32 ) + Ssw_ManSweepResimulate( p ); // attempt recycling the SAT solver if ( p->pPars->nSatVarMax && p->nSatVars > p->pPars->nSatVarMax && - p->nCallsSince > p->pPars->nCallsRecycle ) + p->nRecycleCalls > p->pPars->nRecycleCalls ) Ssw_ManSatSolverRecycle( p ); } + // resimulate + if ( p->nPatterns > 0 ) + Ssw_ManSweepResimulate( p ); + // cleanup Vec_PtrFree( vClass ); p->nSatFailsTotal += p->nSatFailsReal; - if ( p->pPars->fVerbose ) - Bar_ProgressStop( pProgress ); +// if ( p->pPars->fVerbose ) +// Bar_ProgressStop( pProgress ); // cleanup - Ssw_ClassesCheck( p->ppClasses ); +// Ssw_ClassesCheck( p->ppClasses ); return p->fRefined; } diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index 33c716ce..8d2c8c24 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -52,12 +52,10 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) p->pPars = pPars; p->pAig = pAig; p->nFrames = pPars->nFramesK + 1; - p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); // SAT solving p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) ); p->vFanins = Vec_PtrAlloc( 100 ); - p->vSimRoots = Vec_PtrAlloc( 1000 ); - p->vSimClasses = Vec_PtrAlloc( 1000 ); // SAT solving (latch corr only) p->vUsedNodes = Vec_PtrAlloc( 1000 ); p->vUsedPis = Vec_PtrAlloc( 1000 ); @@ -102,13 +100,15 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) { double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); - printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", - p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory ); + printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n", + p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory ); printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), p->nSatVarsTotal/p->pPars->nIters ); printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n", p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers ); + printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n", + p->nSatVars, p->nConeMax, p->nRecycles, p->nSimRounds ); printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); @@ -139,12 +139,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) ***********************************************************************/ void Ssw_ManCleanup( Ssw_Man_t * p ) { - Aig_ManCleanMarkB( p->pAig ); if ( p->pFrames ) { Aig_ManStop( p->pFrames ); p->pFrames = NULL; - memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); + memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); } if ( p->pSat ) { @@ -154,6 +153,11 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) p->pSat = NULL; memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) ); } + if ( p->vSimInfo ) + { + Vec_PtrFree( p->vSimInfo ); + p->vSimInfo = NULL; + } p->nConstrTotal = 0; p->nConstrReduced = 0; } @@ -172,6 +176,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) void Ssw_ManStop( Ssw_Man_t * p ) { Aig_ManCleanMarkA( p->pAig ); + Aig_ManCleanMarkB( p->pAig ); if ( p->pPars->fVerbose ) Ssw_ManPrintStats( p ); if ( p->ppClasses ) @@ -179,11 +184,9 @@ void Ssw_ManStop( Ssw_Man_t * p ) if ( p->pSml ) Ssw_SmlStop( p->pSml ); Vec_PtrFree( p->vFanins ); - Vec_PtrFree( p->vSimRoots ); - Vec_PtrFree( p->vSimClasses ); Vec_PtrFree( p->vUsedNodes ); Vec_PtrFree( p->vUsedPis ); - FREE( p->pNodeToFraig ); + FREE( p->pNodeToFrames ); FREE( p->pSatVars ); FREE( p->pPatWords ); free( p ); diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c index a11bdf98..c77ad30d 100644 --- a/src/aig/ssw/sswPairs.c +++ b/src/aig/ssw/sswPairs.c @@ -289,7 +289,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA // create equivalence classes using these IDs p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses ); p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord ); // perform refinement of classes pAigNew = Ssw_SignalCorrespondenceRefine( p ); // cleanup diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index 769e923c..ba8ad247 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -57,7 +57,7 @@ static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRa SeeAlso [] ***********************************************************************/ -unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj ) +unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ) { static int s_SPrimes[128] = { 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, @@ -96,7 +96,7 @@ unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj ) +int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i; @@ -118,7 +118,7 @@ int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) { unsigned * pSims0, * pSims1; int i; @@ -130,6 +130,39 @@ int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) return 1; } +/**Function************************************************************* + + Synopsis [Returns 1 if the node appears to be constant 1 candidate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj ) +{ + return pObj->fPhase == pObj->fMarkB; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the nodes appear equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) +{ + return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB); +} + + /**Function************************************************************* Synopsis [Counts the number of 1s in the XOR of simulation data.] @@ -340,7 +373,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p ) assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); Aig_ManForEachPo( p->pAig, pObj, i ) { - if ( !Ssw_SmlNodeIsConst( p, Aig_ObjFanin0(pObj) ) ) + if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) ) { // create the counter-example from this pattern return Ssw_SmlCheckOutputSavePattern( p, pObj ); @@ -404,7 +437,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) SeeAlso [] ***********************************************************************/ -void Ssw_SmlAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ) +void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ) { unsigned * pSims; int i; @@ -414,6 +447,25 @@ void Ssw_SmlAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram pSims[i] = fConst1? ~(unsigned)0 : 0; } +/**Function************************************************************* + + Synopsis [Assigns constant patterns to the PI node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame ) +{ + unsigned * pSims; + assert( Aig_ObjIsPi(pObj) ); + pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; + pSims[iWord] = Word; +} + /**Function************************************************************* Synopsis [Assings random simulation info for the PIs.] @@ -438,7 +490,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit ) Ssw_SmlAssignRandom( p, pObj ); // assign the initial state for the latches Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_SmlAssignConst( p, pObj, 0, 0 ); + Ssw_SmlObjAssignConst( p, pObj, 0, 0 ); } else { @@ -467,7 +519,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) { // copy the PI info Aig_ManForEachPi( p->pAig, pObj, i ) - Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); + Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); // flip one bit Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); for ( i = 0; i < Limit; i++ ) @@ -481,11 +533,11 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig); for ( f = 0; f < p->nFrames; f++ ) Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f ); + Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f ); // copy the latch info k = 0; Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); + Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); // assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pFrames) ); // flip one bit of the last frame @@ -517,7 +569,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ) // copy the pattern into the primary inputs Aig_ManForEachPi( p->pAig, pObj, i ) - Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); + Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 ); // set distance one PIs for the first frame Limit = AIG_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 ); @@ -530,7 +582,6 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ) Ssw_SmlAssignRandomFrame( p, pObj, f ); } - /**Function************************************************************* Synopsis [Simulates one node.] @@ -746,46 +797,39 @@ p->timeSim += clock() - clk; p->nSimRounds++; } - -#if 0 - /**Function************************************************************* - Synopsis [Resimulates fraiging manager after finding a counter-example.] + Synopsis [Simulates AIG manager.] - Description [] + Description [Assumes that the PI simulation info is attached.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Ssw_SmlResimulate( Ssw_Man_t * p ) +void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p ) { - int nChanges, clk; - Ssw_SmlAssignDist1( p, p->pPatWords ); - Ssw_SmlSimulateOne( p ); -// if ( p->pPars->fPatScores ) -// Ssw_CleanPatScores( p ); - if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) - return; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, clk; clk = clock(); - nChanges = Ssw_ClassesRefine( p->pCla, 1 ); - nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); - if ( p->pCla->vImps ) - nChanges += Ssw_ImpRefineUsingCex( p, p->pCla->vImps ); - if ( p->vOneHots ) - nChanges += Ssw_OneHotRefineUsingCex( p, p->vOneHots ); -p->timeRef += clock() - clk; - if ( !p->pPars->nFramesK && nChanges < 1 ) - printf( "Error: A counter-example did not refine classes!\n" ); -// assert( nChanges >= 1 ); -//printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges ); + // simulate the nodes + Aig_ManForEachNode( p->pAig, pObj, i ) + Ssw_SmlNodeSimulate( p, pObj, 0 ); + // copy simulation info into outputs + Saig_ManForEachLi( p->pAig, pObj, i ) + Ssw_SmlNodeCopyFanin( p, pObj, 0 ); + // copy simulation info into the inputs + Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) + Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 ); +p->timeSim += clock() - clk; +p->nSimRounds++; } + /**Function************************************************************* - Synopsis [Performs simulation of the manager.] + Synopsis [Allocates simulation manager.] Description [] @@ -794,69 +838,19 @@ p->timeRef += clock() - clk; SeeAlso [] ***********************************************************************/ -void Ssw_SmlSimulate( Ssw_Man_t * p, int fInit ) +Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ) { - int fVerbose = 0; - int nChanges, nClasses, clk; - assert( !fInit || Aig_ManRegNum(p->pAig) ); - // start the classes - Ssw_SmlInitialize( p, fInit ); - Ssw_SmlSimulateOne( p ); - if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) - return; - Ssw_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 ); -// Ssw_ClassesPrint( p->pCla, 0 ); -if ( fVerbose ) -printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Ssw_ClassesCountLits(p->pCla) ); - -//return; - - // refine classes by walking 0/1 patterns - Ssw_SmlSavePattern0( p, fInit ); - Ssw_SmlAssignDist1( p, p->pPatWords ); - Ssw_SmlSimulateOne( p ); - if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) - return; -clk = clock(); - nChanges = Ssw_ClassesRefine( p->pCla, 1 ); - nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); -p->timeRef += clock() - clk; -if ( fVerbose ) -printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) ); - Ssw_SmlSavePattern1( p, fInit ); - Ssw_SmlAssignDist1( p, p->pPatWords ); - Ssw_SmlSimulateOne( p ); - if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) - return; -clk = clock(); - nChanges = Ssw_ClassesRefine( p->pCla, 1 ); - nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); -p->timeRef += clock() - clk; - -if ( fVerbose ) -printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) ); - // refine classes by random simulation - do { - Ssw_SmlInitialize( p, fInit ); - Ssw_SmlSimulateOne( p ); - nClasses = Vec_PtrSize(p->pCla->vClasses); - if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) ) - return; -clk = clock(); - nChanges = Ssw_ClassesRefine( p->pCla, 1 ); - nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL ); -p->timeRef += clock() - clk; -if ( fVerbose ) -printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) ); - } while ( (double)nChanges / nClasses > p->pPars->dSimSatur ); - -// if ( p->pPars->fVerbose ) -// printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", -// Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Ssw_ClassesCountLits(p->pCla) ); -// Ssw_ClassesPrint( p->pCla, 0 ); + Ssw_Sml_t * p; + p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame ); + memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); + p->pAig = pAig; + p->nPref = nPref; + p->nFrames = nPref + nFrames; + p->nWordsFrame = nWordsFrame; + p->nWordsTotal = (nPref + nFrames) * nWordsFrame; + p->nWordsPref = nPref * nWordsFrame; + return p; } - -#endif /**Function************************************************************* @@ -869,18 +863,9 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize( SeeAlso [] ***********************************************************************/ -Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ) +void Ssw_SmlClean( Ssw_Sml_t * p ) { - Ssw_Sml_t * p; - p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame ); - memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); - p->pAig = pAig; - p->nPref = nPref; - p->nFrames = nPref + nFrames; - p->nWordsFrame = nWordsFrame; - p->nWordsTotal = (nPref + nFrames) * nWordsFrame; - p->nWordsPref = nPref * nWordsFrame; - return p; + memset( p->pData, 0, sizeof(unsigned) * Aig_ManObjNumMax(p->pAig) * p->nWordsTotal ); } /**Function************************************************************* @@ -1005,11 +990,11 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) // assign simulation info for the registers iBit = 0; Saig_ManForEachLo( pAig, pObj, i ) - Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); + Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); // assign simulation info for the primary inputs for ( i = 0; i <= p->iFrame; i++ ) Saig_ManForEachPi( pAig, pObj, k ) - Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); + Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); assert( iBit == p->nBits ); // run random simulation Ssw_SmlSimulateOne( pSml ); @@ -1042,11 +1027,11 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) // assign simulation info for the registers iBit = 0; Saig_ManForEachLo( pAig, pObj, i ) - Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); + Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); // assign simulation info for the primary inputs for ( i = 0; i <= p->iFrame; i++ ) Saig_ManForEachPi( pAig, pObj, k ) - Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); + Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); assert( iBit == p->nBits ); // run random simulation Ssw_SmlSimulateOne( pSml ); @@ -1271,13 +1256,13 @@ int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p ) // assign simulation info for the registers iBit = 0; Saig_ManForEachLo( pAig, pObj, i ) -// Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - Ssw_SmlAssignConst( pSml, pObj, 0, 0 ); +// Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); + Ssw_SmlObjAssignConst( pSml, pObj, 0, 0 ); // assign simulation info for the primary inputs iBit = p->nRegs; for ( i = 0; i <= p->iFrame; i++ ) Saig_ManForEachPi( pAig, pObj, k ) - Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); + Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); assert( iBit == p->nBits ); // run random simulation Ssw_SmlSimulateOne( pSml ); diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c index 715750ca..c85b8bcf 100644 --- a/src/aig/ssw/sswSimSat.c +++ b/src/aig/ssw/sswSimSat.c @@ -28,157 +28,6 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Collects internal nodes in the reverse DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManCollectTfoCands_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) -{ - Aig_Obj_t * pFanout, * pRepr; - int iFanout = -1, i; - assert( !Aig_IsComplement(pObj) ); - if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) ) - return; - Aig_ObjSetTravIdCurrent(p->pAig, pObj); - // traverse the fanouts - Aig_ObjForEachFanout( p->pAig, pObj, pFanout, iFanout, i ) - Ssw_ManCollectTfoCands_rec( p, pFanout ); - // check if the given node has a representative - pRepr = Aig_ObjRepr( p->pAig, pObj ); - if ( pRepr == NULL ) - return; - // pRepr is the constant 1 node - if ( pRepr == Aig_ManConst1(p->pAig) ) - { - Vec_PtrPush( p->vSimRoots, pObj ); - return; - } - // pRepr is the representative of the equivalence class - if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) ) - return; - Aig_ObjSetTravIdCurrent(p->pAig, pRepr); - Vec_PtrPush( p->vSimClasses, pRepr ); -} - -/**Function************************************************************* - - Synopsis [Collect equivalence classes and const1 cands in the TFO.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ) -{ - Vec_PtrClear( p->vSimRoots ); - Vec_PtrClear( p->vSimClasses ); - Aig_ManIncrementTravId( p->pAig ); - Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) ); - Ssw_ManCollectTfoCands_rec( p, pObj1 ); - Ssw_ManCollectTfoCands_rec( p, pObj2 ); - Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease ); - Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease ); -} - -/**Function************************************************************* - - Synopsis [Retrives value of the PI in the original AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) -{ - Aig_Obj_t * pObjFraig; - int nVarNum, Value; - assert( Aig_ObjIsPi(pObj) ); - pObjFraig = Ssw_ObjFraig( p, pObj, f ); - nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) ); - Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); - if ( p->pPars->fPolarFlip ) - { - if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1; - } -/* - if ( nVarNum==0 ) - printf( "x" ); - else if ( Value == 0 ) - printf( "0" ); - else - printf( "1" ); -*/ - return Value; -} - -/**Function************************************************************* - - Synopsis [Resimulates the cone of influence of the solved nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) -{ - if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) ) - return; - Aig_ObjSetTravIdCurrent(p->pAig, pObj); - if ( Aig_ObjIsPi(pObj) ) - { - pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f ); - return; - } - Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f ); - Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj), f ); - pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) - & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Resimulates the cone of influence of the other nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) -{ - if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) ) - return; - Aig_ObjSetTravIdCurrent(p->pAig, pObj); - if ( Aig_ObjIsPi(pObj) ) - { - // set random value - pObj->fMarkB = Aig_ManRandom(0) & 1; - return; - } - Ssw_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) ); - Ssw_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) ); - pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) - & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); -} - /**Function************************************************************* Synopsis [Handle the counter-example.] @@ -190,52 +39,7 @@ void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ) -{ - Aig_Obj_t * pRoot, ** ppClass; - int i, k, nSize, RetValue1, RetValue2, clk = clock(); - // get the equivalence classes - Ssw_ManCollectTfoCands( p, pObj, pRepr ); - // resimulate the cone of influence of the solved nodes - Aig_ManIncrementTravId( p->pAig ); - Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) ); - Ssw_ManResimulateSolved_rec( p, pObj, f ); - Ssw_ManResimulateSolved_rec( p, pRepr, f ); - // resimulate the cone of influence of the other nodes - Vec_PtrForEachEntry( p->vSimRoots, pRoot, i ) - Ssw_ManResimulateOther_rec( p, pRoot ); - // refine these nodes - RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 ); - // resimulate the cone of influence of the cand classes - RetValue2 = 0; - Vec_PtrForEachEntry( p->vSimClasses, pRoot, i ) - { - ppClass = Ssw_ClassesReadClass( p->ppClasses, pRoot, &nSize ); - for ( k = 0; k < nSize; k++ ) - Ssw_ManResimulateOther_rec( p, ppClass[k] ); - // refine this class - RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRoot, 0 ); - } - // make sure refinement happened - if ( Aig_ObjIsConst1(pRepr) ) - assert( RetValue1 ); - else - assert( RetValue2 ); -p->timeSimSat += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [Handle the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ) +void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr ) { Aig_Obj_t * pObj; int i, RetValue1, RetValue2, clk = clock(); @@ -255,18 +59,17 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR { assert( RetValue1 ); if ( RetValue1 == 0 ) - printf( "\nSsw_ManResimulateCexTotal() Error: RetValue1 does not hold.\n" ); + printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" ); } else { assert( RetValue2 ); if ( RetValue2 == 0 ) - printf( "\nSsw_ManResimulateCexTotal() Error: RetValue2 does not hold.\n" ); + printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" ); } p->timeSimSat += clock() - clk; } - /**Function************************************************************* Synopsis [Handle the counter-example.] @@ -278,7 +81,7 @@ p->timeSimSat += clock() - clk; SeeAlso [] ***********************************************************************/ -void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ) +void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ) { int RetValue1, RetValue2, clk = clock(); // set the PI simulation information @@ -293,18 +96,17 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * { assert( RetValue1 ); if ( RetValue1 == 0 ) - printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue1 does not hold.\n" ); + printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" ); } else { assert( RetValue2 ); if ( RetValue2 == 0 ) - printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue2 does not hold.\n" ); + printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" ); } p->timeSimSat += clock() - clk; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 1cf4b81b..9330dafa 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -76,6 +76,33 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p ) pObjLo->fMarkA |= pObjLi->fMarkA; } +/**Function************************************************************* + + Synopsis [Retrives value of the PI in the original AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) +{ + Aig_Obj_t * pObjFraig; + int nVarNum, Value; + assert( Aig_ObjIsPi(pObj) ); + pObjFraig = Ssw_ObjFrame( p, pObj, f ); + nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) ); + Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); +// Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum )); + if ( p->pPars->fPolarFlip ) + { + if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1; + } + return Value; +} + /**Function************************************************************* Synopsis [Copy pattern from the solver into the internal storage.] @@ -114,7 +141,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f ) int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); Aig_ManForEachPi( p->pAig, pObj, i ) - if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) ) + if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) ) Aig_InfoSetBit( p->pPatWords, i ); } @@ -138,9 +165,9 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) if ( pObjRepr == NULL ) return; // get the fraiged node - pObjFraig = Ssw_ObjFraig( p, pObj, f ); + pObjFraig = Ssw_ObjFrame( p, pObj, f ); // get the fraiged representative - pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f ); + pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f ); // check if constant 0 pattern distinquishes these nodes assert( pObjFraig != NULL && pObjReprFraig != NULL ); if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ) @@ -168,7 +195,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) if ( RetValue == 1 ) // proved equivalent { pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); - Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 ); + Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 ); return; } if ( RetValue == -1 ) // timed out @@ -181,16 +208,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA ) { assert( 0 ); - printf( "\nMistake!!!\n" ); + printf( "\nSsw_ManSweepNode(): Error!\n" ); } // disproved the equivalence Ssw_SmlSavePatternAig( p, f ); } -// Ssw_ManResimulateCex( p, pObj, pObjRepr, f ); if ( p->pPars->nConstrs == 0 ) - Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f ); + Ssw_ManResimulateWord( p, pObj, pObjRepr, f ); else - Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f ); + Ssw_ManResimulateBit( p, pObj, pObjRepr ); assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr ); p->fRefined = 1; } @@ -216,7 +242,7 @@ clk = clock(); // start initialized timeframes p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_ObjSetFraig( p, pObj, 0, Aig_ManConst0(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) ); // sweep internal nodes p->fRefined = 0; @@ -226,16 +252,16 @@ clk = clock(); for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs - Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); - Ssw_ObjSetFraig( p, pObj, f, pObjNew ); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_ManSweepNode( p, pObj, f, 1 ); } // quit if this is the last timeframe @@ -246,7 +272,7 @@ clk = clock(); Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) { pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f); - Ssw_ObjSetFraig( p, pObjLo, f+1, pObjNew ); + Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew ); Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) ); } } @@ -307,12 +333,12 @@ p->timeMarkCones += clock() - clk; // map constants and PIs of the last frame f = p->pPars->nFramesK; - Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); // make sure LOs are assigned Saig_ManForEachLo( p->pAig, pObj, i ) - assert( Ssw_ObjFraig( p, pObj, f ) != NULL ); + assert( Ssw_ObjFrame( p, pObj, f ) != NULL ); // sweep internal nodes p->fRefined = 0; p->nSatFailsReal = 0; @@ -330,7 +356,7 @@ p->timeMarkCones += clock() - clk; { pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA; pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); - Ssw_ObjSetFraig( p, pObj, f, pObjNew ); + Ssw_ObjSetFrame( p, pObj, f, pObjNew ); Ssw_ManSweepNode( p, pObj, f, 0 ); } } -- cgit v1.2.3