ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
llb4Cluster.c
Go to the documentation of this file.
1
20
21#include "llbInt.h"
22
24
25
29
33
45void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
46{
47 Aig_Obj_t * pFanin0, * pFanin1;
48 if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
49 return;
50 Aig_ObjSetTravIdCurrent( pAig, pObj );
51 assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
52 if ( Aig_ObjIsCi(pObj) )
53 {
54 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
55 return;
56 }
57 // try fanins with higher level first
58 pFanin0 = Aig_ObjFanin0(pObj);
59 pFanin1 = Aig_ObjFanin1(pObj);
60// if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
61 if ( pFanin0->Level > pFanin1->Level )
62 {
63 Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
64 Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
65 }
66 else
67 {
68 Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
69 Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
70 }
71 if ( pObj->fMarkA )
72 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
73}
74
86Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig, int * pCounter )
87{
88 Vec_Int_t * vNodes = NULL;
89 Vec_Int_t * vOrder;
90 Aig_Obj_t * pObj;
91 int i, Counter = 0;
92 // mark nodes to exclude: AND with low level and CO drivers
93 Aig_ManCleanMarkA( pAig );
94 Aig_ManForEachNode( pAig, pObj, i )
95 if ( Aig_ObjLevel(pObj) > 3 )
96 pObj->fMarkA = 1;
97 Aig_ManForEachCo( pAig, pObj, i )
98 Aig_ObjFanin0(pObj)->fMarkA = 0;
99
100 // collect nodes in the order
101 vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
103 Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
104// Aig_ManForEachCo( pAig, pObj, i )
105 Saig_ManForEachLi( pAig, pObj, i )
106 {
107 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
108 Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
109 }
110 Aig_ManForEachCi( pAig, pObj, i )
111 if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
112 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
113 Aig_ManCleanMarkA( pAig );
114 Vec_IntFreeP( &vNodes );
115// assert( Counter == Aig_ManObjNum(pAig) - 1 );
116
117/*
118 Saig_ManForEachPi( pAig, pObj, i )
119 printf( "pi%d ", Llb_ObjBddVar(vOrder, pObj) );
120 printf( "\n" );
121 Saig_ManForEachLo( pAig, pObj, i )
122 printf( "lo%d ", Llb_ObjBddVar(vOrder, pObj) );
123 printf( "\n" );
124 Saig_ManForEachPo( pAig, pObj, i )
125 printf( "po%d ", Llb_ObjBddVar(vOrder, pObj) );
126 printf( "\n" );
127 Saig_ManForEachLi( pAig, pObj, i )
128 printf( "li%d ", Llb_ObjBddVar(vOrder, pObj) );
129 printf( "\n" );
130 Aig_ManForEachNode( pAig, pObj, i )
131 printf( "n%d ", Llb_ObjBddVar(vOrder, pObj) );
132 printf( "\n" );
133*/
134 if ( pCounter )
135 *pCounter = Counter;
136 return vOrder;
137}
138
150DdNode * Llb_Nonlin4FindPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Ptr_t * vRoots )
151{
152 DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
153 if ( Aig_ObjIsConst1(pObj) )
154 return Cudd_ReadOne(dd);
155 if ( Aig_ObjIsCi(pObj) )
156 return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
157 if ( pObj->pData )
158 return (DdNode *)pObj->pData;
159 if ( Aig_ObjIsCo(pObj) )
160 {
161 bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
162 bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart );
163 Vec_PtrPush( vRoots, bPart );
164 return NULL;
165 }
166 bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
167 bBdd1 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) );
168 bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
169 if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
170 {
171 vVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
172 bPart = Cudd_bddXnor( dd, vVar, bBdd ); Cudd_Ref( bPart );
173 Vec_PtrPush( vRoots, bPart );
174 Cudd_RecursiveDeref( dd, bBdd );
175 bBdd = vVar; Cudd_Ref( vVar );
176 }
177 pObj->pData = bBdd;
178 return bBdd;
179}
180
192Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fOutputs )
193{
194 Vec_Ptr_t * vRoots;
195 Aig_Obj_t * pObj;
196 int i;
197 Aig_ManCleanData( pAig );
198 vRoots = Vec_PtrAlloc( 100 );
199 if ( fOutputs )
200 {
201 Saig_ManForEachPo( pAig, pObj, i )
202 Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots );
203 }
204 else
205 {
206 Saig_ManForEachLi( pAig, pObj, i )
207 Llb_Nonlin4FindPartitions_rec( dd, pObj, vOrder, vRoots );
208 }
209 Aig_ManForEachNode( pAig, pObj, i )
210 if ( pObj->pData )
211 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
212 return vRoots;
213}
214
226Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
227{
228 Vec_Int_t * vVars2Q;
229 Aig_Obj_t * pObj;
230 int i;
231 vVars2Q = Vec_IntAlloc( 0 );
232 Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
233 Saig_ManForEachLo( pAig, pObj, i )
234 Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
235// Aig_ManForEachCo( pAig, pObj, i )
236 Saig_ManForEachLi( pAig, pObj, i )
237 Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
238 return vVars2Q;
239}
240
252int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, DdNode * bFunc, int fCo, int fFlop )
253{
254 DdNode * bSupp;
255 Aig_Obj_t * pObj;
256 int i, Counter = 0;
257 bSupp = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupp );
258 if ( !fCo && !fFlop )
259 {
260 Saig_ManForEachPi( pAig, pObj, i )
261 if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
262 Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
263 }
264 else if ( fCo && !fFlop )
265 {
266 Saig_ManForEachPo( pAig, pObj, i )
267 if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
268 Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
269 }
270 else if ( !fCo && fFlop )
271 {
272 Saig_ManForEachLo( pAig, pObj, i )
273 if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
274 Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
275 }
276 else if ( fCo && fFlop )
277 {
278 Saig_ManForEachLi( pAig, pObj, i )
279 if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
280 Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_ObjBddVar(vOrder, pObj)) );
281 }
282 Cudd_RecursiveDeref( dd, bSupp );
283 return Counter;
284}
285
297void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
298{
299 DdNode * bTemp;
300 int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd;
301 Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
302 {
303//Extra_bddPrintSupport(dd, bTemp); printf("\n" );
304 nSuppAll = Cudd_SupportSize(dd,bTemp);
305 nSuppPi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0);
306 nSuppPo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0);
307 nSuppLi = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 1);
308 nSuppLo = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1);
309 nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo);
310
311 if ( Cudd_DagSize(bTemp) <= 10 )
312 continue;
313
314 printf( "%4d : bdd =%6d supp =%3d ", i, Cudd_DagSize(bTemp), nSuppAll );
315 printf( "pi =%3d ", nSuppPi );
316 printf( "po =%3d ", nSuppPo );
317 printf( "lo =%3d ", nSuppLo );
318 printf( "li =%3d ", nSuppLi );
319 printf( "and =%3d", nSuppAnd );
320 printf( "\n" );
321 }
322}
323
335void Llb_Nonlin4PrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
336{
337 Aig_Obj_t * pObj;
338 int i, * pSupp;
339 int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0;
340
341 pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) );
342 Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp );
343
344 Aig_ManForEachObj( pAig, pObj, i )
345 {
346 if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
347 continue;
348 // remove variables that do not participate
349 if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 )
350 {
351 if ( Aig_ObjIsNode(pObj) )
352 Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 );
353 continue;
354 }
355 nSuppAll++;
356 if ( Saig_ObjIsPi(pAig, pObj) )
357 nSuppPi++;
358 else if ( Saig_ObjIsLo(pAig, pObj) )
359 nSuppLo++;
360 else if ( Saig_ObjIsPo(pAig, pObj) )
361 nSuppPo++;
362 else if ( Saig_ObjIsLi(pAig, pObj) )
363 nSuppLi++;
364 else
365 nSuppAnd++;
366 }
367 ABC_FREE( pSupp );
368
369 printf( "Groups =%3d ", Vec_PtrSize(vGroups) );
370 printf( "Variables: all =%4d ", nSuppAll );
371 printf( "pi =%4d ", nSuppPi );
372 printf( "po =%4d ", nSuppPo );
373 printf( "lo =%4d ", nSuppLo );
374 printf( "li =%4d ", nSuppLi );
375 printf( "and =%4d", nSuppAnd );
376 printf( "\n" );
377}
378
390void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose )
391{
392 DdManager * dd;
393 Vec_Int_t * vOrder, * vVars2Q;
394 Vec_Ptr_t * vParts, * vGroups;
395 DdNode * bTemp;
396 int i, nVarNum;
397
398 // create the BDD manager
399 vOrder = Llb_Nonlin4FindOrder( pAig, &nVarNum );
400 dd = Cudd_Init( nVarNum, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
401// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
402
403 vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
404 vParts = Llb_Nonlin4FindPartitions( dd, pAig, vOrder, 0 );
405
406 vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddMax );
407 Vec_IntFree( vVars2Q );
408
409 Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
410 Cudd_RecursiveDeref( dd, bTemp );
411 Vec_PtrFree( vParts );
412
413
414// if ( fVerbose )
415 Llb_Nonlin4PrintSuppProfile( dd, pAig, vOrder, vGroups );
416 if ( fVerbose )
417 printf( "Before reordering\n" );
418 if ( fVerbose )
419 Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
420
421// Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
422// printf( "After reordering\n" );
423// Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
424
425 if ( pvOrder )
426 *pvOrder = vOrder;
427 else
428 Vec_IntFree( vOrder );
429
430 if ( pvGroups )
431 *pvGroups = vGroups;
432 else
433 {
434 Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
435 Cudd_RecursiveDeref( dd, bTemp );
436 Vec_PtrFree( vGroups );
437 }
438
439 if ( pdd )
440 *pdd = dd;
441 else
442 Extra_StopManager( dd );
443// Cudd_Quit( dd );
444}
445
449
450
452
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
void Aig_ManCleanMarkA(Aig_Man_t *p)
Definition aigUtil.c:148
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
void Extra_StopManager(DdManager *dd)
int * Extra_VectorSupportArray(DdManager *dd, DdNode **F, int n, int *support)
int Llb_Nonlin4CountTerms(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, DdNode *bFunc, int fCo, int fFlop)
DdNode * Llb_Nonlin4FindPartitions_rec(DdManager *dd, Aig_Obj_t *pObj, Vec_Int_t *vOrder, Vec_Ptr_t *vRoots)
void Llb_Nonlin4PrintGroups(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, Vec_Ptr_t *vGroups)
Vec_Int_t * Llb_Nonlin4FindOrder(Aig_Man_t *pAig, int *pCounter)
Definition llb4Cluster.c:86
ABC_NAMESPACE_IMPL_START void Llb_Nonlin4FindOrder_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vOrder, int *pCounter)
DECLARATIONS ///.
Definition llb4Cluster.c:45
Vec_Ptr_t * Llb_Nonlin4FindPartitions(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, int fOutputs)
void Llb_Nonlin4Cluster(Aig_Man_t *pAig, DdManager **pdd, Vec_Int_t **pvOrder, Vec_Ptr_t **pvGroups, int nBddMax, int fVerbose)
Vec_Int_t * Llb_Nonlin4FindVars2Q(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder)
void Llb_Nonlin4PrintSuppProfile(DdManager *dd, Aig_Man_t *pAig, Vec_Int_t *vOrder, Vec_Ptr_t *vGroups)
Vec_Ptr_t * Llb_Nonlin4Group(DdManager *dd, Vec_Ptr_t *vParts, Vec_Int_t *vVars2Q, int nSizeMax)
Definition llb4Image.c:806
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
unsigned int fMarkA
Definition aig.h:79
void * pData
Definition aig.h:87
unsigned Level
Definition aig.h:82
#define assert(ex)
Definition util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55