1 /**CFile****************************************************************
2
3 FileName [fra.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [[New FRAIG package.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__aig__fra__fra_h
22 #define ABC__aig__fra__fra_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include <stdio.h>
30 #include <stdlib.h>
31 #include <string.h>
32 #include <assert.h>
33
34 #include "misc/vec/vec.h"
35 #include "aig/aig/aig.h"
36 #include "opt/dar/dar.h"
37 #include "sat/bsat/satSolver.h"
38 #include "aig/ioa/ioa.h"
39
40 ////////////////////////////////////////////////////////////////////////
41 /// PARAMETERS ///
42 ////////////////////////////////////////////////////////////////////////
43
44
45
46 ABC_NAMESPACE_HEADER_START
47
48
49 ////////////////////////////////////////////////////////////////////////
50 /// BASIC TYPES ///
51 ////////////////////////////////////////////////////////////////////////
52
53 typedef struct Fra_Par_t_ Fra_Par_t;
54 typedef struct Fra_Ssw_t_ Fra_Ssw_t;
55 typedef struct Fra_Sec_t_ Fra_Sec_t;
56 typedef struct Fra_Man_t_ Fra_Man_t;
57 typedef struct Fra_Cla_t_ Fra_Cla_t;
58 typedef struct Fra_Sml_t_ Fra_Sml_t;
59 typedef struct Fra_Bmc_t_ Fra_Bmc_t;
60
61 // FRAIG parameters
62 struct Fra_Par_t_
63 {
64 int nSimWords; // the number of words in the simulation info
65 double dSimSatur; // the ratio of refined classes when saturation is reached
66 int fPatScores; // enables simulation pattern scoring
67 int MaxScore; // max score after which resimulation is used
68 double dActConeRatio; // the ratio of cone to be bumped
69 double dActConeBumpMax; // the largest bump in activity
70 int fChoicing; // enables choicing
71 int fSpeculate; // use speculative reduction
72 int fProve; // prove the miter outputs
73 int fVerbose; // verbose output
74 int fDoSparse; // skip sparse functions
75 int fConeBias; // bias variables in the cone (good for unsat runs)
76 int nBTLimitNode; // conflict limit at a node
77 int nBTLimitMiter; // conflict limit at an output
78 int nLevelMax; // the max level to consider seriously
79 int nFramesP; // the number of timeframes to in the prefix
80 int nFramesK; // the number of timeframes to unroll
81 int nMaxImps; // the maximum number of implications to consider
82 int nMaxLevs; // the maximum number of levels to consider
83 int fRewrite; // use rewriting for constraint reduction
84 int fLatchCorr; // computes latch correspondence only
85 int fUseImps; // use implications
86 int fUse1Hot; // use one-hotness conditions
87 int fWriteImps; // record implications
88 int fDontShowBar; // does not show progressbar during fraiging
89 };
90
91 // seq SAT sweeping parameters
92 struct Fra_Ssw_t_
93 {
94 int nPartSize; // size of the partition
95 int nOverSize; // size of the overlap between partitions
96 int nFramesP; // number of frames in the prefix
97 int nFramesK; // number of frames for induction (1=simple)
98 int nMaxImps; // max implications to consider
99 int nMaxLevs; // max levels to consider
100 int nMinDomSize; // min clock domain considered for optimization
101 int fUseImps; // use implications
102 int fRewrite; // enable rewriting of the specualatively reduced model
103 int fFraiging; // enable comb SAT sweeping as preprocessing
104 int fLatchCorr; // perform register correspondence
105 int fWriteImps; // write implications into a file
106 int fUse1Hot; // use one-hotness constraints
107 int fVerbose; // enable verbose output
108 int fSilent; // disable any output
109 int nIters; // the number of iterations performed
110 float TimeLimit; // the runtime budget for this call
111 };
112
113 // SEC parametesr
114 struct Fra_Sec_t_
115 {
116 int fTryComb; // try CEC call as a preprocessing step
117 int fTryBmc; // try BMC call as a preprocessing step
118 int nFramesMax; // the max number of frames used for induction
119 int nBTLimit; // the conflict limit at a node
120 int nBTLimitGlobal; // the global conflict limit
121 int nBTLimitInter; // the conflict limit for interpolation
122 int nBddVarsMax; // the state space limit for BDD reachability
123 int nBddMax; // the max number of BDD nodes
124 int nBddIterMax; // the limit on the number of BDD iterations
125 int nPdrTimeout; // the timeout for PDR in the end
126 int fPhaseAbstract; // enables phase abstraction
127 int fRetimeFirst; // enables most-forward retiming at the beginning
128 int fRetimeRegs; // enables min-register retiming at the beginning
129 int fFraiging; // enables fraiging at the beginning
130 int fInduction; // enable the use of induction
131 int fInterpolation; // enables interpolation
132 int fInterSeparate; // enables interpolation for each outputs separately
133 int fReachability; // enables BDD based reachability
134 int fReorderImage; // enables BDD reordering during image computation
135 int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
136 int fUseNewProver; // the new prover
137 int fUsePdr; // the PDR
138 int fSilent; // disables all output
139 int fVerbose; // enables verbose reporting of statistics
140 int fVeryVerbose; // enables very verbose reporting
141 int TimeLimit; // enables the timeout
142 int fReadUnsolved; // inserts the unsolved model back
143 int nSMnumber; // the number of model written
144 // internal parameters
145 int fRecursive; // set to 1 when SEC is called recursively
146 int fReportSolution; // enables report solution in a special form
147 };
148
149 // FRAIG equivalence classes
150 struct Fra_Cla_t_
151 {
152 Aig_Man_t * pAig; // the original AIG manager
153 Aig_Obj_t ** pMemRepr; // pointers to representatives of each node
154 Vec_Ptr_t * vClasses; // equivalence classes
155 Vec_Ptr_t * vClasses1; // equivalence class of Const1 node
156 Vec_Ptr_t * vClassesTemp; // temporary storage for new classes
157 Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
158 Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
159 Vec_Ptr_t * vClassOld; // old equivalence class after splitting
160 Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
161 int nPairs; // the number of pairs of nodes
162 int fRefinement; // set to 1 when refinement has happened
163 Vec_Int_t * vImps; // implications
164 // procedures used for class refinement
165 int (*pFuncNodeHash) (Aig_Obj_t *, int); // returns has key of the node
166 int (*pFuncNodeIsConst) (Aig_Obj_t *); // returns 1 if the node is a constant
167 int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
168 };
169
170 // simulation manager
171 struct Fra_Sml_t_
172 {
173 Aig_Man_t * pAig; // the original AIG manager
174 int nPref; // the number of times frames in the prefix
175 int nFrames; // the number of times frames
176 int nWordsFrame; // the number of words in each time frame
177 int nWordsTotal; // the total number of words at a node
178 int nWordsPref; // the number of word in the prefix
179 int fNonConstOut; // have seen a non-const-0 output during simulation
180 int nSimRounds; // statistics
181 int timeSim; // statistics
182 unsigned pData[0]; // simulation data for the nodes
183 };
184
185 // FRAIG manager
186 struct Fra_Man_t_
187 {
188 // high-level data
189 Fra_Par_t * pPars; // parameters governing fraiging
190 // AIG managers
191 Aig_Man_t * pManAig; // the starting AIG manager
192 Aig_Man_t * pManFraig; // the final AIG manager
193 // mapping AIG into FRAIG
194 int nFramesAll; // the number of timeframes used
195 Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
196 int nSizeAlloc; // allocated size of the arrays for timeframe nodes
197 // equivalence classes
198 Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes
199 // simulation info
200 Fra_Sml_t * pSml; // simulation manager
201 // bounded model checking manager
202 Fra_Bmc_t * pBmc;
203 // counter example storage
204 int nPatWords; // the number of words in the counter example
205 unsigned * pPatWords; // the counter example
206 Vec_Int_t * vCex;
207 // one-hotness conditions
208 Vec_Int_t * vOneHots;
209 // satisfiability solving
210 sat_solver * pSat; // SAT solver
211 int nSatVars; // the number of variables currently used
212 Vec_Ptr_t * vPiVars; // the PIs of the cone used
213 ABC_INT64_T nBTLimitGlobal; // resource limit
214 ABC_INT64_T nInsLimitGlobal; // resource limit
215 Vec_Ptr_t ** pMemFanins; // the arrays of fanins for some FRAIG nodes
216 int * pMemSatNums; // the array of SAT numbers for some FRAIG nodes
217 int nMemAlloc; // allocated size of the arrays for FRAIG varnums and fanins
218 Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out
219 // statistics
220 int nSimRounds;
221 int nNodesMiter;
222 int nLitsBeg;
223 int nLitsEnd;
224 int nNodesBeg;
225 int nNodesEnd;
226 int nRegsBeg;
227 int nRegsEnd;
228 int nSatCalls;
229 int nSatCallsSat;
230 int nSatCallsUnsat;
231 int nSatProof;
232 int nSatFails;
233 int nSatFailsReal;
234 int nSpeculs;
235 int nChoices;
236 int nChoicesFake;
237 int nSatCallsRecent;
238 int nSatCallsSkipped;
239 // runtime
240 abctime timeSim;
241 abctime timeTrav;
242 abctime timeRwr;
243 abctime timeSat;
244 abctime timeSatUnsat;
245 abctime timeSatSat;
246 abctime timeSatFail;
247 abctime timeRef;
248 abctime timeTotal;
249 abctime time1;
250 abctime time2;
251 };
252
253 ////////////////////////////////////////////////////////////////////////
254 /// MACRO DEFINITIONS ///
255 ////////////////////////////////////////////////////////////////////////
256
Fra_ObjSim(Fra_Sml_t * p,int Id)257 static inline unsigned * Fra_ObjSim( Fra_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; }
Fra_ObjRandomSim()258 static inline unsigned Fra_ObjRandomSim() { return Aig_ManRandom(0); }
259
Fra_ObjFraig(Aig_Obj_t * pObj,int i)260 static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; }
Fra_ObjSetFraig(Aig_Obj_t * pObj,int i,Aig_Obj_t * pNode)261 static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
262
Fra_ObjFaninVec(Aig_Obj_t * pObj)263 static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
Fra_ObjSetFaninVec(Aig_Obj_t * pObj,Vec_Ptr_t * vFanins)264 static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
265
Fra_ObjSatNum(Aig_Obj_t * pObj)266 static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
Fra_ObjSetSatNum(Aig_Obj_t * pObj,int Num)267 static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
268
Fra_ClassObjRepr(Aig_Obj_t * pObj)269 static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; }
Fra_ClassObjSetRepr(Aig_Obj_t * pObj,Aig_Obj_t * pNode)270 static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }
271
Fra_ObjChild0Fra(Aig_Obj_t * pObj,int i)272 static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
Fra_ObjChild1Fra(Aig_Obj_t * pObj,int i)273 static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
274
Fra_ImpLeft(int Imp)275 static inline int Fra_ImpLeft( int Imp ) { return Imp & 0xFFFF; }
Fra_ImpRight(int Imp)276 static inline int Fra_ImpRight( int Imp ) { return Imp >> 16; }
Fra_ImpCreate(int Left,int Right)277 static inline int Fra_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
278
279 ////////////////////////////////////////////////////////////////////////
280 /// ITERATORS ///
281 ////////////////////////////////////////////////////////////////////////
282
283 ////////////////////////////////////////////////////////////////////////
284 /// FUNCTION DECLARATIONS ///
285 ////////////////////////////////////////////////////////////////////////
286
287 /*=== fraCec.c ========================================================*/
288 extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
289 extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
290 extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
291 /*=== fraClass.c ========================================================*/
292 extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
293 extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
294 extern void Fra_BmcStop( Fra_Bmc_t * p );
295 extern void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
296 extern void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
297 /*=== fraClass.c ========================================================*/
298 extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
299 extern void Fra_ClassesStop( Fra_Cla_t * p );
300 extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
301 extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
302 extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
303 extern int Fra_ClassesRefine( Fra_Cla_t * p );
304 extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
305 extern int Fra_ClassesCountLits( Fra_Cla_t * p );
306 extern int Fra_ClassesCountPairs( Fra_Cla_t * p );
307 extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
308 extern void Fra_ClassesLatchCorr( Fra_Man_t * p );
309 extern void Fra_ClassesPostprocess( Fra_Cla_t * p );
310 extern void Fra_ClassesSelectRepr( Fra_Cla_t * p );
311 extern Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
312 /*=== fraCnf.c ========================================================*/
313 extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
314 /*=== fraCore.c ========================================================*/
315 extern void Fra_FraigSweep( Fra_Man_t * pManAig );
316 extern int Fra_FraigMiterStatus( Aig_Man_t * p );
317 extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
318 extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
319 extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
320 extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
321 /*=== fraHot.c ========================================================*/
322 extern Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
323 extern void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots );
324 extern void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots );
325 extern int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots );
326 extern int Fra_OneHotCount( Fra_Man_t * p, Vec_Int_t * vOneHots );
327 extern void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots );
328 extern Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots );
329 extern void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots );
330 /*=== fraImp.c ========================================================*/
331 extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
332 extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
333 extern int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
334 extern int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
335 extern void Fra_ImpCompactArray( Vec_Int_t * vImps );
336 extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
337 extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
338 extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
339 /*=== fraInd.c ========================================================*/
340 extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
341 /*=== fraIndVer.c =====================================================*/
342 extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
343 /*=== fraLcr.c ========================================================*/
344 extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit );
345 /*=== fraMan.c ========================================================*/
346 extern void Fra_ParamsDefault( Fra_Par_t * pParams );
347 extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
348 extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
349 extern void Fra_ManClean( Fra_Man_t * p, int nNodesMax );
350 extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p );
351 extern void Fra_ManFinalizeComb( Fra_Man_t * p );
352 extern void Fra_ManStop( Fra_Man_t * p );
353 extern void Fra_ManPrint( Fra_Man_t * p );
354 /*=== fraSat.c ========================================================*/
355 extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
356 extern int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
357 extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
358 extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
359 /*=== fraSec.c ========================================================*/
360 extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
361 extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult );
362 /*=== fraSim.c ========================================================*/
363 extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
364 extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
365 extern int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
366 extern int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
367 extern int Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj );
368 extern int Fra_SmlCheckOutput( Fra_Man_t * p );
369 extern void Fra_SmlSavePattern( Fra_Man_t * p );
370 extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit );
371 extern void Fra_SmlResimulate( Fra_Man_t * p );
372 extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
373 extern void Fra_SmlStop( Fra_Sml_t * p );
374 extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter );
375 extern Fra_Sml_t * Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose );
376 extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter );
377 extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
378 extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
379
380 ABC_NAMESPACE_HEADER_END
381
382
383
384 #endif
385
386 ////////////////////////////////////////////////////////////////////////
387 /// END OF FILE ///
388 ////////////////////////////////////////////////////////////////////////
389
390