sswInt.h 17 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
/**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 $]

***********************************************************************/
 
21 22
#ifndef ABC__aig__ssw__sswInt_h
#define ABC__aig__ssw__sswInt_h
Alan Mishchenko committed
23

24

Alan Mishchenko committed
25 26 27 28
////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

29 30
#include "aig/saig/saig.h"
#include "sat/bsat/satSolver.h"
Alan Mishchenko committed
31
#include "ssw.h"
32
#include "aig/ioa/ioa.h"
Alan Mishchenko committed
33 34 35 36 37

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

38 39 40 41


ABC_NAMESPACE_HEADER_START

Alan Mishchenko committed
42

Alan Mishchenko committed
43 44 45 46
////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
47
typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
Alan Mishchenko committed
48 49
typedef struct Ssw_Frm_t_ Ssw_Frm_t; // unrolled frames manager
typedef struct Ssw_Sat_t_ Ssw_Sat_t; // SAT solver manager
Alan Mishchenko committed
50
typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager
Alan Mishchenko committed
51 52 53 54 55 56 57 58 59

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
Alan Mishchenko committed
60
    Aig_Obj_t **     pNodeToFrames;  // mapping of AIG nodes into FRAIG nodes
Alan Mishchenko committed
61 62 63
    // equivalence classes
    Ssw_Cla_t *      ppClasses;      // equivalence classes of nodes
    int              fRefined;       // is set to 1 when refinement happens
Alan Mishchenko committed
64 65 66
    // SAT solving 
    Ssw_Sat_t *      pMSatBmc;       // SAT manager for base case
    Ssw_Sat_t *      pMSat;          // SAT manager for inductive case
Alan Mishchenko committed
67
    // SAT solving (latch corr only)
Alan Mishchenko committed
68 69 70 71 72 73 74 75 76
    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
Alan Mishchenko committed
77 78 79
    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
Alan Mishchenko committed
80 81
    // uniqueness
    Vec_Ptr_t *      vCommon;        // the set of common variables in the logic cones
Alan Mishchenko committed
82
    int              iOutputLit;     // the output literal of the uniqueness constraint
Alan Mishchenko committed
83
    Vec_Int_t *      vDiffPairs;     // is set to 1 if reg pair can be diff
Alan Mishchenko committed
84
    int              nUniques;       // the number of uniqueness constraints used 
Alan Mishchenko committed
85 86
    int              nUniquesAdded;  // useful uniqueness constraints
    int              nUniquesUseful; // useful uniqueness constraints
Alan Mishchenko committed
87 88 89 90
    // 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
Alan Mishchenko committed
91 92 93 94 95 96 97 98
    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
99
    Vec_Int_t *      vInits;         // the init values of primary inputs under constraints
Alan Mishchenko committed
100 101 102
    // counter example storage
    int              nPatWords;      // the number of words in the counter example
    unsigned *       pPatWords;      // the counter example
Alan Mishchenko committed
103 104 105
    // constraints
    int              nConstrTotal;   // the number of total constraints
    int              nConstrReduced; // the number of reduced constraints
Alan Mishchenko committed
106
    int              nStrangers;     // the number of strange situations
Alan Mishchenko committed
107 108 109 110 111 112
    // 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
Alan Mishchenko committed
113 114 115 116 117 118 119
    // node/register/lit statistics
    int              nLitsBeg;
    int              nLitsEnd;
    int              nNodesBeg;
    int              nNodesEnd;
    int              nRegsBeg;
    int              nRegsEnd;
120 121 122 123 124 125 126 127 128
    // equiv statistis
    int              nConesTotal;
    int              nConesConstr;
    int              nEquivsTotal;
    int              nEquivsConstr;
    int              nNodesBegC;
    int              nNodesEndC;
    int              nRegsBegC;
    int              nRegsEndC;
Alan Mishchenko committed
129
    // runtime stats
130 131 132 133 134 135 136 137 138 139
    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
Alan Mishchenko committed
140 141
};

Alan Mishchenko committed
142 143 144 145 146 147 148 149 150 151
// 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 
Alan Mishchenko committed
152
    int              nSolverCalls;   // the total number of SAT calls
Alan Mishchenko committed
153 154 155 156 157 158 159 160 161 162 163 164
};

// 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
};

Alan Mishchenko committed
165 166 167 168
////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
169 170
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);      }
Alan Mishchenko committed
171 172 173 174 175 176 177 178 179 180 181

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) );
}

Alan Mishchenko committed
182 183
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; }
Alan Mishchenko committed
184

Alan Mishchenko committed
185 186
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;  }
Alan Mishchenko committed
187

188
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 );     }
Alan Mishchenko committed
189 190 191 192 193
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;  }

Alan Mishchenko committed
194 195 196 197 198
////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== sswAig.c ===================================================*/
Alan Mishchenko committed
199 200
extern Ssw_Frm_t *   Ssw_FrmStart( Aig_Man_t * pAig );
extern void          Ssw_FrmStop( Ssw_Frm_t * p );
Alan Mishchenko committed
201
extern Aig_Man_t *   Ssw_FramesWithClasses( Ssw_Man_t * p );
Alan Mishchenko committed
202 203
extern Aig_Man_t *   Ssw_SpeculativeReduction( Ssw_Man_t * p );
/*=== sswBmc.c ===================================================*/
Alan Mishchenko committed
204 205 206 207 208 209 210
/*=== 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 );
Alan Mishchenko committed
211
extern Aig_Man_t *   Ssw_ClassesReadAig( Ssw_Cla_t * p );
Alan Mishchenko committed
212 213
extern Vec_Ptr_t *   Ssw_ClassesGetRefined( Ssw_Cla_t * p );
extern void          Ssw_ClassesClearRefined( Ssw_Cla_t * p );
Alan Mishchenko committed
214 215 216 217
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 );
Alan Mishchenko committed
218
extern void          Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
Alan Mishchenko committed
219 220 221
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 );
222
extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose );
Alan Mishchenko committed
223
extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
224
extern Ssw_Cla_t *   Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig );
Alan Mishchenko committed
225
extern Ssw_Cla_t *   Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
Alan Mishchenko committed
226
extern Ssw_Cla_t *   Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
Alan Mishchenko committed
227
extern Ssw_Cla_t *   Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
Alan Mishchenko committed
228
extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
229
extern int           Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive );
Alan Mishchenko committed
230 231
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 );
Alan Mishchenko committed
232
extern int           Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
233
extern int           Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr );
Alan Mishchenko committed
234
/*=== sswCnf.c ===================================================*/
Alan Mishchenko committed
235 236 237 238
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 );
239 240 241 242
/*=== 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 );
Alan Mishchenko committed
243 244
/*=== sswCore.c ===================================================*/
extern Aig_Man_t *   Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
Alan Mishchenko committed
245 246 247
/*=== 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 );
Alan Mishchenko committed
248 249
/*=== sswLcorr.c ==========================================================*/
extern int           Ssw_ManSweepLatch( Ssw_Man_t * p );
Alan Mishchenko committed
250 251 252 253 254 255 256
/*=== 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 );
257
extern int           Ssw_NodeIsConstrained( Ssw_Man_t * p, Aig_Obj_t * pPoObj );
Alan Mishchenko committed
258 259
/*=== sswSemi.c ===================================================*/
extern int           Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
Alan Mishchenko committed
260
/*=== sswSim.c ===================================================*/
Alan Mishchenko committed
261 262 263 264 265
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 );
Alan Mishchenko committed
266
extern void          Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame );
Alan Mishchenko committed
267
extern Ssw_Sml_t *   Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
Alan Mishchenko committed
268
extern void          Ssw_SmlClean( Ssw_Sml_t * p );
Alan Mishchenko committed
269
extern void          Ssw_SmlStop( Ssw_Sml_t * p );
Alan Mishchenko committed
270 271
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 );
Alan Mishchenko committed
272 273
extern void          Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void          Ssw_SmlSimulateOne( Ssw_Sml_t * p );
Alan Mishchenko committed
274
extern void          Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
Alan Mishchenko committed
275
extern void          Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pVisited, int nVisCounter );
Alan Mishchenko committed
276
extern void          Ssw_SmlResimulateSeq( Ssw_Sml_t * p );
Alan Mishchenko committed
277
/*=== sswSimSat.c ===================================================*/
Alan Mishchenko committed
278 279
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 );
Alan Mishchenko committed
280
/*=== sswSweep.c ===================================================*/
Alan Mishchenko committed
281
extern int           Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
282
extern void          Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f );
283
extern int           Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs );
Alan Mishchenko committed
284 285
extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int           Ssw_ManSweep( Ssw_Man_t * p );
Alan Mishchenko committed
286
/*=== sswUnique.c ===================================================*/
Alan Mishchenko committed
287
extern void          Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
Alan Mishchenko committed
288
extern int           Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose );
Alan Mishchenko committed
289
extern int           Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
Alan Mishchenko committed
290

291 292 293 294 295


ABC_NAMESPACE_HEADER_END


Alan Mishchenko committed
296 297 298 299 300 301 302

#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////