diff options
Diffstat (limited to 'src/aig/ssw_old/sswInt.h')
| -rw-r--r-- | src/aig/ssw_old/sswInt.h | 232 |
1 files changed, 0 insertions, 232 deletions
diff --git a/src/aig/ssw_old/sswInt.h b/src/aig/ssw_old/sswInt.h deleted file mode 100644 index d7bf46a8..00000000 --- a/src/aig/ssw_old/sswInt.h +++ /dev/null @@ -1,232 +0,0 @@ -/**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 __SSW_INT_H__ -#define __SSW_INT_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include "saig.h" -#include "satSolver.h" -#include "ssw.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager -typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager -typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager - -struct Ssw_Man_t_ -{ - // 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 - 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 - Vec_Int_t * vSatVars; // 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 - // SAT solving (latch corr only) - 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 - // uniqueness - Vec_Ptr_t * vCommon; // the set of common variables in the logic cones - int iOutputLit; // the output literal of the uniqueness constaint - int nUniques; // the number of uniqueness constaints used - // sequential simulator - Ssw_Sml_t * pSml; - // counter example storage - int nPatWords; // the number of words in the counter example - unsigned * pPatWords; // the counter example - unsigned * pPatWords2; // 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 nSatFailsTotal; // 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; - // runtime stats - int timeBmc; // bounded model checking - int timeReduce; // speculative reduction - int timeMarkCones; // marking the cones not to be refined - int timeSimSat; // simulation of the counter-examples - int timeSat; // solving SAT - int timeSatSat; // sat - int timeSatUnsat; // unsat - int timeSatUndec; // undecided - int timeOther; // other runtime - int timeTotal; // total runtime -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, pObj->Id ); } -static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntWriteEntryFill( 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; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== sswAig.c ===================================================*/ -extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ); -extern Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ); -/*=== sswBmc.c ===================================================*/ -extern int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose ); -/*=== 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 fLatchCorr, int nMaxLevs, int fVerbose ); -extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); -extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig ); -extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ); -extern 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 ); -/*=== sswCnf.c ===================================================*/ -extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); -/*=== sswCore.c ===================================================*/ -extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( 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 ); -extern void Ssw_ManStartSolver( 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 ); -/*=== 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 void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame ); -extern unsigned Ssw_SmlObjGetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iWord, 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 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 ); -extern void Ssw_ManResimulateWord2( 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 int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ); -extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); -extern int Ssw_ManSweep( Ssw_Man_t * p ); -/*=== sswUnique.c ===================================================*/ -extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ); -extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - |