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