diff options
Diffstat (limited to 'src/aig/ssw_old/sswLcorr.c')
-rw-r--r-- | src/aig/ssw_old/sswLcorr.c | 364 |
1 files changed, 364 insertions, 0 deletions
diff --git a/src/aig/ssw_old/sswLcorr.c b/src/aig/ssw_old/sswLcorr.c new file mode 100644 index 00000000..cde9b0c9 --- /dev/null +++ b/src/aig/ssw_old/sswLcorr.c @@ -0,0 +1,364 @@ +/**CFile**************************************************************** + + FileName [sswLcorr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Latch correspondence.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswLcorr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" +//#include "bar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Recycles the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSatSolverRecycle( Ssw_Man_t * p ) +{ + int Lit; + if ( p->pSat ) + { + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( p->vUsedNodes, pObj, i ) + Ssw_ObjSetSatNum( p, pObj, 0 ); + Vec_PtrClear( p->vUsedNodes ); + Vec_PtrClear( p->vUsedPis ); +// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) ); + sat_solver_delete( p->pSat ); + } + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, 1000 ); + // var 0 is not used + // var 1 is reserved for const1 node - add the clause + p->nSatVars = 1; +// p->nSatVars = 0; + Lit = toLit( p->nSatVars ); + if ( p->pPars->fPolarFlip ) + Lit = lit_neg( Lit ); + sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); + Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ ); + + p->nRecycles++; + p->nRecycleCalls = 0; +} + + +/**Function************************************************************* + + Synopsis [Tranfers simulation information from FRAIG to AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSweepTransfer( Ssw_Man_t * p ) +{ + Aig_Obj_t * pObj, * pObjFraig; + unsigned * pInfo; + int i; + // transfer simulation information + Aig_ManForEachPi( p->pAig, pObj, 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 [Performs one round of simulation with counter-examples.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; + 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************************************************************* + + Synopsis [Builds fraiged logic cone of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pObjNew; + assert( !Aig_IsComplement(pObj) ); + 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_ObjSetFrame( p, pObj, 0, pObjNew ); +} + +/**Function************************************************************* + + Synopsis [Recycles the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj ) +{ + 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) ); + pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 ); + // get the fraiged representative + if ( Aig_ObjIsPi(pObjRepr) ) + { + pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); + Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) ); + pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 ); + } + else + 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->nRecycleCalls++; + p->nCallsCount++; + + // check equivalence of the two nodes + if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) ) + { + p->nPatterns++; + p->nStrangers++; + p->fRefined = 1; + } + else + { + RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); + if ( RetValue == 1 ) // proved equivalence + { + p->nCallsUnsat++; + return; + } + if ( RetValue == -1 ) // timed out + { + Ssw_ClassesRemoveNode( p->ppClasses, pObj ); + p->nCallsUnsat++; + p->fRefined = 1; + return; + } + else // disproved equivalence + { + Ssw_SmlAddPattern( p, pObjRepr, pObj ); + p->nPatterns++; + p->nCallsSat++; + p->fRefined = 1; + } + } +} + +/**Function************************************************************* + + Synopsis [Performs one iteration of sweeping latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_ManSweepLatch( Ssw_Man_t * p ) +{ +// Bar_Progress_t * pProgress = NULL; + Vec_Ptr_t * vClass; + Aig_Obj_t * pObj, * pRepr, * pTemp; + int i, k; + + // start the timeframe + p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) ); + // map constants and PIs + Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) ); + Saig_ManForEachPi( p->pAig, pObj, i ) + 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_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) ); + 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 ); + // consider the case of constant candidate + if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) ) + Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj ); + else + { + // consider the case of equivalence class + Ssw_ClassesCollectClass( p->ppClasses, pObj, vClass ); + if ( Vec_PtrSize(vClass) == 0 ) + continue; + // 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->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 ); + + // cleanup +// Ssw_ClassesCheck( p->ppClasses ); + return p->fRefined; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |