1 /**CFile****************************************************************
2
3 FileName [abs.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Abstraction package.]
8
9 Synopsis [External declarations.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__proof_abs__Abs_h
22 #define ABC__proof_abs__Abs_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include "aig/gia/gia.h"
30 #include "aig/gia/giaAig.h"
31 #include "aig/saig/saig.h"
32
33 ////////////////////////////////////////////////////////////////////////
34 /// PARAMETERS ///
35 ////////////////////////////////////////////////////////////////////////
36
37
38 ABC_NAMESPACE_HEADER_START
39
40
41 ////////////////////////////////////////////////////////////////////////
42 /// BASIC TYPES ///
43 ////////////////////////////////////////////////////////////////////////
44
45 // abstraction parameters
46 typedef struct Abs_Par_t_ Abs_Par_t;
47 struct Abs_Par_t_
48 {
49 int nFramesMax; // maximum frames
50 int nFramesStart; // starting frame
51 int nFramesPast; // overlap frames
52 int nConfLimit; // conflict limit
53 int nLearnedMax; // max number of learned clauses
54 int nLearnedStart; // max number of learned clauses
55 int nLearnedDelta; // delta increase of learned clauses
56 int nLearnedPerce; // percentage of clauses to leave
57 int nTimeOut; // timeout in seconds
58 int nRatioMin; // stop when less than this % of object is unabstracted
59 int nRatioMin2; // stop when less than this % of object is unabstracted during refinement
60 int nRatioMax; // restart when the number of abstracted object is more than this
61 int fUseTermVars; // use terminal variables
62 int fUseRollback; // use rollback to the starting number of frames
63 int fPropFanout; // propagate fanout implications
64 int fAddLayer; // refinement strategy by adding layers
65 int fNewRefine; // uses new refinement heuristics
66 int fUseSkip; // skip proving intermediate timeframes
67 int fUseSimple; // use simple CNF construction
68 int fSkipHash; // skip hashing CNF while unrolling
69 int fUseFullProof; // use full proof for UNSAT cores
70 int fDumpVabs; // dumps the abstracted model
71 int fDumpMabs; // dumps the original AIG with abstraction map
72 int fCallProver; // calls the prover
73 int fSimpProver; // calls simplification before prover
74 char * pFileVabs; // dumps the abstracted model into this file
75 int fVerbose; // verbose flag
76 int fVeryVerbose; // print additional information
77 int iFrame; // the number of frames covered
78 int iFrameProved; // the number of frames proved
79 int nFramesNoChange; // the number of last frames without changes
80 int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
81 };
82
83 // old abstraction parameters
84 typedef struct Gia_ParAbs_t_ Gia_ParAbs_t;
85 struct Gia_ParAbs_t_
86 {
87 int Algo; // the algorithm to be used
88 int nFramesMax; // timeframes for PBA
89 int nConfMax; // conflicts for PBA
90 int fDynamic; // dynamic unfolding for PBA
91 int fConstr; // use constraints
92 int nFramesBmc; // timeframes for BMC
93 int nConfMaxBmc; // conflicts for BMC
94 int nStableMax; // the number of stable frames to quit
95 int nRatio; // ratio of flops to quit
96 int TimeOut; // approximate timeout in seconds
97 int TimeOutVT; // approximate timeout in seconds
98 int nBobPar; // Bob's parameter
99 int fUseBdds; // use BDDs to refine abstraction
100 int fUseDprove; // use 'dprove' to refine abstraction
101 int fUseStart; // use starting frame
102 int fVerbose; // verbose output
103 int fVeryVerbose; // printing additional information
104 int Status; // the problem status
105 int nFramesDone; // the number of frames covered
106 };
107
108 ////////////////////////////////////////////////////////////////////////
109 /// MACRO DEFINITIONS ///
110 ////////////////////////////////////////////////////////////////////////
111
Ga2_ObjOffset(Gia_Man_t * p,Gia_Obj_t * pObj)112 static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
Ga2_ObjLeaveNum(Gia_Man_t * p,Gia_Obj_t * pObj)113 static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
Ga2_ObjLeavePtr(Gia_Man_t * p,Gia_Obj_t * pObj)114 static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
Ga2_ObjTruth(Gia_Man_t * p,Gia_Obj_t * pObj)115 static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
Ga2_ObjRefNum(Gia_Man_t * p,Gia_Obj_t * pObj)116 static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
Ga2_ObjLeaves(Gia_Man_t * p,Gia_Obj_t * pObj)117 static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
118
119 ////////////////////////////////////////////////////////////////////////
120 /// FUNCTION DECLARATIONS ///
121 ////////////////////////////////////////////////////////////////////////
122
123 /*=== abs.c =========================================================*/
124 /*=== absDup.c =========================================================*/
125 extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
126 extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
127 extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes );
128 extern void Gia_ManPrintFlopClasses( Gia_Man_t * p );
129 extern void Gia_ManPrintObjClasses( Gia_Man_t * p );
130 extern void Gia_ManPrintGateClasses( Gia_Man_t * p );
131 /*=== absGla.c =========================================================*/
132 extern int Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars );
133 /*=== absGlaOld.c =========================================================*/
134 extern int Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta );
135 /*=== absIter.c =========================================================*/
136 extern Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
137 /*=== absPth.c =========================================================*/
138 extern void Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose );
139 extern void Gia_GlaProveCancel( int fVerbose );
140 extern int Gia_GlaProveCheck( int fVerbose );
141 /*=== absVta.c =========================================================*/
142 extern int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars );
143 /*=== absUtil.c =========================================================*/
144 extern void Abs_ParSetDefaults( Abs_Par_t * p );
145 extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
146 extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
147 extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
148 extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
149 extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
150 extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
151
152 /*=== absRpm.c =========================================================*/
153 extern Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose );
154 /*=== absRpmOld.c =========================================================*/
155 extern Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose );
156 extern void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p );
157 extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
158
159 /*=== absOldCex.c ==========================================================*/
160 extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
161 extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
162 /*=== absOldRef.c ==========================================================*/
163 extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
164 /*=== absOldSat.c ==========================================================*/
165 extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
166 /*=== absOldSim.c ==========================================================*/
167 extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );
168
169
170 ABC_NAMESPACE_HEADER_END
171
172 #endif
173
174 ////////////////////////////////////////////////////////////////////////
175 /// END OF FILE ///
176 ////////////////////////////////////////////////////////////////////////
177
178