ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
llb2Image.c
Go to the documentation of this file.
1
20
21#include "llbInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30extern Vec_Ptr_t * Llb_ManCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
31extern Vec_Ptr_t * Llb_ManCutRange( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper );
32
36
48Vec_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
122void 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
183DdManager * 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
259DdNode * 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
288void 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
340void 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
364DdNode * 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();
402if ( fVerbose )
403printf( " %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 );
409if ( fVerbose )
410printf( "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
425if ( fVerbose )
426printf( "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
435if ( fVerbose )
436printf( "Supp =%3d. ", Cudd_SupportSize(dd, bImage) );
437if ( fVerbose )
438Abc_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
479
480
481ABC_NAMESPACE_IMPL_END
482
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition aig.h:408
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Extra_bddChangePolarity
DdNode * Extra_bddChangePolarity(DdManager *dd, DdNode *bFunc, DdNode *bVars)
Definition extraBddMisc.c:1029
Llb_DriverPhaseCube
DdNode * Llb_DriverPhaseCube(Aig_Man_t *pAig, Vec_Int_t *vDriRefs, DdManager *dd)
Definition llb2Driver.c:128
Llb_ImgPartition
DdManager * Llb_ImgPartition(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, abctime TimeTarget)
Definition llb2Image.c:183
Llb_ImgQuantifyFirst
void Llb_ImgQuantifyFirst(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, Vec_Ptr_t *vQuant0, int fVerbose)
Definition llb2Image.c:288
Llb_ImgQuantifyReset
void Llb_ImgQuantifyReset(Vec_Ptr_t *vDdMans)
Definition llb2Image.c:340
Llb_ImgSchedule
void Llb_ImgSchedule(Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
Definition llb2Image.c:122
Llb_ImgComputeCube
DdNode * Llb_ImgComputeCube(Aig_Man_t *pAig, Vec_Int_t *vNodeIds, DdManager *dd)
Definition llb2Image.c:259
Llb_ManCutRange
Vec_Ptr_t * Llb_ManCutRange(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
Definition llb2Flow.c:436
Llb_ImgSupports
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)
FUNCTION DEFINITIONS ///.
Definition llb2Image.c:48
Llb_ManCutNodes
ABC_NAMESPACE_IMPL_START Vec_Ptr_t * Llb_ManCutNodes(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper)
DECLARATIONS ///.
Definition llb2Flow.c:374
Llb_ImgComputeImage
DdNode * 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)
Definition llb2Image.c:364
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55