diff options
Diffstat (limited to 'src/aig/ssw/sswInt.h')
| -rw-r--r-- | src/aig/ssw/sswInt.h | 40 |
1 files changed, 32 insertions, 8 deletions
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 21621c0d..009c09c4 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -41,11 +41,10 @@ extern "C" { /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// -// equivalence classes -typedef struct Ssw_Cla_t_ Ssw_Cla_t; +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 -// manager -typedef struct Ssw_Man_t_ Ssw_Man_t; struct Ssw_Man_t_ { // parameters @@ -57,25 +56,38 @@ struct Ssw_Man_t_ Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes of nodes -// Aig_Obj_t ** pReprsProved; // equivalences proved int fRefined; // is set to 1 when refinement happens // 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 + // sequential simulator + Ssw_Sml_t * pSml; + // 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 nStragers; + int nStrangers; // the number of strange situations // SAT calls statistics int nSatCalls; // the number of SAT calls int nSatProof; // the number of proofs + int nSatFails; // the number of timeouts 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; // runtime stats int timeBmc; // bounded model checking int timeReduce; // speculative reduction @@ -131,12 +143,14 @@ extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int 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 void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs ); +extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); -extern int Ssw_ClassesRefine( Ssw_Cla_t * p ); +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 ); /*=== sswMan.c ===================================================*/ @@ -147,9 +161,19 @@ 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 Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ); +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_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ); +extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p ); /*=== sswSimSat.c ===================================================*/ 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 ); /*=== sswSweep.c ===================================================*/ extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); |