/**CFile**************************************************************** FileName [sswInt.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [Inductive prover with constraints.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - September 1, 2008.] Revision [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef ABC__aig__ssw__sswInt_h #define ABC__aig__ssw__sswInt_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include "aig/saig/saig.h" #include "sat/bsat/satSolver.h" #include "ssw.h" #include "aig/ioa/ioa.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// 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 struct Ssw_Man_t_ { // parameters Ssw_Pars_t * pPars; // parameters int nFrames; // for quick lookup // AIGs used in the package Aig_Man_t * pAig; // user-given AIG Aig_Man_t * pFrames; // final AIG 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 // SAT solving Ssw_Sat_t * pMSatBmc; // SAT manager for base case Ssw_Sat_t * pMSat; // SAT manager for inductive case // SAT solving (latch corr only) 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 nRecyclesTotal; // the number of time SAT solver was recycled int nVarsMax; // the maximum variables in the solver int nCallsMax; // the maximum number of SAT calls // uniqueness Vec_Ptr_t * vCommon; // the set of common variables in the logic cones int iOutputLit; // the output literal of the uniqueness constraint Vec_Int_t * vDiffPairs; // is set to 1 if reg pair can be diff int nUniques; // the number of uniqueness constraints used int nUniquesAdded; // useful uniqueness constraints int nUniquesUseful; // useful uniqueness constraints // dynamic constraint addition 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 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 Vec_Int_t * vInits; // the init values of primary inputs under constraints // counter example storage int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example // constraints int nConstrTotal; // the number of total constraints int nConstrReduced; // the number of reduced constraints int nStrangers; // the number of strange situations // SAT calls statistics int nSatCalls; // the number of SAT calls int nSatProof; // the number of proofs int nSatFailsReal; // the number of timeouts int nSatCallsUnsat; // the number of unsat SAT calls int nSatCallsSat; // the number of sat SAT calls // node/register/lit statistics int nLitsBeg; int nLitsEnd; int nNodesBeg; int nNodesEnd; int nRegsBeg; int nRegsEnd; // equiv statistis int nConesTotal; int nConesConstr; int nEquivsTotal; int nEquivsConstr; int nNodesBegC; int nNodesEndC; int nRegsBegC; int nRegsEndC; // runtime stats abctime timeBmc; // bounded model checking abctime timeReduce; // speculative reduction abctime timeMarkCones; // marking the cones not to be refined abctime timeSimSat; // simulation of the counter-examples abctime timeSat; // solving SAT abctime timeSatSat; // sat abctime timeSatUnsat; // unsat abctime timeSatUndec; // undecided abctime timeOther; // other runtime abctime timeTotal; // total runtime }; // internal SAT manager struct Ssw_Sat_t_ { Aig_Man_t * pAig; // the AIG manager int fPolarFlip; // flips polarity sat_solver * pSat; // recyclable SAT solver int nSatVars; // the counter of SAT variables Vec_Int_t * vSatVars; // mapping of each node into its SAT var Vec_Ptr_t * vFanins; // fanins of the CNF node Vec_Ptr_t * vUsedPis; // the PIs with SAT variables int nSolverCalls; // the total number of SAT calls }; // internal frames manager struct Ssw_Frm_t_ { Aig_Man_t * pAig; // user-given AIG int nObjs; // offset in terms of AIG nodes int nFrames; // the number of frames in current unrolling Aig_Man_t * pFrames; // unrolled AIG Vec_Ptr_t * vAig2Frm; // mapping of AIG nodes into frame nodes }; //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// static inline int Ssw_ObjSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vSatVars, pObj->Id ); } static inline void Ssw_ObjSetSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vSatVars, pObj->Id, Num); } static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) { return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig); } static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) { assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) ); Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); } 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_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; } static inline Aig_Obj_t * Ssw_ObjFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); } static inline void Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); } static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_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_Frm_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 /// //////////////////////////////////////////////////////////////////////// /*=== sswAig.c ===================================================*/ extern Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig ); extern void Ssw_FrmStop( Ssw_Frm_t * p ); extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ); extern Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ); /*=== sswBmc.c ===================================================*/ /*=== sswClass.c =================================================*/ extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig ); extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ); extern void Ssw_ClassesStop( Ssw_Cla_t * p ); extern Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p ); extern Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p ); extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p ); extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p ); extern int Ssw_ClassesClassNum( Ssw_Cla_t * p ); extern int Ssw_ClassesLitNum( Ssw_Cla_t * p ); extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ); extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass ); 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 nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); extern Ssw_Cla_t * Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig ); 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_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs ); extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive ); extern int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, 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_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr ); /*=== sswCnf.c ===================================================*/ extern Ssw_Sat_t * Ssw_SatStart( int fPolarFlip ); extern void Ssw_SatStop( Ssw_Sat_t * p ); extern void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj ); extern int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig ); /*=== sswConstr.c ===================================================*/ extern int Ssw_ManSweepBmcConstr( Ssw_Man_t * p ); extern int Ssw_ManSweepConstr( Ssw_Man_t * p ); extern void Ssw_ManRefineByConstrSim( Ssw_Man_t * p ); /*=== sswCore.c ===================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ); /*=== sswDyn.c ===================================================*/ extern void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ); extern int Ssw_ManSweepDyn( Ssw_Man_t * p ); /*=== sswLcorr.c ==========================================================*/ extern int Ssw_ManSweepLatch( Ssw_Man_t * p ); /*=== sswMan.c ===================================================*/ extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); extern void Ssw_ManCleanup( Ssw_Man_t * p ); extern void Ssw_ManStop( Ssw_Man_t * p ); /*=== sswSat.c ===================================================*/ 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 ); extern int Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj ); /*=== sswSemi.c ===================================================*/ extern int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ); /*=== 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 void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ); 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 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 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 ); extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ); extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ); extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs ); extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); /*=== sswUnique.c ===================================================*/ extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p ); extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose ); extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////