1 /**CFile****************************************************************
2
3 FileName [bmcBmc2.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
8
9 Synopsis [Simple BMC package.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: bmcBmc2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "sat/cnf/cnf.h"
22 #include "sat/bsat/satStore.h"
23 #include "sat/satoko/satoko.h"
24 #include "proof/ssw/ssw.h"
25 #include "bmc.h"
26
27 ABC_NAMESPACE_IMPL_START
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 //#define AIG_VISITED ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
34
35 typedef struct Saig_Bmc_t_ Saig_Bmc_t;
36 struct Saig_Bmc_t_
37 {
38 // parameters
39 int nFramesMax; // the max number of timeframes to consider
40 int nNodesMax; // the max number of nodes to add
41 int nConfMaxOne; // the max number of conflicts at a target
42 int nConfMaxAll; // the max number of conflicts for all targets
43 int fVerbose; // enables verbose output
44 // AIG managers
45 Aig_Man_t * pAig; // the user's AIG manager
46 Aig_Man_t * pFrm; // Frames manager
47 Vec_Int_t * vVisited; // nodes visited in Frames
48 // node mapping
49 int nObjs; // the largest number of an AIG object
50 Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes
51 // SAT solver
52 sat_solver * pSat; // SAT solver
53 satoko_t * pSat2; // SAT solver
54 int nSatVars; // the number of used SAT variables
55 Vec_Int_t * vObj2Var; // mapping of frames objects in CNF variables
56 int nStitchVars;
57 // subproblems
58 Vec_Ptr_t * vTargets; // targets to be solved in this interval
59 int iFramePrev; // previous frame
60 int iFrameLast; // last frame
61 int iOutputLast; // last output
62 int iFrameFail; // failed frame
63 int iOutputFail; // failed output
64 };
65
Saig_BmcObjFrame(Saig_Bmc_t * p,Aig_Obj_t * pObj,int i)66 static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
67 {
68 // return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );
69 Aig_Obj_t * pRes;
70 Vec_Int_t * vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
71 int iObjLit = Vec_IntEntry( vFrame, Aig_ObjId(pObj) );
72 if ( iObjLit == -1 )
73 return NULL;
74 pRes = Aig_ManObj( p->pFrm, Abc_Lit2Var(iObjLit) );
75 if ( pRes == NULL )
76 Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), -1 );
77 else
78 pRes = Aig_NotCond( pRes, Abc_LitIsCompl(iObjLit) );
79 return pRes;
80 }
Saig_BmcObjSetFrame(Saig_Bmc_t * p,Aig_Obj_t * pObj,int i,Aig_Obj_t * pNode)81 static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode )
82 {
83 // Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );
84 Vec_Int_t * vFrame;
85 int iObjLit;
86 if ( i == Vec_PtrSize(p->vAig2Frm) )
87 Vec_PtrPush( p->vAig2Frm, Vec_IntStartFull(p->nObjs) );
88 assert( i < Vec_PtrSize(p->vAig2Frm) );
89 vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
90 if ( pNode == NULL )
91 iObjLit = -1;
92 else
93 iObjLit = Abc_Var2Lit( Aig_ObjId(Aig_Regular(pNode)), Aig_IsComplement(pNode) );
94 Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), iObjLit );
95 }
96
Saig_BmcObjChild0(Saig_Bmc_t * p,Aig_Obj_t * pObj,int i)97 static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)); }
Saig_BmcObjChild1(Saig_Bmc_t * p,Aig_Obj_t * pObj,int i)98 static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)); }
99
Saig_BmcSatNum(Saig_Bmc_t * p,Aig_Obj_t * pObj)100 static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); }
Saig_BmcSetSatNum(Saig_Bmc_t * p,Aig_Obj_t * pObj,int Num)101 static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); }
102
103 ////////////////////////////////////////////////////////////////////////
104 /// FUNCTION DEFINITIONS ///
105 ////////////////////////////////////////////////////////////////////////
106
107 #define ABS_ZER 1
108 #define ABS_ONE 2
109 #define ABS_UND 3
110
Abs_ManSimInfoNot(int Value)111 static inline int Abs_ManSimInfoNot( int Value )
112 {
113 if ( Value == ABS_ZER )
114 return ABS_ONE;
115 if ( Value == ABS_ONE )
116 return ABS_ZER;
117 return ABS_UND;
118 }
119
Abs_ManSimInfoAnd(int Value0,int Value1)120 static inline int Abs_ManSimInfoAnd( int Value0, int Value1 )
121 {
122 if ( Value0 == ABS_ZER || Value1 == ABS_ZER )
123 return ABS_ZER;
124 if ( Value0 == ABS_ONE && Value1 == ABS_ONE )
125 return ABS_ONE;
126 return ABS_UND;
127 }
128
Abs_ManSimInfoGet(Vec_Ptr_t * vSimInfo,Aig_Obj_t * pObj,int iFrame)129 static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
130 {
131 unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
132 return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
133 }
134
Abs_ManSimInfoSet(Vec_Ptr_t * vSimInfo,Aig_Obj_t * pObj,int iFrame,int Value)135 static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
136 {
137 unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
138 assert( Value >= ABS_ZER && Value <= ABS_UND );
139 Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
140 pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
141 }
142
143 /**Function*************************************************************
144
145 Synopsis [Performs ternary simulation for one node.]
146
147 Description []
148
149 SideEffects []
150
151 SeeAlso []
152
153 ***********************************************************************/
Abs_ManExtendOneEval_rec(Vec_Ptr_t * vSimInfo,Aig_Man_t * p,Aig_Obj_t * pObj,int iFrame)154 int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame )
155 {
156 int Value0, Value1, Value;
157 Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
158 if ( Value )
159 return Value;
160 if ( Aig_ObjIsCi(pObj) )
161 {
162 assert( Saig_ObjIsLo(p, pObj) );
163 Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 );
164 Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
165 return Value;
166 }
167 Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame );
168 if ( Aig_ObjFaninC0(pObj) )
169 Value0 = Abs_ManSimInfoNot( Value0 );
170 if ( Aig_ObjIsCo(pObj) )
171 {
172 Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
173 return Value0;
174 }
175 assert( Aig_ObjIsNode(pObj) );
176 if ( Value0 == ABS_ZER )
177 Value = ABS_ZER;
178 else
179 {
180 Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame );
181 if ( Aig_ObjFaninC1(pObj) )
182 Value1 = Abs_ManSimInfoNot( Value1 );
183 Value = Abs_ManSimInfoAnd( Value0, Value1 );
184 }
185 Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
186 assert( Value );
187 return Value;
188 }
189
190 /**Function*************************************************************
191
192 Synopsis [Performs ternary simulation for one design.]
193
194 Description [The returned array contains the result of ternary
195 simulation for all the frames where the output could be proved 0.]
196
197 SideEffects []
198
199 SeeAlso []
200
201 ***********************************************************************/
Abs_ManTernarySimulate(Aig_Man_t * p,int nFramesMax,int fVerbose)202 Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose )
203 {
204 Vec_Ptr_t * vSimInfo;
205 Aig_Obj_t * pObj;
206 int i, f, nFramesLimit, nFrameWords;
207 abctime clk = Abc_Clock();
208 assert( Aig_ManRegNum(p) > 0 );
209 // the maximum number of frames will be determined to use at most 200Mb of RAM
210 nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
211 nFramesLimit = Abc_MinInt( nFramesLimit, nFramesMax );
212 nFrameWords = Abc_BitWordNum( 2 * Aig_ManObjNum(p) );
213 // allocate simulation info
214 vSimInfo = Vec_PtrAlloc( nFramesLimit );
215 for ( f = 0; f < nFramesLimit; f++ )
216 {
217 Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) );
218 if ( f == 0 )
219 {
220 Saig_ManForEachLo( p, pObj, i )
221 Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER );
222 }
223 Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE );
224 Saig_ManForEachPi( p, pObj, i )
225 Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND );
226 Saig_ManForEachPo( p, pObj, i )
227 Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f );
228 // check if simulation has derived at least one fail or unknown
229 Saig_ManForEachPo( p, pObj, i )
230 if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER )
231 {
232 if ( fVerbose )
233 {
234 printf( "Ternary sim found non-zero output in frame %d. Used %5.2f MB. ",
235 f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
236 ABC_PRT( "Time", Abc_Clock() - clk );
237 }
238 return vSimInfo;
239 }
240 }
241 if ( fVerbose )
242 {
243 printf( "Ternary sim proved all outputs in the first %d frames. Used %5.2f MB. ",
244 nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
245 ABC_PRT( "Time", Abc_Clock() - clk );
246 }
247 return vSimInfo;
248 }
249
250 /**Function*************************************************************
251
252 Synopsis [Free the array of simulation info.]
253
254 Description []
255
256 SideEffects []
257
258 SeeAlso []
259
260 ***********************************************************************/
Abs_ManFreeAray(Vec_Ptr_t * p)261 void Abs_ManFreeAray( Vec_Ptr_t * p )
262 {
263 void * pTemp;
264 int i;
265 Vec_PtrForEachEntry( void *, p, pTemp, i )
266 ABC_FREE( pTemp );
267 Vec_PtrFree( p );
268 }
269
270
271 /**Function*************************************************************
272
273 Synopsis [Create manager.]
274
275 Description []
276
277 SideEffects []
278
279 SeeAlso []
280
281 ***********************************************************************/
Saig_BmcManStart(Aig_Man_t * pAig,int nFramesMax,int nNodesMax,int nConfMaxOne,int nConfMaxAll,int fVerbose,int fUseSatoko)282 Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fUseSatoko )
283 {
284 Saig_Bmc_t * p;
285 Aig_Obj_t * pObj;
286 int i, Lit;
287 // assert( Aig_ManRegNum(pAig) > 0 );
288 p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
289 memset( p, 0, sizeof(Saig_Bmc_t) );
290 // set parameters
291 p->nFramesMax = nFramesMax;
292 p->nNodesMax = nNodesMax;
293 p->nConfMaxOne = nConfMaxOne;
294 p->nConfMaxAll = nConfMaxAll;
295 p->fVerbose = fVerbose;
296 p->pAig = pAig;
297 p->nObjs = Aig_ManObjNumMax(pAig);
298 // create node and variable mappings
299 p->vAig2Frm = Vec_PtrAlloc( 100 );
300 p->vObj2Var = Vec_IntAlloc( 0 );
301 Vec_IntFill( p->vObj2Var, p->nObjs, 0 );
302 // start the AIG manager and map primary inputs
303 p->pFrm = Aig_ManStart( p->nObjs );
304 Saig_ManForEachLo( pAig, pObj, i )
305 Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) );
306 // create SAT solver
307 p->nSatVars = 1;
308 Lit = toLit( p->nSatVars );
309 if ( fUseSatoko )
310 {
311 satoko_opts_t opts;
312 satoko_default_opts(&opts);
313 opts.conf_limit = nConfMaxOne;
314 p->pSat2 = satoko_create();
315 satoko_configure(p->pSat2, &opts);
316 satoko_setnvars(p->pSat2, 2000);
317 satoko_add_clause( p->pSat2, &Lit, 1 );
318 }
319 else
320 {
321 p->pSat = sat_solver_new();
322 p->pSat->nLearntStart = 10000;//p->pPars->nLearnedStart;
323 p->pSat->nLearntDelta = 5000;//p->pPars->nLearnedDelta;
324 p->pSat->nLearntRatio = 75;//p->pPars->nLearnedPerce;
325 p->pSat->nLearntMax = p->pSat->nLearntStart;
326 sat_solver_setnvars( p->pSat, 2000 );
327 sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
328 }
329 Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
330 // other data structures
331 p->vTargets = Vec_PtrAlloc( 1000 );
332 p->vVisited = Vec_IntAlloc( 1000 );
333 p->iOutputFail = -1;
334 p->iFrameFail = -1;
335 return p;
336 }
337
338 /**Function*************************************************************
339
340 Synopsis [Delete manager.]
341
342 Description []
343
344 SideEffects []
345
346 SeeAlso []
347
348 ***********************************************************************/
Saig_BmcManStop(Saig_Bmc_t * p)349 void Saig_BmcManStop( Saig_Bmc_t * p )
350 {
351 Aig_ManStop( p->pFrm );
352 Vec_VecFree( (Vec_Vec_t *)p->vAig2Frm );
353 Vec_IntFree( p->vObj2Var );
354 if ( p->pSat ) sat_solver_delete( p->pSat );
355 if ( p->pSat2 ) satoko_destroy( p->pSat2 );
356 Vec_PtrFree( p->vTargets );
357 Vec_IntFree( p->vVisited );
358 ABC_FREE( p );
359 }
360
361 /**Function*************************************************************
362
363 Synopsis [Explores the possibility of constructing the output.]
364
365 Description []
366
367 SideEffects []
368
369 SeeAlso []
370
371 ***********************************************************************/
372 /*
373 Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
374 {
375 Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
376 pRes = Saig_BmcObjFrame( p, pObj, i );
377 if ( pRes != NULL )
378 return pRes;
379 if ( Saig_ObjIsPi( p->pAig, pObj ) )
380 pRes = AIG_VISITED;
381 else if ( Saig_ObjIsLo( p->pAig, pObj ) )
382 pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
383 else if ( Aig_ObjIsCo( pObj ) )
384 {
385 pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
386 if ( pRes != AIG_VISITED )
387 pRes = Saig_BmcObjChild0( p, pObj, i );
388 }
389 else
390 {
391 p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
392 if ( p0 != AIG_VISITED )
393 p0 = Saig_BmcObjChild0( p, pObj, i );
394 p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i );
395 if ( p1 != AIG_VISITED )
396 p1 = Saig_BmcObjChild1( p, pObj, i );
397
398 if ( p0 == Aig_Not(p1) )
399 pRes = Aig_ManConst0(p->pFrm);
400 else if ( Aig_Regular(p0) == pConst1 )
401 pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm);
402 else if ( Aig_Regular(p1) == pConst1 )
403 pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm);
404 else
405 pRes = AIG_VISITED;
406
407 if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) )
408 pRes = AIG_VISITED;
409 }
410 Saig_BmcObjSetFrame( p, pObj, i, pRes );
411 return pRes;
412 }
413 */
414
415 /**Function*************************************************************
416
417 Synopsis [Performs the actual construction of the output.]
418
419 Description []
420
421 SideEffects []
422
423 SeeAlso []
424
425 ***********************************************************************/
Saig_BmcIntervalConstruct_rec(Saig_Bmc_t * p,Aig_Obj_t * pObj,int i,Vec_Int_t * vVisited)426 Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Int_t * vVisited )
427 {
428 Aig_Obj_t * pRes;
429 pRes = Saig_BmcObjFrame( p, pObj, i );
430 if ( pRes != NULL )
431 return pRes;
432 if ( Saig_ObjIsPi( p->pAig, pObj ) )
433 pRes = Aig_ObjCreateCi(p->pFrm);
434 else if ( Saig_ObjIsLo( p->pAig, pObj ) )
435 pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited );
436 else if ( Aig_ObjIsCo( pObj ) )
437 {
438 Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
439 pRes = Saig_BmcObjChild0( p, pObj, i );
440 }
441 else
442 {
443 Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
444 if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) )
445 pRes = Aig_ManConst0(p->pFrm);
446 else
447 {
448 Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
449 pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
450 }
451 }
452 assert( pRes != NULL );
453 Saig_BmcObjSetFrame( p, pObj, i, pRes );
454 Vec_IntPush( vVisited, Aig_ObjId(pObj) );
455 Vec_IntPush( vVisited, i );
456 return pRes;
457 }
458
459 /**Function*************************************************************
460
461 Synopsis [Adds new AIG nodes to the frames.]
462
463 Description []
464
465 SideEffects []
466
467 SeeAlso []
468
469 ***********************************************************************/
Saig_BmcInterval(Saig_Bmc_t * p)470 void Saig_BmcInterval( Saig_Bmc_t * p )
471 {
472 Aig_Obj_t * pTarget;
473 int i, iObj, iFrame;
474 int nNodes = Aig_ManObjNum( p->pFrm );
475 Vec_PtrClear( p->vTargets );
476 p->iFramePrev = p->iFrameLast;
477 for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
478 {
479 if ( p->iOutputLast == 0 )
480 {
481 Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
482 }
483 for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
484 {
485 if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
486 return;
487 // Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast );
488 Vec_IntClear( p->vVisited );
489 pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
490 Vec_PtrPush( p->vTargets, pTarget );
491 Aig_ObjCreateCo( p->pFrm, pTarget );
492 Aig_ManCleanup( p->pFrm ); // it is not efficient to cleanup the whole manager!!!
493 // check if the node is gone
494 Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i )
495 Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame );
496 // it is not efficient to remove nodes, which may be used later!!!
497 }
498 }
499 }
500
501 /**Function*************************************************************
502
503 Synopsis [Performs the actual construction of the output.]
504
505 Description []
506
507 SideEffects []
508
509 SeeAlso []
510
511 ***********************************************************************/
Saig_BmcIntervalToAig_rec(Saig_Bmc_t * p,Aig_Man_t * pNew,Aig_Obj_t * pObj)512 Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
513 {
514 if ( pObj->pData )
515 return (Aig_Obj_t *)pObj->pData;
516 Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
517 if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) )
518 {
519 p->nStitchVars += !Aig_ObjIsCi(pObj);
520 return (Aig_Obj_t *)(pObj->pData = Aig_ObjCreateCi(pNew));
521 }
522 Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
523 Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
524 assert( pObj->pData == NULL );
525 return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
526 }
527
528 /**Function*************************************************************
529
530 Synopsis [Creates AIG of the newly added nodes.]
531
532 Description []
533
534 SideEffects []
535
536 SeeAlso []
537
538 ***********************************************************************/
Saig_BmcIntervalToAig(Saig_Bmc_t * p)539 Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
540 {
541 Aig_Man_t * pNew;
542 Aig_Obj_t * pObj, * pObjNew;
543 int i;
544 Aig_ManForEachObj( p->pFrm, pObj, i )
545 assert( pObj->pData == NULL );
546
547 pNew = Aig_ManStart( p->nNodesMax );
548 Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
549 Vec_IntClear( p->vVisited );
550 Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) );
551 Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
552 {
553 // assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
554 pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
555 assert( !Aig_IsComplement(pObjNew) );
556 Aig_ObjCreateCo( pNew, pObjNew );
557 }
558 return pNew;
559 }
560
561 /**Function*************************************************************
562
563 Synopsis [Derives CNF for the newly added nodes.]
564
565 Description []
566
567 SideEffects []
568
569 SeeAlso []
570
571 ***********************************************************************/
Saig_BmcLoadCnf(Saig_Bmc_t * p,Cnf_Dat_t * pCnf)572 void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
573 {
574 Aig_Obj_t * pObj, * pObjNew;
575 int i, Lits[2], VarNumOld, VarNumNew;
576 Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i )
577 {
578 // get the new variable of this node
579 pObjNew = (Aig_Obj_t *)pObj->pData;
580 pObj->pData = NULL;
581 VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
582 if ( VarNumNew == -1 )
583 continue;
584 // get the old variable of this node
585 VarNumOld = Saig_BmcSatNum( p, pObj );
586 if ( VarNumOld == 0 )
587 {
588 Saig_BmcSetSatNum( p, pObj, VarNumNew );
589 continue;
590 }
591 // add clauses connecting existing variables
592 Lits[0] = toLitCond( VarNumOld, 0 );
593 Lits[1] = toLitCond( VarNumNew, 1 );
594 if ( p->pSat2 )
595 {
596 if ( !satoko_add_clause( p->pSat2, Lits, 2 ) )
597 assert( 0 );
598 }
599 else
600 {
601 if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
602 assert( 0 );
603 }
604 Lits[0] = toLitCond( VarNumOld, 1 );
605 Lits[1] = toLitCond( VarNumNew, 0 );
606 if ( p->pSat2 )
607 {
608 if ( !satoko_add_clause( p->pSat2, Lits, 2 ) )
609 assert( 0 );
610 }
611 else
612 {
613 if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
614 assert( 0 );
615 }
616 }
617 // add CNF to the SAT solver
618 if ( p->pSat2 )
619 {
620 for ( i = 0; i < pCnf->nClauses; i++ )
621 if ( !satoko_add_clause( p->pSat2, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
622 break;
623 }
624 else
625 {
626 for ( i = 0; i < pCnf->nClauses; i++ )
627 if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
628 break;
629 }
630 if ( i < pCnf->nClauses )
631 printf( "SAT solver became UNSAT after adding clauses.\n" );
632 }
633
634 /**Function*************************************************************
635
636 Synopsis [Solves targets with the given resource limit.]
637
638 Description []
639
640 SideEffects []
641
642 SeeAlso []
643
644 ***********************************************************************/
Saig_BmcDeriveFailed(Saig_Bmc_t * p,int iTargetFail)645 void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail )
646 {
647 int k;
648 p->iOutputFail = p->iOutputLast;
649 p->iFrameFail = p->iFrameLast;
650 for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
651 {
652 if ( p->iOutputFail == 0 )
653 {
654 p->iOutputFail = Saig_ManPoNum(p->pAig);
655 p->iFrameFail--;
656 }
657 p->iOutputFail--;
658 }
659 }
660
661 /**Function*************************************************************
662
663 Synopsis [Solves targets with the given resource limit.]
664
665 Description []
666
667 SideEffects []
668
669 SeeAlso []
670
671 ***********************************************************************/
Saig_BmcGenerateCounterExample(Saig_Bmc_t * p)672 Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
673 {
674 Abc_Cex_t * pCex;
675 Aig_Obj_t * pObj, * pObjFrm;
676 int i, f, iVarNum;
677 // start the counter-example
678 pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
679 pCex->iFrame = p->iFrameFail;
680 pCex->iPo = p->iOutputFail;
681 // copy the bit data
682 for ( f = 0; f <= p->iFrameFail; f++ )
683 {
684 Saig_ManForEachPi( p->pAig, pObj, i )
685 {
686 pObjFrm = Saig_BmcObjFrame( p, pObj, f );
687 if ( pObjFrm == NULL )
688 continue;
689 iVarNum = Saig_BmcSatNum( p, pObjFrm );
690 if ( iVarNum == 0 )
691 continue;
692 if ( p->pSat2 ? satoko_read_cex_varvalue(p->pSat2, iVarNum) : sat_solver_var_value(p->pSat, iVarNum) )
693 Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
694 }
695 }
696 // verify the counter example
697 if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
698 {
699 printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
700 Abc_CexFree( pCex );
701 pCex = NULL;
702 }
703 return pCex;
704 }
705
706 /**Function*************************************************************
707
708 Synopsis [Solves targets with the given resource limit.]
709
710 Description []
711
712 SideEffects []
713
714 SeeAlso []
715
716 ***********************************************************************/
Saig_BmcSolveTargets(Saig_Bmc_t * p,int nStart,int * pnOutsSolved)717 int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
718 {
719 Aig_Obj_t * pObj;
720 int i, k, VarNum, Lit, status, RetValue;
721 assert( Vec_PtrSize(p->vTargets) > 0 );
722 if ( p->pSat && p->pSat->qtail != p->pSat->qhead )
723 {
724 RetValue = sat_solver_simplify(p->pSat);
725 assert( RetValue != 0 );
726 }
727 Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
728 {
729 if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
730 continue;
731 if ( p->nConfMaxAll && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
732 return l_Undef;
733 VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
734 Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
735 if ( p->pSat2 )
736 RetValue = satoko_solve_assumptions_limit( p->pSat2, &Lit, 1, p->nConfMaxOne );
737 else
738 RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
739 if ( RetValue == l_False ) // unsat
740 {
741 // add final unit clause
742 Lit = lit_neg( Lit );
743 if ( p->pSat2 )
744 status = satoko_add_clause( p->pSat2, &Lit, 1 );
745 else
746 status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
747 assert( status );
748 if ( p->pSat )
749 {
750 // add learned units
751 for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
752 {
753 Lit = veci_begin(&p->pSat->unit_lits)[k];
754 status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
755 assert( status );
756 }
757 veci_resize(&p->pSat->unit_lits, 0);
758 // propagate units
759 sat_solver_compress( p->pSat );
760 }
761 continue;
762 }
763 if ( RetValue == l_Undef ) // undecided
764 return l_Undef;
765 // generate counter-example
766 Saig_BmcDeriveFailed( p, i );
767 p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
768
769 {
770 // extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex );
771 // Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
772 }
773 return l_True;
774 }
775 return l_False;
776 }
777
778 /**Function*************************************************************
779
780 Synopsis []
781
782 Description []
783
784 SideEffects []
785
786 SeeAlso []
787
788 ***********************************************************************/
Saig_BmcAddTargetsAsPos(Saig_Bmc_t * p)789 void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
790 {
791 Aig_Obj_t * pObj;
792 int i;
793 Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
794 Aig_ObjCreateCo( p->pFrm, pObj );
795 Aig_ManPrintStats( p->pFrm );
796 Aig_ManCleanup( p->pFrm );
797 Aig_ManPrintStats( p->pFrm );
798 }
799
800 /**Function*************************************************************
801
802 Synopsis [Performs BMC with the given parameters.]
803
804 Description []
805
806 SideEffects []
807
808 SeeAlso []
809
810 ***********************************************************************/
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)811 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 )
812 {
813 Saig_Bmc_t * p;
814 Aig_Man_t * pNew;
815 Cnf_Dat_t * pCnf;
816 int nOutsSolved = 0;
817 int Iter, RetValue = -1;
818 abctime nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
819 abctime clk = Abc_Clock(), clk2, clkTotal = Abc_Clock();
820 int Status = -1;
821 /*
822 Vec_Ptr_t * vSimInfo;
823 vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
824 Abs_ManFreeAray( vSimInfo );
825 */
826 if ( fVerbose )
827 {
828 printf( "Running \"bmc2\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
829 Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
830 Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
831 printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n",
832 nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
833 }
834 nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
835 p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose, fUseSatoko );
836 // set runtime limit
837 if ( nTimeOut )
838 {
839 if ( p->pSat2 )
840 satoko_set_runtime_limit( p->pSat2, nTimeToStop );
841 else
842 sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
843 }
844 for ( Iter = 0; ; Iter++ )
845 {
846 clk2 = Abc_Clock();
847 // add new logic interval to frames
848 Saig_BmcInterval( p );
849 // Saig_BmcAddTargetsAsPos( p );
850 if ( Vec_PtrSize(p->vTargets) == 0 )
851 break;
852 // convert logic slice into new AIG
853 pNew = Saig_BmcIntervalToAig( p );
854 //printf( "StitchVars = %d.\n", p->nStitchVars );
855 // derive CNF for the new AIG
856 pCnf = Cnf_Derive( pNew, Aig_ManCoNum(pNew) );
857 Cnf_DataLift( pCnf, p->nSatVars );
858 p->nSatVars += pCnf->nVars;
859 // add this CNF to the solver
860 Saig_BmcLoadCnf( p, pCnf );
861 Cnf_DataFree( pCnf );
862 Aig_ManStop( pNew );
863 // solve the targets
864 RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
865 if ( fVerbose )
866 {
867 printf( "%4d : F =%5d. O =%4d. And =%8d. Var =%8d. Conf =%7d. ",
868 Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars,
869 p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2) );
870 printf( "%4.0f MB", 4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
871 printf( "%9.2f sec", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
872 printf( "\n" );
873 fflush( stdout );
874 }
875 if ( RetValue != l_False )
876 break;
877 // check the timeout
878 if ( nTimeOut && Abc_Clock() > nTimeToStop )
879 {
880 if ( !fSilent )
881 printf( "Reached timeout (%d seconds).\n", nTimeOut );
882 if ( piFrames )
883 *piFrames = p->iFrameLast-1;
884 Saig_BmcManStop( p );
885 return Status;
886 }
887 }
888 if ( RetValue == l_True )
889 {
890 assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
891 if ( !fSilent )
892 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ",
893 p->iOutputFail, p->pAig->pName, p->iFrameFail );
894 Status = 0;
895 if ( piFrames )
896 *piFrames = p->iFrameFail - 1;
897 }
898 else // if ( RetValue == l_False || RetValue == l_Undef )
899 {
900 if ( !fSilent )
901 Abc_Print( 1, "No output failed in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) );
902 if ( piFrames )
903 {
904 if ( p->iOutputLast > 0 )
905 *piFrames = p->iFramePrev - 2;
906 else
907 *piFrames = p->iFramePrev - 1;
908 }
909 }
910 if ( !fSilent )
911 {
912 if ( fVerbOverwrite )
913 {
914 ABC_PRTr( "Time", Abc_Clock() - clk );
915 }
916 else
917 {
918 ABC_PRT( "Time", Abc_Clock() - clk );
919 }
920 if ( RetValue != l_True )
921 {
922 if ( p->iFrameLast >= p->nFramesMax )
923 printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
924 else if ( p->nConfMaxAll && (p->pSat ? (int)p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > p->nConfMaxAll )
925 printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
926 else if ( nTimeOut && Abc_Clock() > nTimeToStop )
927 printf( "Reached timeout (%d seconds).\n", nTimeOut );
928 else
929 printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
930 }
931 }
932 Saig_BmcManStop( p );
933 fflush( stdout );
934 return Status;
935 }
936
937
938 ////////////////////////////////////////////////////////////////////////
939 /// END OF FILE ///
940 ////////////////////////////////////////////////////////////////////////
941
942
943 ABC_NAMESPACE_IMPL_END
944
945