1 /**CFile****************************************************************
2
3 FileName [sswInt.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Inductive prover with constraints.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 1, 2008.]
16
17 Revision [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__aig__ssw__sswInt_h
22 #define ABC__aig__ssw__sswInt_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include "aig/saig/saig.h"
30 #include "sat/bsat/satSolver.h"
31 #include "ssw.h"
32 #include "aig/ioa/ioa.h"
33
34 ////////////////////////////////////////////////////////////////////////
35 /// PARAMETERS ///
36 ////////////////////////////////////////////////////////////////////////
37
38
39
40 ABC_NAMESPACE_HEADER_START
41
42
43 ////////////////////////////////////////////////////////////////////////
44 /// BASIC TYPES ///
45 ////////////////////////////////////////////////////////////////////////
46
47 typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
48 typedef struct Ssw_Frm_t_ Ssw_Frm_t; // unrolled frames manager
49 typedef struct Ssw_Sat_t_ Ssw_Sat_t; // SAT solver manager
50 typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager
51
52 struct Ssw_Man_t_
53 {
54 // parameters
55 Ssw_Pars_t * pPars; // parameters
56 int nFrames; // for quick lookup
57 // AIGs used in the package
58 Aig_Man_t * pAig; // user-given AIG
59 Aig_Man_t * pFrames; // final AIG
60 Aig_Obj_t ** pNodeToFrames; // mapping of AIG nodes into FRAIG nodes
61 // equivalence classes
62 Ssw_Cla_t * ppClasses; // equivalence classes of nodes
63 int fRefined; // is set to 1 when refinement happens
64 // SAT solving
65 Ssw_Sat_t * pMSatBmc; // SAT manager for base case
66 Ssw_Sat_t * pMSat; // SAT manager for inductive case
67 // SAT solving (latch corr only)
68 Vec_Ptr_t * vSimInfo; // simulation information for the framed PIs
69 int nPatterns; // the number of patterns saved
70 int nSimRounds; // the number of simulation rounds performed
71 int nCallsCount; // the number of calls in this round
72 int nCallsDelta; // the number of calls to skip
73 int nCallsSat; // the number of SAT calls in this round
74 int nCallsUnsat; // the number of UNSAT calls in this round
75 int nRecycleCalls; // the number of calls since last recycling
76 int nRecycles; // the number of time SAT solver was recycled
77 int nRecyclesTotal; // the number of time SAT solver was recycled
78 int nVarsMax; // the maximum variables in the solver
79 int nCallsMax; // the maximum number of SAT calls
80 // uniqueness
81 Vec_Ptr_t * vCommon; // the set of common variables in the logic cones
82 int iOutputLit; // the output literal of the uniqueness constraint
83 Vec_Int_t * vDiffPairs; // is set to 1 if reg pair can be diff
84 int nUniques; // the number of uniqueness constraints used
85 int nUniquesAdded; // useful uniqueness constraints
86 int nUniquesUseful; // useful uniqueness constraints
87 // dynamic constraint addition
88 int nSRMiterMaxId; // max ID after which the last frame begins
89 Vec_Ptr_t * vNewLos; // new time frame LOs of to constrain
90 Vec_Int_t * vNewPos; // new time frame POs of to add constraints
91 int * pVisited; // flags to label visited nodes in each frame
92 int nVisCounter; // the traversal ID
93 // sequential simulation
94 Ssw_Sml_t * pSml; // the simulator
95 int iNodeStart; // the first node considered
96 int iNodeLast; // the last node considered
97 Vec_Ptr_t * vResimConsts; // resimulation constants
98 Vec_Ptr_t * vResimClasses; // resimulation classes
99 Vec_Int_t * vInits; // the init values of primary inputs under constraints
100 // counter example storage
101 int nPatWords; // the number of words in the counter example
102 unsigned * pPatWords; // the counter example
103 // constraints
104 int nConstrTotal; // the number of total constraints
105 int nConstrReduced; // the number of reduced constraints
106 int nStrangers; // the number of strange situations
107 // SAT calls statistics
108 int nSatCalls; // the number of SAT calls
109 int nSatProof; // the number of proofs
110 int nSatFailsReal; // the number of timeouts
111 int nSatCallsUnsat; // the number of unsat SAT calls
112 int nSatCallsSat; // the number of sat SAT calls
113 // node/register/lit statistics
114 int nLitsBeg;
115 int nLitsEnd;
116 int nNodesBeg;
117 int nNodesEnd;
118 int nRegsBeg;
119 int nRegsEnd;
120 // equiv statistis
121 int nConesTotal;
122 int nConesConstr;
123 int nEquivsTotal;
124 int nEquivsConstr;
125 int nNodesBegC;
126 int nNodesEndC;
127 int nRegsBegC;
128 int nRegsEndC;
129 // runtime stats
130 abctime timeBmc; // bounded model checking
131 abctime timeReduce; // speculative reduction
132 abctime timeMarkCones; // marking the cones not to be refined
133 abctime timeSimSat; // simulation of the counter-examples
134 abctime timeSat; // solving SAT
135 abctime timeSatSat; // sat
136 abctime timeSatUnsat; // unsat
137 abctime timeSatUndec; // undecided
138 abctime timeOther; // other runtime
139 abctime timeTotal; // total runtime
140 };
141
142 // internal SAT manager
143 struct Ssw_Sat_t_
144 {
145 Aig_Man_t * pAig; // the AIG manager
146 int fPolarFlip; // flips polarity
147 sat_solver * pSat; // recyclable SAT solver
148 int nSatVars; // the counter of SAT variables
149 Vec_Int_t * vSatVars; // mapping of each node into its SAT var
150 Vec_Ptr_t * vFanins; // fanins of the CNF node
151 Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
152 int nSolverCalls; // the total number of SAT calls
153 };
154
155 // internal frames manager
156 struct Ssw_Frm_t_
157 {
158 Aig_Man_t * pAig; // user-given AIG
159 int nObjs; // offset in terms of AIG nodes
160 int nFrames; // the number of frames in current unrolling
161 Aig_Man_t * pFrames; // unrolled AIG
162 Vec_Ptr_t * vAig2Frm; // mapping of AIG nodes into frame nodes
163 };
164
165 ////////////////////////////////////////////////////////////////////////
166 /// MACRO DEFINITIONS ///
167 ////////////////////////////////////////////////////////////////////////
168
Ssw_ObjSatNum(Ssw_Sat_t * p,Aig_Obj_t * pObj)169 static inline int Ssw_ObjSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vSatVars, pObj->Id ); }
Ssw_ObjSetSatNum(Ssw_Sat_t * p,Aig_Obj_t * pObj,int Num)170 static inline void Ssw_ObjSetSatNum( Ssw_Sat_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vSatVars, pObj->Id, Num); }
171
Ssw_ObjIsConst1Cand(Aig_Man_t * pAig,Aig_Obj_t * pObj)172 static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
173 {
174 return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
175 }
Ssw_ObjSetConst1Cand(Aig_Man_t * pAig,Aig_Obj_t * pObj)176 static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
177 {
178 assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) );
179 Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
180 }
181
Ssw_ObjFrame(Ssw_Man_t * p,Aig_Obj_t * pObj,int i)182 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]; }
Ssw_ObjSetFrame(Ssw_Man_t * p,Aig_Obj_t * pObj,int i,Aig_Obj_t * pNode)183 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; }
184
Ssw_ObjChild0Fra(Ssw_Man_t * p,Aig_Obj_t * pObj,int i)185 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; }
Ssw_ObjChild1Fra(Ssw_Man_t * p,Aig_Obj_t * pObj,int i)186 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; }
187
Ssw_ObjFrame_(Ssw_Frm_t * p,Aig_Obj_t * pObj,int i)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 ); }
Ssw_ObjSetFrame_(Ssw_Frm_t * p,Aig_Obj_t * pObj,int i,Aig_Obj_t * pNode)189 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 ); }
190
Ssw_ObjChild0Fra_(Ssw_Frm_t * p,Aig_Obj_t * pObj,int i)191 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; }
Ssw_ObjChild1Fra_(Ssw_Frm_t * p,Aig_Obj_t * pObj,int i)192 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; }
193
194 ////////////////////////////////////////////////////////////////////////
195 /// FUNCTION DECLARATIONS ///
196 ////////////////////////////////////////////////////////////////////////
197
198 /*=== sswAig.c ===================================================*/
199 extern Ssw_Frm_t * Ssw_FrmStart( Aig_Man_t * pAig );
200 extern void Ssw_FrmStop( Ssw_Frm_t * p );
201 extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p );
202 extern Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p );
203 /*=== sswBmc.c ===================================================*/
204 /*=== sswClass.c =================================================*/
205 extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig );
206 extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
207 unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
208 int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
209 int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
210 extern void Ssw_ClassesStop( Ssw_Cla_t * p );
211 extern Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p );
212 extern Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p );
213 extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p );
214 extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p );
215 extern int Ssw_ClassesClassNum( Ssw_Cla_t * p );
216 extern int Ssw_ClassesLitNum( Ssw_Cla_t * p );
217 extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
218 extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
219 extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
220 extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
221 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 );
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 );
225 extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
226 extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
227 extern Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
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 );
230 extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
231 extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
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 );
234 /*=== sswCnf.c ===================================================*/
235 extern Ssw_Sat_t * Ssw_SatStart( int fPolarFlip );
236 extern void Ssw_SatStop( Ssw_Sat_t * p );
237 extern void Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj );
238 extern int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig );
239 /*=== sswConstr.c ===================================================*/
240 extern int Ssw_ManSweepBmcConstr( Ssw_Man_t * p );
241 extern int Ssw_ManSweepConstr( Ssw_Man_t * p );
242 extern void Ssw_ManRefineByConstrSim( Ssw_Man_t * p );
243 /*=== sswCore.c ===================================================*/
244 extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
245 /*=== sswDyn.c ===================================================*/
246 extern void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
247 extern int Ssw_ManSweepDyn( Ssw_Man_t * p );
248 /*=== sswLcorr.c ==========================================================*/
249 extern int Ssw_ManSweepLatch( Ssw_Man_t * p );
250 /*=== sswMan.c ===================================================*/
251 extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
252 extern void Ssw_ManCleanup( Ssw_Man_t * p );
253 extern void Ssw_ManStop( Ssw_Man_t * p );
254 /*=== sswSat.c ===================================================*/
255 extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
256 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 );
258 /*=== sswSemi.c ===================================================*/
259 extern int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
260 /*=== sswSim.c ===================================================*/
261 extern unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
262 extern int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
263 extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
264 extern int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
265 extern int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
266 extern void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame );
267 extern Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
268 extern void Ssw_SmlClean( Ssw_Sml_t * p );
269 extern void Ssw_SmlStop( Ssw_Sml_t * p );
270 extern void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
271 extern void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
272 extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
273 extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
274 extern void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
275 extern void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pVisited, int nVisCounter );
276 extern void Ssw_SmlResimulateSeq( Ssw_Sml_t * p );
277 /*=== sswSimSat.c ===================================================*/
278 extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
279 extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
280 /*=== sswSweep.c ===================================================*/
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 );
284 extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
285 extern int Ssw_ManSweep( Ssw_Man_t * p );
286 /*=== sswUnique.c ===================================================*/
287 extern void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
288 extern int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose );
289 extern int Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
290
291
292
293 ABC_NAMESPACE_HEADER_END
294
295
296
297 #endif
298
299 ////////////////////////////////////////////////////////////////////////
300 /// END OF FILE ///
301 ////////////////////////////////////////////////////////////////////////
302
303