1 /**CFile****************************************************************
2
3 FileName [llb2Image.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [BDD based reachability.]
8
9 Synopsis [Computes image using partitioned structure.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: llb2Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "llbInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 extern Vec_Ptr_t * Llb_ManCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
31 extern Vec_Ptr_t * Llb_ManCutRange( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Computes supports of the partitions.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Llb_ImgSupports(Aig_Man_t * p,Vec_Ptr_t * vDdMans,Vec_Int_t * vStart,Vec_Int_t * vStop,int fAddPis,int fVerbose)48 Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose )
49 {
50 Vec_Ptr_t * vSupps;
51 Vec_Int_t * vOne;
52 Aig_Obj_t * pObj;
53 DdManager * dd;
54 DdNode * bSupp, * bTemp;
55 int i, Entry, nSize;
56 nSize = Cudd_ReadSize( (DdManager *)Vec_PtrEntry( vDdMans, 0 ) );
57 vSupps = Vec_PtrAlloc( 100 );
58 // create initial
59 vOne = Vec_IntStart( nSize );
60 Vec_IntForEachEntry( vStart, Entry, i )
61 Vec_IntWriteEntry( vOne, Entry, 1 );
62 Vec_PtrPush( vSupps, vOne );
63 // create intermediate
64 Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
65 {
66 vOne = Vec_IntStart( nSize );
67 bSupp = Cudd_Support( dd, dd->bFunc ); Cudd_Ref( bSupp );
68 for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
69 Vec_IntWriteEntry( vOne, bTemp->index, 1 );
70 Cudd_RecursiveDeref( dd, bSupp );
71 Vec_PtrPush( vSupps, vOne );
72 }
73 // create final
74 vOne = Vec_IntStart( nSize );
75 Vec_IntForEachEntry( vStop, Entry, i )
76 Vec_IntWriteEntry( vOne, Entry, 1 );
77 if ( fAddPis )
78 Saig_ManForEachPi( p, pObj, i )
79 Vec_IntWriteEntry( vOne, Aig_ObjId(pObj), 1 );
80 Vec_PtrPush( vSupps, vOne );
81
82 // print supports
83 assert( nSize == Aig_ManObjNumMax(p) );
84 if ( !fVerbose )
85 return vSupps;
86 Aig_ManForEachObj( p, pObj, i )
87 {
88 int k, Counter = 0;
89 Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
90 Counter += Vec_IntEntry(vOne, i);
91 if ( Counter == 0 )
92 continue;
93 printf( "Obj = %4d : ", i );
94 if ( Saig_ObjIsPi(p,pObj) )
95 printf( "pi " );
96 else if ( Saig_ObjIsLo(p,pObj) )
97 printf( "lo " );
98 else if ( Saig_ObjIsLi(p,pObj) )
99 printf( "li " );
100 else if ( Aig_ObjIsNode(pObj) )
101 printf( "and " );
102 Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
103 printf( "%d", Vec_IntEntry(vOne, i) );
104 printf( "\n" );
105 }
106 return vSupps;
107 }
108
109 /**Function*************************************************************
110
111 Synopsis [Computes quantification schedule.]
112
113 Description [Input array contains supports: 0=starting, ... intermediate...
114 N-1=final. Output arrays contain immediately quantifiable vars (vQuant0)
115 and vars that should be quantified after conjunction (vQuant1).]
116
117 SideEffects []
118
119 SeeAlso []
120
121 ***********************************************************************/
Llb_ImgSchedule(Vec_Ptr_t * vSupps,Vec_Ptr_t ** pvQuant0,Vec_Ptr_t ** pvQuant1,int fVerbose)122 void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose )
123 {
124 Vec_Int_t * vOne;
125 int nVarsAll, Counter, iSupp = -1, Entry, i, k;
126 // start quantification arrays
127 *pvQuant0 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
128 *pvQuant1 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
129 Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
130 {
131 Vec_PtrPush( *pvQuant0, Vec_IntAlloc(16) );
132 Vec_PtrPush( *pvQuant1, Vec_IntAlloc(16) );
133 }
134 // count how many times each var appears
135 nVarsAll = Vec_IntSize( (Vec_Int_t *)Vec_PtrEntry(vSupps, 0) );
136 for ( i = 0; i < nVarsAll; i++ )
137 {
138 Counter = 0;
139 Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vOne, k )
140 if ( Vec_IntEntry(vOne, i) )
141 {
142 iSupp = k;
143 Counter++;
144 }
145 if ( Counter == 0 )
146 continue;
147 if ( Counter == 1 )
148 Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, iSupp), i );
149 else // if ( Counter > 1 )
150 Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, iSupp), i );
151 }
152
153 if ( fVerbose )
154 for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
155 {
156 printf( "%2d : Quant0 = ", i );
157 Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant0, i), Entry, k )
158 printf( "%d ", Entry );
159 printf( "\n" );
160 }
161
162 if ( fVerbose )
163 for ( i = 0; i < Vec_PtrSize(vSupps); i++ )
164 {
165 printf( "%2d : Quant1 = ", i );
166 Vec_IntForEachEntry( (Vec_Int_t *)Vec_PtrEntry(*pvQuant1, i), Entry, k )
167 printf( "%d ", Entry );
168 printf( "\n" );
169 }
170 }
171
172 /**Function*************************************************************
173
174 Synopsis [Computes one partition in a separate BDD manager.]
175
176 Description []
177
178 SideEffects []
179
180 SeeAlso []
181
182 ***********************************************************************/
Llb_ImgPartition(Aig_Man_t * p,Vec_Ptr_t * vLower,Vec_Ptr_t * vUpper,abctime TimeTarget)183 DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, abctime TimeTarget )
184 {
185 Vec_Ptr_t * vNodes, * vRange;
186 Aig_Obj_t * pObj;
187 DdManager * dd;
188 DdNode * bBdd0, * bBdd1, * bProd, * bRes, * bTemp;
189 int i;
190
191 dd = Cudd_Init( Aig_ManObjNumMax(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
192 Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
193 dd->TimeStop = TimeTarget;
194
195 Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
196 pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
197
198 vNodes = Llb_ManCutNodes( p, vLower, vUpper );
199 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
200 {
201 bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
202 bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
203 // pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
204 // pObj->pData = Extra_bddAndTime( dd, bBdd0, bBdd1, TimeTarget );
205 pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );
206 if ( pObj->pData == NULL )
207 {
208 Cudd_Quit( dd );
209 Vec_PtrFree( vNodes );
210 return NULL;
211 }
212 Cudd_Ref( (DdNode *)pObj->pData );
213 }
214
215 vRange = Llb_ManCutRange( p, vLower, vUpper );
216 bRes = Cudd_ReadOne(dd); Cudd_Ref( bRes );
217 Vec_PtrForEachEntry( Aig_Obj_t *, vRange, pObj, i )
218 {
219 assert( Aig_ObjIsNode(pObj) );
220 bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData ); Cudd_Ref( bProd );
221 // bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
222 // bRes = Extra_bddAndTime( dd, bTemp = bRes, bProd, TimeTarget );
223 bRes = Cudd_bddAnd( dd, bTemp = bRes, bProd );
224 if ( bRes == NULL )
225 {
226 Cudd_Quit( dd );
227 Vec_PtrFree( vRange );
228 Vec_PtrFree( vNodes );
229 return NULL;
230 }
231 Cudd_Ref( bRes );
232 Cudd_RecursiveDeref( dd, bTemp );
233 Cudd_RecursiveDeref( dd, bProd );
234 }
235 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
236 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
237
238 Vec_PtrFree( vRange );
239 Vec_PtrFree( vNodes );
240 Cudd_AutodynDisable( dd );
241 // Cudd_RecursiveDeref( dd, bRes );
242 // Extra_StopManager( dd );
243 dd->bFunc = bRes;
244 dd->TimeStop = 0;
245 return dd;
246 }
247
248 /**Function*************************************************************
249
250 Synopsis [Derives positive cube composed of nodes IDs.]
251
252 Description []
253
254 SideEffects []
255
256 SeeAlso []
257
258 ***********************************************************************/
Llb_ImgComputeCube(Aig_Man_t * pAig,Vec_Int_t * vNodeIds,DdManager * dd)259 DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager * dd )
260 {
261 DdNode * bProd, * bTemp;
262 Aig_Obj_t * pObj;
263 int i;
264 abctime TimeStop;
265 TimeStop = dd->TimeStop; dd->TimeStop = 0;
266 bProd = Cudd_ReadOne(dd); Cudd_Ref( bProd );
267 Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i )
268 {
269 bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)) ); Cudd_Ref( bProd );
270 Cudd_RecursiveDeref( dd, bTemp );
271 }
272 Cudd_Deref( bProd );
273 dd->TimeStop = TimeStop;
274 return bProd;
275 }
276
277 /**Function*************************************************************
278
279 Synopsis []
280
281 Description []
282
283 SideEffects []
284
285 SeeAlso []
286
287 ***********************************************************************/
Llb_ImgQuantifyFirst(Aig_Man_t * pAig,Vec_Ptr_t * vDdMans,Vec_Ptr_t * vQuant0,int fVerbose)288 void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose )
289 {
290 DdManager * dd;
291 DdNode * bProd, * bRes, * bTemp;
292 int i;
293 abctime clk = Abc_Clock();
294 Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
295 {
296 // remember unquantified ones
297 assert( dd->bFunc2 == NULL );
298 dd->bFunc2 = dd->bFunc; Cudd_Ref( dd->bFunc2 );
299
300 Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
301
302 bRes = dd->bFunc;
303 if ( fVerbose )
304 Abc_Print( 1, "Part %2d : Init =%5d. ", i, Cudd_DagSize(bRes) );
305 bProd = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, i+1), dd ); Cudd_Ref( bProd );
306 bRes = Cudd_bddExistAbstract( dd, bTemp = bRes, bProd ); Cudd_Ref( bRes );
307 Cudd_RecursiveDeref( dd, bTemp );
308 Cudd_RecursiveDeref( dd, bProd );
309 dd->bFunc = bRes;
310
311 Cudd_AutodynDisable( dd );
312
313 if ( fVerbose )
314 Abc_Print( 1, "Quant =%5d. ", Cudd_DagSize(bRes) );
315 Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
316 if ( fVerbose )
317 Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) );
318 Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
319 if ( fVerbose )
320 Abc_Print( 1, "Reo = %5d. ", Cudd_DagSize(bRes) );
321 if ( fVerbose )
322 Abc_Print( 1, "Supp = %3d. ", Cudd_SupportSize(dd, bRes) );
323 if ( fVerbose )
324 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
325
326 }
327 }
328
329 /**Function*************************************************************
330
331 Synopsis []
332
333 Description []
334
335 SideEffects []
336
337 SeeAlso []
338
339 ***********************************************************************/
Llb_ImgQuantifyReset(Vec_Ptr_t * vDdMans)340 void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans )
341 {
342 DdManager * dd;
343 int i;
344 Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
345 {
346 assert( dd->bFunc2 != NULL );
347 Cudd_RecursiveDeref( dd, dd->bFunc );
348 dd->bFunc = dd->bFunc2;
349 dd->bFunc2 = NULL;
350 }
351 }
352
353 /**Function*************************************************************
354
355 Synopsis [Computes image of the initial set of states.]
356
357 Description []
358
359 SideEffects []
360
361 SeeAlso []
362
363 ***********************************************************************/
Llb_ImgComputeImage(Aig_Man_t * pAig,Vec_Ptr_t * vDdMans,DdManager * dd,DdNode * bInit,Vec_Ptr_t * vQuant0,Vec_Ptr_t * vQuant1,Vec_Int_t * vDriRefs,abctime TimeTarget,int fBackward,int fReorder,int fVerbose)364 DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit,
365 Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs,
366 abctime TimeTarget, int fBackward, int fReorder, int fVerbose )
367 {
368 // int fCheckSupport = 0;
369 DdManager * ddPart;
370 DdNode * bImage, * bGroup, * bCube, * bTemp;
371 int i;
372 abctime clk, clk0 = Abc_Clock();
373
374 bImage = bInit; Cudd_Ref( bImage );
375 if ( fBackward )
376 {
377 // change polarity
378 bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube );
379 bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
380 Cudd_RecursiveDeref( dd, bTemp );
381 Cudd_RecursiveDeref( dd, bCube );
382 }
383 else
384 {
385 // quantify unique vriables
386 bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
387 bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube );
388 if ( bImage == NULL )
389 {
390 Cudd_RecursiveDeref( dd, bTemp );
391 Cudd_RecursiveDeref( dd, bCube );
392 return NULL;
393 }
394 Cudd_Ref( bImage );
395 Cudd_RecursiveDeref( dd, bTemp );
396 Cudd_RecursiveDeref( dd, bCube );
397 }
398 // perform image computation
399 Vec_PtrForEachEntry( DdManager *, vDdMans, ddPart, i )
400 {
401 clk = Abc_Clock();
402 if ( fVerbose )
403 printf( " %2d : ", i );
404 // transfer the BDD from the group manager to the main manager
405 bGroup = Cudd_bddTransfer( ddPart, dd, ddPart->bFunc );
406 if ( bGroup == NULL )
407 return NULL;
408 Cudd_Ref( bGroup );
409 if ( fVerbose )
410 printf( "Pt0 =%6d. Pt1 =%6d. ", Cudd_DagSize(ddPart->bFunc), Cudd_DagSize(bGroup) );
411 // perform partial product
412 bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant1, i+1), dd ); Cudd_Ref( bCube );
413 // bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );
414 // bImage = Extra_bddAndAbstractTime( dd, bTemp = bImage, bGroup, bCube, TimeTarget );
415 bImage = Cudd_bddAndAbstract( dd, bTemp = bImage, bGroup, bCube );
416 if ( bImage == NULL )
417 {
418 Cudd_RecursiveDeref( dd, bTemp );
419 Cudd_RecursiveDeref( dd, bCube );
420 Cudd_RecursiveDeref( dd, bGroup );
421 return NULL;
422 }
423 Cudd_Ref( bImage );
424
425 if ( fVerbose )
426 printf( "Im0 =%6d. Im1 =%6d. ", Cudd_DagSize(bTemp), Cudd_DagSize(bImage) );
427 //printf("\n"); Extra_bddPrintSupport(dd, bImage); printf("\n");
428 Cudd_RecursiveDeref( dd, bTemp );
429 Cudd_RecursiveDeref( dd, bCube );
430 Cudd_RecursiveDeref( dd, bGroup );
431
432 // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
433 // Abc_Print( 1, "Reo =%6d. ", Cudd_DagSize(bImage) );
434
435 if ( fVerbose )
436 printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) );
437 if ( fVerbose )
438 Abc_PrintTime( 1, "T", Abc_Clock() - clk );
439 }
440
441 if ( !fBackward )
442 {
443 // change polarity
444 bCube = Llb_DriverPhaseCube( pAig, vDriRefs, dd ); Cudd_Ref( bCube );
445 bImage = Extra_bddChangePolarity( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
446 Cudd_RecursiveDeref( dd, bTemp );
447 Cudd_RecursiveDeref( dd, bCube );
448 }
449 else
450 {
451 // quantify unique vriables
452 bCube = Llb_ImgComputeCube( pAig, (Vec_Int_t *)Vec_PtrEntry(vQuant0, 0), dd ); Cudd_Ref( bCube );
453 bImage = Cudd_bddExistAbstract( dd, bTemp = bImage, bCube ); Cudd_Ref( bImage );
454 Cudd_RecursiveDeref( dd, bTemp );
455 Cudd_RecursiveDeref( dd, bCube );
456 }
457
458 if ( fReorder )
459 {
460 if ( fVerbose )
461 Abc_Print( 1, " Reordering... Before =%5d. ", Cudd_DagSize(bImage) );
462 Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
463 if ( fVerbose )
464 Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) );
465 // Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
466 // Abc_Print( 1, "After =%5d. ", Cudd_DagSize(bImage) );
467 if ( fVerbose )
468 Abc_PrintTime( 1, "Time", Abc_Clock() - clk0 );
469 // Abc_Print( 1, "\n" );
470 }
471
472 Cudd_Deref( bImage );
473 return bImage;
474 }
475
476 ////////////////////////////////////////////////////////////////////////
477 /// END OF FILE ///
478 ////////////////////////////////////////////////////////////////////////
479
480
481 ABC_NAMESPACE_IMPL_END
482
483