1 /**CFile****************************************************************
2
3 FileName [bmc.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
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: bmc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC___sat_bmc_BMC_h
22 #define ABC___sat_bmc_BMC_h
23
24
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #include "aig/saig/saig.h"
30 #include "aig/gia/gia.h"
31
32 ////////////////////////////////////////////////////////////////////////
33 /// PARAMETERS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 ABC_NAMESPACE_HEADER_START
37
38 //#define USE_NODE_ORDER 1
39
40 ////////////////////////////////////////////////////////////////////////
41 /// BASIC TYPES ///
42 ////////////////////////////////////////////////////////////////////////
43
44
45 // exact synthesis parameters
46
47 typedef struct Bmc_EsPar_t_ Bmc_EsPar_t;
48 struct Bmc_EsPar_t_
49 {
50 int nVars;
51 int nNodes;
52 int nLutSize;
53 int nMajSupp;
54 int fMajority;
55 int fUseIncr;
56 int fOnlyAnd;
57 int fGlucose;
58 int fOrderNodes;
59 int fEnumSols;
60 int fFewerVars;
61 int RuntimeLim;
62 int fVerbose;
63 char * pTtStr;
64 };
65
Bmc_EsParSetDefault(Bmc_EsPar_t * pPars)66 static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
67 {
68 memset( pPars, 0, sizeof(Bmc_EsPar_t) );
69 pPars->nVars = 0;
70 pPars->nNodes = 0;
71 pPars->nLutSize = 2;
72 pPars->nMajSupp = 0;
73 pPars->fMajority = 0;
74 pPars->fUseIncr = 0;
75 pPars->fOnlyAnd = 0;
76 pPars->fGlucose = 0;
77 pPars->fOrderNodes = 0;
78 pPars->fEnumSols = 0;
79 pPars->fFewerVars = 0;
80 pPars->RuntimeLim = 0;
81 pPars->fVerbose = 1;
82 }
83
84
85 // unrolling manager
86 typedef struct Unr_Man_t_ Unr_Man_t;
87
88 typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
89 struct Saig_ParBmc_t_
90 {
91 int nStart; // starting timeframe
92 int nFramesMax; // maximum number of timeframes
93 int nConfLimit; // maximum number of conflicts at a node
94 int nConfLimitJump; // maximum number of conflicts after jumping
95 int nFramesJump; // the number of tiemframes to jump
96 int nTimeOut; // approximate timeout in seconds
97 int nTimeOutGap; // approximate timeout in seconds since the last change
98 int nTimeOutOne; // timeout per output in multi-output solving
99 int nPisAbstract; // the number of PIs to abstract
100 int fSolveAll; // does not stop at the first SAT output
101 int fStoreCex; // enable storing CEXes in the MO mode
102 int fUseBridge; // use bridge interface
103 int fDropSatOuts; // replace sat outputs by constant 0
104 int nFfToAddMax; // max number of flops to add during CBA
105 int fSkipRand; // skip random decisions
106 int fNoRestarts; // disables periodic restarts
107 int fUseSatoko; // enables using Satoko
108 int fUseGlucose; // enables using Glucose 3.0
109 int nLearnedStart; // starting learned clause limit
110 int nLearnedDelta; // delta of learned clause limit
111 int nLearnedPerce; // ratio of learned clause limit
112 int fVerbose; // verbose
113 int fNotVerbose; // skip line-by-line print-out
114 char * pLogFileName; // log file name
115 int fSilent; // completely silent
116 int iFrame; // explored up to this frame
117 int nFailOuts; // the number of failed outputs
118 int nDropOuts; // the number of dropped outputs
119 abctime timeLastSolved; // the time when the last output was solved
120 int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
121 int RunId; // BMC id in this run
122 int(*pFuncStop)(int); // callback to terminate
123 };
124
125
126 typedef struct Bmc_AndPar_t_ Bmc_AndPar_t;
127 struct Bmc_AndPar_t_
128 {
129 int nStart; // starting timeframe
130 int nFramesMax; // maximum number of timeframes
131 int nFramesAdd; // the number of additional frames
132 int nConfLimit; // maximum number of conflicts at a node
133 int nTimeOut; // timeout in seconds
134 int nLutSize; // LUT size for cut computation
135 int nProcs; // the number of parallel solvers
136 int fLoadCnf; // dynamic CNF loading
137 int fDumpFrames; // dump unrolled timeframes
138 int fUseSynth; // use synthesis
139 int fUseOldCnf; // use old CNF construction
140 int fUseGlucose; // use Glucose 3.0 as the default solver
141 int fUseEliminate; // use variable elimination
142 int fVerbose; // verbose
143 int fVeryVerbose; // very verbose
144 int fNotVerbose; // skip line-by-line print-out
145 int iFrame; // explored up to this frame
146 int nFailOuts; // the number of failed outputs
147 int nDropOuts; // the number of dropped outputs
148
149 void (*pFuncOnFrameDone)(int, int, int); // callback on each frame status (frame, po, statuss)
150 };
151
152 typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t;
153 struct Bmc_BCorePar_t_
154 {
155 int iFrame; // timeframe
156 int iOutput; // property output
157 int nTimeOut; // timeout in seconds
158 char * pFilePivots; // file name with AIG IDs of pivot objects
159 char * pFileProof; // file name to write the resulting proof
160 int fVerbose; // verbose output
161 };
162
163 typedef struct Bmc_MulPar_t_ Bmc_MulPar_t;
164 struct Bmc_MulPar_t_
165 {
166 int TimeOutGlo;
167 int TimeOutLoc;
168 int TimeOutInc;
169 int TimeOutGap;
170 int TimePerOut;
171 int fUseSyn;
172 int fDumpFinal;
173 int fVerbose;
174 int fVeryVerbose;
175 };
176
177 typedef struct Bmc_ParFf_t_ Bmc_ParFf_t;
178 struct Bmc_ParFf_t_
179 {
180 char * pFileName;
181 char * pFormStr;
182 int Algo;
183 int fComplVars;
184 int fStartPats;
185 int nTimeOut;
186 int nIterCheck;
187 int nCardConstr;
188 int fNonStrict;
189 int fBasic;
190 int fFfOnly;
191 int fCheckUntest;
192 int fDump;
193 int fDumpDelay;
194 int fDumpUntest;
195 int fDumpNewFaults;
196 int fVerbose;
197 };
198
199 ////////////////////////////////////////////////////////////////////////
200 /// MACRO DEFINITIONS ///
201 ////////////////////////////////////////////////////////////////////////
202
203 ////////////////////////////////////////////////////////////////////////
204 /// FUNCTION DECLARATIONS ///
205 ////////////////////////////////////////////////////////////////////////
206
207 /*=== bmcBCore.c ==========================================================*/
208 extern void Bmc_ManBCorePerform( Gia_Man_t * pGia, Bmc_BCorePar_t * pPars );
209 /*=== bmcBmc.c ==========================================================*/
210 extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit, int fUseSatoko );
211 /*=== bmcBmc2.c ==========================================================*/
212 extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent, int fUseSatoko );
213 /*=== bmcBmc3.c ==========================================================*/
214 extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
215 extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
216 /*=== bmcBmcAnd.c ==========================================================*/
217 extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
218 /*=== bmcCexCare.c ==========================================================*/
219 extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
220 extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
221 extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
222 extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
223 extern Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
224 extern Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
225 /*=== bmcCexCut.c ==========================================================*/
226 extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
227 extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
228 /*=== bmcCexMin.c ==========================================================*/
229 extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
230 /*=== bmcCexTool.c ==========================================================*/
231 extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose );
232 extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
233 /*=== bmcICheck.c ==========================================================*/
234 extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
235 extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose );
236 /*=== bmcUnroll.c ==========================================================*/
237 extern Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
238 extern Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f );
239 extern void Unr_ManFree( Unr_Man_t * p );
240
241
242 ABC_NAMESPACE_HEADER_END
243
244
245
246 #endif
247
248 ////////////////////////////////////////////////////////////////////////
249 /// END OF FILE ///
250 ////////////////////////////////////////////////////////////////////////
251
252