1 /**CFile****************************************************************
2
3 FileName [fraBmc.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [Bounded model checking.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraBmc.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 // simulation manager
31 struct Fra_Bmc_t_
32 {
33 // parameters
34 int nPref; // the size of the prefix
35 int nDepth; // the depth of the frames
36 int nFramesAll; // the total number of timeframes
37 // implications to be filtered
38 Vec_Int_t * vImps;
39 // AIG managers
40 Aig_Man_t * pAig; // the original AIG manager
41 Aig_Man_t * pAigFrames; // initialized timeframes
42 Aig_Man_t * pAigFraig; // the fraiged initialized timeframes
43 // mapping of nodes
44 Aig_Obj_t ** pObjToFrames; // mapping of the original node into frames
45 Aig_Obj_t ** pObjToFraig; // mapping of the frames node into fraig
46 };
47
Bmc_ObjFrames(Aig_Obj_t * pObj,int i)48 static inline Aig_Obj_t * Bmc_ObjFrames( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i]; }
Bmc_ObjSetFrames(Aig_Obj_t * pObj,int i,Aig_Obj_t * pNode)49 static inline void Bmc_ObjSetFrames( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i] = pNode; }
50
Bmc_ObjFraig(Aig_Obj_t * pObj)51 static inline Aig_Obj_t * Bmc_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id]; }
Bmc_ObjSetFraig(Aig_Obj_t * pObj,Aig_Obj_t * pNode)52 static inline void Bmc_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id] = pNode; }
53
Bmc_ObjChild0Frames(Aig_Obj_t * pObj,int i)54 static inline Aig_Obj_t * Bmc_ObjChild0Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
Bmc_ObjChild1Frames(Aig_Obj_t * pObj,int i)55 static inline Aig_Obj_t * Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
56
57 ////////////////////////////////////////////////////////////////////////
58 /// FUNCTION DEFINITIONS ///
59 ////////////////////////////////////////////////////////////////////////
60
61 /**Function*************************************************************
62
63 Synopsis [Returns 1 if the nodes are equivalent.]
64
65 Description []
66
67 SideEffects []
68
69 SeeAlso []
70
71 ***********************************************************************/
Fra_BmcNodesAreEqual(Aig_Obj_t * pObj0,Aig_Obj_t * pObj1)72 int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
73 {
74 Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
75 Aig_Obj_t * pObjFrames0, * pObjFrames1;
76 Aig_Obj_t * pObjFraig0, * pObjFraig1;
77 int i;
78 for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ )
79 {
80 pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) );
81 pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) );
82 if ( pObjFrames0 == pObjFrames1 )
83 continue;
84 pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) );
85 pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) );
86 if ( pObjFraig0 != pObjFraig1 )
87 return 0;
88 }
89 return 1;
90 }
91
92 /**Function*************************************************************
93
94 Synopsis [Returns 1 if the node is costant.]
95
96 Description []
97
98 SideEffects []
99
100 SeeAlso []
101
102 ***********************************************************************/
Fra_BmcNodeIsConst(Aig_Obj_t * pObj)103 int Fra_BmcNodeIsConst( Aig_Obj_t * pObj )
104 {
105 Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
106 return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
107 }
108
109 /**Function*************************************************************
110
111 Synopsis [Refines implications using BMC.]
112
113 Description [The input is the combinational FRAIG manager,
114 which is used to FRAIG the timeframes. ]
115
116 SideEffects []
117
118 SeeAlso []
119
120 ***********************************************************************/
Fra_BmcFilterImplications(Fra_Man_t * p,Fra_Bmc_t * pBmc)121 void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
122 {
123 Aig_Obj_t * pLeft, * pRight;
124 Aig_Obj_t * pLeftT, * pRightT;
125 Aig_Obj_t * pLeftF, * pRightF;
126 int i, f, Imp, Left, Right;
127 int fComplL, fComplR;
128 assert( p->nFramesAll == 1 );
129 assert( p->pManAig == pBmc->pAigFrames );
130 Vec_IntForEachEntry( pBmc->vImps, Imp, i )
131 {
132 if ( Imp == 0 )
133 continue;
134 Left = Fra_ImpLeft(Imp);
135 Right = Fra_ImpRight(Imp);
136 // get the corresponding nodes
137 pLeft = Aig_ManObj( pBmc->pAig, Left );
138 pRight = Aig_ManObj( pBmc->pAig, Right );
139 // iterate through the timeframes
140 for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
141 {
142 // get timeframe nodes
143 pLeftT = Bmc_ObjFrames( pLeft, f );
144 pRightT = Bmc_ObjFrames( pRight, f );
145 // get the corresponding FRAIG nodes
146 pLeftF = Fra_ObjFraig( Aig_Regular(pLeftT), 0 );
147 pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 );
148 // get the complemented attributes
149 fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT);
150 fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT);
151 // check equality
152 if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
153 {
154 if ( fComplL == fComplR ) // x => x - always true
155 continue;
156 assert( fComplL != fComplR );
157 // consider 4 possibilities:
158 // NOT(1) => 1 or 0 => 1 - always true
159 // 1 => NOT(1) or 1 => 0 - never true
160 // NOT(x) => x or x - not always true
161 // x => NOT(x) or NOT(x) - not always true
162 if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
163 continue;
164 // disproved implication
165 Vec_IntWriteEntry( pBmc->vImps, i, 0 );
166 break;
167 }
168 // check the implication
169 if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
170 {
171 Vec_IntWriteEntry( pBmc->vImps, i, 0 );
172 break;
173 }
174 }
175 }
176 Fra_ImpCompactArray( pBmc->vImps );
177 }
178
179
180 /**Function*************************************************************
181
182 Synopsis [Starts the BMC manager.]
183
184 Description []
185
186 SideEffects []
187
188 SeeAlso []
189
190 ***********************************************************************/
Fra_BmcStart(Aig_Man_t * pAig,int nPref,int nDepth)191 Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
192 {
193 Fra_Bmc_t * p;
194 p = ABC_ALLOC( Fra_Bmc_t, 1 );
195 memset( p, 0, sizeof(Fra_Bmc_t) );
196 p->pAig = pAig;
197 p->nPref = nPref;
198 p->nDepth = nDepth;
199 p->nFramesAll = nPref + nDepth;
200 p->pObjToFrames = ABC_ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
201 memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
202 return p;
203 }
204
205 /**Function*************************************************************
206
207 Synopsis [Stops the BMC manager.]
208
209 Description []
210
211 SideEffects []
212
213 SeeAlso []
214
215 ***********************************************************************/
Fra_BmcStop(Fra_Bmc_t * p)216 void Fra_BmcStop( Fra_Bmc_t * p )
217 {
218 Aig_ManStop( p->pAigFrames );
219 if ( p->pAigFraig )
220 Aig_ManStop( p->pAigFraig );
221 ABC_FREE( p->pObjToFrames );
222 ABC_FREE( p->pObjToFraig );
223 ABC_FREE( p );
224 }
225
226 /**Function*************************************************************
227
228 Synopsis [Constructs initialized timeframes of the AIG.]
229
230 Description []
231
232 SideEffects []
233
234 SeeAlso []
235
236 ***********************************************************************/
Fra_BmcFrames(Fra_Bmc_t * p,int fKeepPos)237 Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
238 {
239 Aig_Man_t * pAigFrames;
240 Aig_Obj_t * pObj, * pObjNew;
241 Aig_Obj_t ** pLatches;
242 int i, k, f;
243
244 // start the fraig package
245 pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
246 pAigFrames->pName = Abc_UtilStrsav( p->pAig->pName );
247 pAigFrames->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
248 // create PI nodes for the frames
249 for ( f = 0; f < p->nFramesAll; f++ )
250 Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
251 for ( f = 0; f < p->nFramesAll; f++ )
252 Aig_ManForEachPiSeq( p->pAig, pObj, i )
253 Bmc_ObjSetFrames( pObj, f, Aig_ObjCreateCi(pAigFrames) );
254 // set initial state for the latches
255 Aig_ManForEachLoSeq( p->pAig, pObj, i )
256 Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );
257
258 // add timeframes
259 pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
260 for ( f = 0; f < p->nFramesAll; f++ )
261 {
262 // add internal nodes of this frame
263 Aig_ManForEachNode( p->pAig, pObj, i )
264 {
265 pObjNew = Aig_And( pAigFrames, Bmc_ObjChild0Frames(pObj,f), Bmc_ObjChild1Frames(pObj,f) );
266 Bmc_ObjSetFrames( pObj, f, pObjNew );
267 }
268 if ( f == p->nFramesAll - 1 )
269 break;
270 // save the latch input values
271 k = 0;
272 Aig_ManForEachLiSeq( p->pAig, pObj, i )
273 pLatches[k++] = Bmc_ObjChild0Frames(pObj,f);
274 assert( k == Aig_ManRegNum(p->pAig) );
275 // insert them to the latch output values
276 k = 0;
277 Aig_ManForEachLoSeq( p->pAig, pObj, i )
278 Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] );
279 assert( k == Aig_ManRegNum(p->pAig) );
280 }
281 ABC_FREE( pLatches );
282 if ( fKeepPos )
283 {
284 for ( f = 0; f < p->nFramesAll; f++ )
285 Aig_ManForEachPoSeq( p->pAig, pObj, i )
286 Aig_ObjCreateCo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) );
287 Aig_ManCleanup( pAigFrames );
288 }
289 else
290 {
291 // add POs to all the dangling nodes
292 Aig_ManForEachObj( pAigFrames, pObjNew, i )
293 if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
294 Aig_ObjCreateCo( pAigFrames, pObjNew );
295 }
296 // return the new manager
297 return pAigFrames;
298 }
299
300 /**Function*************************************************************
301
302 Synopsis [Performs BMC for the given AIG.]
303
304 Description []
305
306 SideEffects []
307
308 SeeAlso []
309
310 ***********************************************************************/
Fra_BmcPerform(Fra_Man_t * p,int nPref,int nDepth)311 void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
312 {
313 Aig_Obj_t * pObj;
314 int i, nImpsOld = 0;
315 abctime clk = Abc_Clock();
316 assert( p->pBmc == NULL );
317 // derive and fraig the frames
318 p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
319 p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 );
320 // if implications are present, configure the AIG manager to check them
321 if ( p->pCla->vImps )
322 {
323 p->pBmc->pAigFrames->pImpFunc = (void (*) (void*, void*))Fra_BmcFilterImplications;
324 p->pBmc->pAigFrames->pImpData = p->pBmc;
325 p->pBmc->vImps = p->pCla->vImps;
326 nImpsOld = Vec_IntSize(p->pCla->vImps);
327 }
328 p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 );
329 p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
330 p->pBmc->pAigFrames->pObjCopies = NULL;
331 // annotate frames nodes with pointers to the manager
332 Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
333 pObj->pData = p;
334 // report the results
335 if ( p->pPars->fVerbose )
336 {
337 printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d. ",
338 Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll,
339 Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
340 ABC_PRT( "Time", Abc_Clock() - clk );
341 printf( "Before BMC: " );
342 // Fra_ClassesPrint( p->pCla, 0 );
343 printf( "Const = %5d. Class = %5d. Lit = %5d. ",
344 Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
345 if ( p->pCla->vImps )
346 printf( "Imp = %5d. ", nImpsOld );
347 printf( "\n" );
348 }
349 // refine the classes
350 p->pCla->pFuncNodeIsConst = Fra_BmcNodeIsConst;
351 p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
352 Fra_ClassesRefine( p->pCla );
353 Fra_ClassesRefine1( p->pCla, 1, NULL );
354 p->pCla->pFuncNodeIsConst = Fra_SmlNodeIsConst;
355 p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
356 // report the results
357 if ( p->pPars->fVerbose )
358 {
359 printf( "After BMC: " );
360 // Fra_ClassesPrint( p->pCla, 0 );
361 printf( "Const = %5d. Class = %5d. Lit = %5d. ",
362 Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
363 if ( p->pCla->vImps )
364 printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
365 printf( "\n" );
366 }
367 // free the BMC manager
368 Fra_BmcStop( p->pBmc );
369 p->pBmc = NULL;
370 }
371
372 /**Function*************************************************************
373
374 Synopsis [Performs BMC for the given AIG.]
375
376 Description []
377
378 SideEffects []
379
380 SeeAlso []
381
382 ***********************************************************************/
Fra_BmcPerformSimple(Aig_Man_t * pAig,int nFrames,int nBTLimit,int fRewrite,int fVerbose)383 void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
384 {
385 extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig );
386 Fra_Man_t * pTemp;
387 Fra_Bmc_t * pBmc;
388 Aig_Man_t * pAigTemp;
389 abctime clk;
390 int iOutput;
391 // derive and fraig the frames
392 clk = Abc_Clock();
393 pBmc = Fra_BmcStart( pAig, 0, nFrames );
394 pTemp = Fra_LcrAigPrepare( pAig );
395 pTemp->pBmc = pBmc;
396 pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 );
397 if ( fVerbose )
398 {
399 printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
400 Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
401 Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
402 printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",
403 nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames),
404 Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
405 ABC_PRT( "Time", Abc_Clock() - clk );
406 }
407 if ( fRewrite )
408 {
409 clk = Abc_Clock();
410 pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
411 Aig_ManStop( pAigTemp );
412 if ( fVerbose )
413 {
414 printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
415 Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
416 ABC_PRT( "Time", Abc_Clock() - clk );
417 }
418 }
419 clk = Abc_Clock();
420 iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
421 if ( iOutput >= 0 )
422 pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
423 else
424 {
425 pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
426 iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
427 if ( pBmc->pAigFraig->pData )
428 {
429 pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, (int *)pBmc->pAigFraig->pData );
430 ABC_FREE( pBmc->pAigFraig->pData );
431 }
432 else if ( iOutput >= 0 )
433 pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
434 }
435 if ( fVerbose )
436 {
437 printf( "Fraiged init frames: Node = %6d. Lev = %5d. ",
438 pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1,
439 pBmc->pAigFraig? Aig_ManLevelNum(pBmc->pAigFraig) : -1 );
440 ABC_PRT( "Time", Abc_Clock() - clk );
441 }
442 Fra_BmcStop( pBmc );
443 ABC_FREE( pTemp );
444 }
445
446
447 ////////////////////////////////////////////////////////////////////////
448 /// END OF FILE ///
449 ////////////////////////////////////////////////////////////////////////
450
451
452 ABC_NAMESPACE_IMPL_END
453
454