1 /**CFile****************************************************************
2
3 FileName [darBalance.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [DAG-aware AIG rewriting.]
8
9 Synopsis [Algebraic AIG balancing.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - April 28, 2007.]
16
17 Revision [$Id: darBalance.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "darInt.h"
22 #include "misc/tim/tim.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 //#define USE_LUTSIZE_BALANCE
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Uniqifies the node.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Dar_ObjCompareLits(Aig_Obj_t ** pp1,Aig_Obj_t ** pp2)48 int Dar_ObjCompareLits( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
49 {
50 int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
51 if ( Diff < 0 )
52 return -1;
53 if ( Diff > 0 )
54 return 1;
55 return 0;
56 }
Dar_BalanceUniqify(Aig_Obj_t * pObj,Vec_Ptr_t * vNodes,int fExor)57 void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor )
58 {
59 Aig_Obj_t * pTemp, * pTempNext;
60 int i, k;
61 // sort the nodes by their literal
62 Vec_PtrSort( vNodes, (int (*)())Dar_ObjCompareLits );
63 // remove duplicates
64 k = 0;
65 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i )
66 {
67 if ( i + 1 == Vec_PtrSize(vNodes) )
68 {
69 Vec_PtrWriteEntry( vNodes, k++, pTemp );
70 break;
71 }
72 pTempNext = (Aig_Obj_t *)Vec_PtrEntry( vNodes, i+1 );
73 if ( !fExor && pTemp == Aig_Not(pTempNext) ) // pos_lit & neg_lit = 0
74 {
75 Vec_PtrClear( vNodes );
76 return;
77 }
78 if ( pTemp != pTempNext ) // save if different
79 Vec_PtrWriteEntry( vNodes, k++, pTemp );
80 else if ( fExor ) // in case of XOR, remove identical
81 i++;
82 }
83 Vec_PtrShrink( vNodes, k );
84 if ( Vec_PtrSize(vNodes) < 2 )
85 return;
86 // check that there is no duplicates
87 pTemp = (Aig_Obj_t *)Vec_PtrEntry( vNodes, 0 );
88 Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pTempNext, i, 1 )
89 {
90 assert( pTemp != pTempNext );
91 pTemp = pTempNext;
92 }
93 }
94
95 /**Function*************************************************************
96
97 Synopsis [Collects the nodes of the supergate.]
98
99 Description []
100
101 SideEffects []
102
103 SeeAlso []
104
105 ***********************************************************************/
Dar_BalanceCone_rec(Aig_Obj_t * pRoot,Aig_Obj_t * pObj,Vec_Ptr_t * vSuper)106 void Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
107 {
108 if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
109 Vec_PtrPush( vSuper, pObj );
110 else
111 {
112 assert( !Aig_IsComplement(pObj) );
113 assert( Aig_ObjIsNode(pObj) );
114 // go through the branches
115 Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
116 Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
117 }
118 }
Dar_BalanceCone(Aig_Obj_t * pObj,Vec_Vec_t * vStore,int Level)119 Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
120 {
121 Vec_Ptr_t * vNodes;
122 assert( !Aig_IsComplement(pObj) );
123 assert( Aig_ObjIsNode(pObj) );
124 // extend the storage
125 if ( Vec_VecSize( vStore ) <= Level )
126 Vec_VecPush( vStore, Level, 0 );
127 // get the temporary array of nodes
128 vNodes = Vec_VecEntry( vStore, Level );
129 Vec_PtrClear( vNodes );
130 // collect the nodes in the implication supergate
131 Dar_BalanceCone_rec( pObj, pObj, vNodes );
132 // remove duplicates
133 Dar_BalanceUniqify( pObj, vNodes, Aig_ObjIsExor(pObj) );
134 return vNodes;
135 }
136
137
138 /**Function*************************************************************
139
140 Synopsis [Collects the nodes of the supergate.]
141
142 Description []
143
144 SideEffects []
145
146 SeeAlso []
147
148 ***********************************************************************/
149 /*
150 int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
151 {
152 int RetValue1, RetValue2, i;
153 // check if the node is visited
154 if ( Aig_Regular(pObj)->fMarkB )
155 {
156 if ( Aig_ObjIsExor(pRoot) )
157 {
158 assert( !Aig_IsComplement(pObj) );
159 // check if the node occurs in the same polarity
160 Vec_PtrRemove( vSuper, pObj );
161 Aig_Regular(pObj)->fMarkB = 0;
162 //printf( " Duplicated EXOR input!!! " );
163 return 1;
164 }
165 else
166 {
167 // check if the node occurs in the same polarity
168 for ( i = 0; i < vSuper->nSize; i++ )
169 if ( vSuper->pArray[i] == pObj )
170 return 1;
171 // check if the node is present in the opposite polarity
172 for ( i = 0; i < vSuper->nSize; i++ )
173 if ( vSuper->pArray[i] == Aig_Not(pObj) )
174 return -1;
175 }
176 assert( 0 );
177 return 0;
178 }
179 // if the new node is complemented or a PI, another gate begins
180 if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1 || Vec_PtrSize(vSuper) > 10000) )
181 {
182 Vec_PtrPush( vSuper, pObj );
183 Aig_Regular(pObj)->fMarkB = 1;
184 return 0;
185 }
186 assert( !Aig_IsComplement(pObj) );
187 assert( Aig_ObjIsNode(pObj) );
188 // go through the branches
189 RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
190 RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
191 if ( RetValue1 == -1 || RetValue2 == -1 )
192 return -1;
193 // return 1 if at least one branch has a duplicate
194 return RetValue1 || RetValue2;
195 }
196 Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
197 {
198 Vec_Ptr_t * vNodes;
199 int RetValue, i;
200 assert( !Aig_IsComplement(pObj) );
201 // extend the storage
202 if ( Vec_VecSize( vStore ) <= Level )
203 Vec_VecPush( vStore, Level, 0 );
204 // get the temporary array of nodes
205 vNodes = Vec_VecEntry( vStore, Level );
206 Vec_PtrClear( vNodes );
207 // collect the nodes in the implication supergate
208 RetValue = Dar_BalanceCone_rec( pObj, pObj, vNodes );
209 assert( RetValue != 0 || vNodes->nSize > 1 );
210 // unmark the visited nodes
211 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
212 Aig_Regular(pObj)->fMarkB = 0;
213 // if we found the node and its complement in the same implication supergate,
214 // return empty set of nodes (meaning that we should use constant-0 node)
215 if ( RetValue == -1 )
216 vNodes->nSize = 0;
217 return vNodes;
218 }
219 */
220
221 /**Function*************************************************************
222
223 Synopsis [Finds the left bound on the next candidate to be paired.]
224
225 Description [The nodes in the array are in the decreasing order of levels.
226 The last node in the array has the smallest level. By default it would be paired
227 with the next node on the left. However, it may be possible to pair it with some
228 other node on the left, in such a way that the new node is shared. This procedure
229 finds the index of the left-most node, which can be paired with the last node.]
230
231 SideEffects []
232
233 SeeAlso []
234
235 ***********************************************************************/
Dar_BalanceFindLeft(Vec_Ptr_t * vSuper)236 int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper )
237 {
238 Aig_Obj_t * pObjRight, * pObjLeft;
239 int Current;
240 // if two or less nodes, pair with the first
241 if ( Vec_PtrSize(vSuper) < 3 )
242 return 0;
243 // set the pointer to the one before the last
244 Current = Vec_PtrSize(vSuper) - 2;
245 pObjRight = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
246 // go through the nodes to the left of this one
247 for ( Current--; Current >= 0; Current-- )
248 {
249 // get the next node on the left
250 pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
251 // if the level of this node is different, quit the loop
252 if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) )
253 break;
254 }
255 Current++;
256 // get the node, for which the equality holds
257 pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
258 assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_Regular(pObjRight)) );
259 return Current;
260 }
261
262 /**Function*************************************************************
263
264 Synopsis [Moves closer to the end the node that is best for sharing.]
265
266 Description [If there is no node with sharing, randomly chooses one of
267 the legal nodes.]
268
269 SideEffects []
270
271 SeeAlso []
272
273 ***********************************************************************/
Dar_BalancePermute(Aig_Man_t * p,Vec_Ptr_t * vSuper,int LeftBound,int fExor)274 void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
275 {
276 Aig_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
277 int RightBound, i;
278 // get the right bound
279 RightBound = Vec_PtrSize(vSuper) - 2;
280 assert( LeftBound <= RightBound );
281 if ( LeftBound == RightBound )
282 return;
283 // get the two last nodes
284 pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound + 1 );
285 pObj2 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound );
286 if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) )
287 return;
288 // find the first node that can be shared
289 for ( i = RightBound; i >= LeftBound; i-- )
290 {
291 pObj3 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, i );
292 if ( Aig_Regular(pObj3) == p->pConst1 )
293 {
294 Vec_PtrWriteEntry( vSuper, i, pObj2 );
295 Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
296 return;
297 }
298 if ( Aig_Regular(pObj1) == Aig_Regular(pObj3) )
299 {
300 if ( pObj3 == pObj2 )
301 return;
302 Vec_PtrWriteEntry( vSuper, i, pObj2 );
303 Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
304 return;
305 }
306 pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND );
307 if ( Aig_TableLookup( p, pGhost ) )
308 {
309 if ( pObj3 == pObj2 )
310 return;
311 Vec_PtrWriteEntry( vSuper, i, pObj2 );
312 Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
313 return;
314 }
315 }
316 /*
317 // we did not find the node to share, randomize choice
318 {
319 int Choice = Aig_ManRandom(0) % (RightBound - LeftBound + 1);
320 pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
321 if ( pObj3 == pObj2 )
322 return;
323 Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
324 Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
325 }
326 */
327 }
328
329 /**Function*************************************************************
330
331 Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
332
333 Description []
334
335 SideEffects []
336
337 SeeAlso []
338
339 ***********************************************************************/
Aig_NodeCompareLevelsDecrease(Aig_Obj_t ** pp1,Aig_Obj_t ** pp2)340 int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
341 {
342 int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
343 if ( Diff > 0 )
344 return -1;
345 if ( Diff < 0 )
346 return 1;
347 Diff = Aig_ObjId(Aig_Regular(*pp1)) - Aig_ObjId(Aig_Regular(*pp2));
348 if ( Diff > 0 )
349 return -1;
350 if ( Diff < 0 )
351 return 1;
352 return 0;
353 }
354
355 /**Function*************************************************************
356
357 Synopsis [Inserts a new node in the order by levels.]
358
359 Description []
360
361 SideEffects []
362
363 SeeAlso []
364
365 ***********************************************************************/
Dar_BalancePushUniqueOrderByLevel(Vec_Ptr_t * vStore,Aig_Obj_t * pObj,int fExor)366 void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj, int fExor )
367 {
368 Aig_Obj_t * pObj1, * pObj2;
369 int i;
370 if ( Vec_PtrPushUnique(vStore, pObj) )
371 {
372 if ( fExor )
373 Vec_PtrRemove(vStore, pObj);
374 return;
375 }
376 // find the p of the node
377 for ( i = vStore->nSize-1; i > 0; i-- )
378 {
379 pObj1 = (Aig_Obj_t *)vStore->pArray[i ];
380 pObj2 = (Aig_Obj_t *)vStore->pArray[i-1];
381 if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) )
382 break;
383 vStore->pArray[i ] = pObj2;
384 vStore->pArray[i-1] = pObj1;
385 }
386 }
387
388 /**Function*************************************************************
389
390 Synopsis [Builds implication supergate.]
391
392 Description []
393
394 SideEffects []
395
396 SeeAlso []
397
398 ***********************************************************************/
Dar_BalanceBuildSuper(Aig_Man_t * p,Vec_Ptr_t * vSuper,Aig_Type_t Type,int fUpdateLevel)399 Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
400 {
401 Aig_Obj_t * pObj1, * pObj2;
402 int LeftBound;
403 assert( vSuper->nSize > 1 );
404 // sort the new nodes by level in the decreasing order
405 Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
406 // balance the nodes
407 while ( vSuper->nSize > 1 )
408 {
409 // find the left bound on the node to be paired
410 LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
411 // find the node that can be shared (if no such node, randomize choice)
412 Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
413 // pull out the last two nodes
414 pObj1 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
415 pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
416 Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR );
417 }
418 return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
419 }
420
421
422 /**Function*************************************************************
423
424 Synopsis [Returns affective support size.]
425
426 Description []
427
428 SideEffects []
429
430 SeeAlso []
431
432 ***********************************************************************/
Aig_BaseSize(Aig_Man_t * p,Aig_Obj_t * pObj,int nLutSize)433 int Aig_BaseSize( Aig_Man_t * p, Aig_Obj_t * pObj, int nLutSize )
434 {
435 int nBaseSize;
436 pObj = Aig_Regular(pObj);
437 if ( Aig_ObjIsConst1(pObj) )
438 return 0;
439 if ( Aig_ObjLevel(pObj) >= nLutSize )
440 return 1;
441 nBaseSize = Aig_SupportSize( p, pObj );
442 if ( nBaseSize >= nLutSize )
443 return 1;
444 return nBaseSize;
445 }
446
447 /**Function*************************************************************
448
449 Synopsis [Builds implication supergate.]
450
451 Description []
452
453 SideEffects []
454
455 SeeAlso []
456
457 ***********************************************************************/
Dar_BalanceBuildSuperTop(Aig_Man_t * p,Vec_Ptr_t * vSuper,Aig_Type_t Type,int fUpdateLevel,int nLutSize)458 Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel, int nLutSize )
459 {
460 Vec_Ptr_t * vSubset;
461 Aig_Obj_t * pObj;
462 int i, nBaseSizeAll, nBaseSize;
463 assert( vSuper->nSize > 1 );
464 // sort the new nodes by level in the decreasing order
465 Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
466 // add one LUT at a time
467 while ( Vec_PtrSize(vSuper) > 1 )
468 {
469 // isolate the group of nodes with nLutSize inputs
470 nBaseSizeAll = 0;
471 vSubset = Vec_PtrAlloc( nLutSize );
472 Vec_PtrForEachEntryReverse( Aig_Obj_t *, vSuper, pObj, i )
473 {
474 nBaseSize = Aig_BaseSize( p, pObj, nLutSize );
475 if ( nBaseSizeAll + nBaseSize > nLutSize && Vec_PtrSize(vSubset) > 1 )
476 break;
477 nBaseSizeAll += nBaseSize;
478 Vec_PtrPush( vSubset, pObj );
479 }
480 // remove them from vSuper
481 Vec_PtrShrink( vSuper, Vec_PtrSize(vSuper) - Vec_PtrSize(vSubset) );
482 // create the new supergate
483 pObj = Dar_BalanceBuildSuper( p, vSubset, Type, fUpdateLevel );
484 Vec_PtrFree( vSubset );
485 // add the new output
486 Dar_BalancePushUniqueOrderByLevel( vSuper, pObj, Type == AIG_OBJ_EXOR );
487 }
488 return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
489 }
490
491 /**Function*************************************************************
492
493 Synopsis [Returns the new node constructed.]
494
495 Description []
496
497 SideEffects []
498
499 SeeAlso []
500
501 ***********************************************************************/
Dar_Balance_rec(Aig_Man_t * pNew,Aig_Obj_t * pObjOld,Vec_Vec_t * vStore,int Level,int fUpdateLevel)502 Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
503 {
504 Aig_Obj_t * pObjNew;
505 Vec_Ptr_t * vSuper;
506 int i;
507 assert( !Aig_IsComplement(pObjOld) );
508 assert( !Aig_ObjIsBuf(pObjOld) );
509 // return if the result is known
510 if ( pObjOld->pData )
511 return (Aig_Obj_t *)pObjOld->pData;
512 assert( Aig_ObjIsNode(pObjOld) );
513 // get the implication supergate
514 vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
515 // check if supergate contains two nodes in the opposite polarity
516 if ( vSuper->nSize == 0 )
517 return (Aig_Obj_t *)(pObjOld->pData = Aig_ManConst0(pNew));
518 // for each old node, derive the new well-balanced node
519 for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
520 {
521 pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
522 if ( pObjNew == NULL )
523 return NULL;
524 vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
525 }
526 // check for exactly one node
527 if ( vSuper->nSize == 1 )
528 return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
529 // build the supergate
530 #ifdef USE_LUTSIZE_BALANCE
531 pObjNew = Dar_BalanceBuildSuperTop( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel, 6 );
532 #else
533 pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
534 #endif
535 if ( pNew->Time2Quit && !(Aig_Regular(pObjNew)->Id & 255) && Abc_Clock() > pNew->Time2Quit )
536 return NULL;
537 // make sure the balanced node is not assigned
538 // assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
539 assert( pObjOld->pData == NULL );
540 return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
541 }
542
543 /**Function*************************************************************
544
545 Synopsis [Performs algebraic balancing of the AIG.]
546
547 Description []
548
549 SideEffects []
550
551 SeeAlso []
552
553 ***********************************************************************/
Dar_ManBalance(Aig_Man_t * p,int fUpdateLevel)554 Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
555 {
556 Aig_Man_t * pNew;
557 Aig_Obj_t * pObj, * pDriver, * pObjNew;
558 Vec_Vec_t * vStore;
559 int i;
560 assert( Aig_ManVerifyTopoOrder(p) );
561 // create the new manager
562 pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
563 pNew->pName = Abc_UtilStrsav( p->pName );
564 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
565 pNew->nAsserts = p->nAsserts;
566 pNew->nConstrs = p->nConstrs;
567 pNew->nBarBufs = p->nBarBufs;
568 pNew->Time2Quit = p->Time2Quit;
569 if ( p->vFlopNums )
570 pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
571 // map the PI nodes
572 Aig_ManCleanData( p );
573 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
574 vStore = Vec_VecAlloc( 50 );
575 if ( p->pManTime != NULL )
576 {
577 float arrTime;
578 Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime );
579 Aig_ManSetCioIds( p );
580 Aig_ManForEachObj( p, pObj, i )
581 {
582 if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
583 continue;
584 if ( Aig_ObjIsCi(pObj) )
585 {
586 // copy the PI
587 pObjNew = Aig_ObjCreateCi(pNew);
588 pObj->pData = pObjNew;
589 // set the arrival time of the new PI
590 arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
591 pObjNew->Level = (int)arrTime;
592 }
593 else if ( Aig_ObjIsCo(pObj) )
594 {
595 // perform balancing
596 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
597 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
598 if ( pObjNew == NULL )
599 {
600 Vec_VecFree( vStore );
601 Aig_ManStop( pNew );
602 return NULL;
603 }
604 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
605 // save arrival time of the output
606 arrTime = (float)Aig_Regular(pObjNew)->Level;
607 Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
608 // create PO
609 pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
610 }
611 else
612 assert( 0 );
613 }
614 Aig_ManCleanCioIds( p );
615 pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
616 }
617 else
618 {
619 Aig_ManForEachCi( p, pObj, i )
620 {
621 pObjNew = Aig_ObjCreateCi(pNew);
622 pObjNew->Level = pObj->Level;
623 pObj->pData = pObjNew;
624 }
625 if ( p->nBarBufs == 0 )
626 {
627 Aig_ManForEachCo( p, pObj, i )
628 {
629 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
630 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
631 if ( pObjNew == NULL )
632 {
633 Vec_VecFree( vStore );
634 Aig_ManStop( pNew );
635 return NULL;
636 }
637 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
638 pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
639 }
640 }
641 else
642 {
643 Vec_Ptr_t * vLits = Vec_PtrStart( Aig_ManCoNum(p) );
644 Aig_ManForEachCo( p, pObj, i )
645 {
646 int k = i < p->nBarBufs ? Aig_ManCoNum(p) - p->nBarBufs + i : i - p->nBarBufs;
647 pObj = Aig_ManCo( p, k );
648 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
649 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
650 if ( pObjNew == NULL )
651 {
652 Vec_VecFree( vStore );
653 Aig_ManStop( pNew );
654 return NULL;
655 }
656 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
657 Vec_PtrWriteEntry( vLits, k, pObjNew );
658 if ( i < p->nBarBufs )
659 Aig_ManCi(pNew, Aig_ManCiNum(p) - p->nBarBufs + i)->Level = Aig_Regular(pObjNew)->Level;
660 }
661 Aig_ManForEachCo( p, pObj, i )
662 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vLits, i) );
663 Vec_PtrFree(vLits);
664 }
665 }
666 Vec_VecFree( vStore );
667 // remove dangling nodes
668 Aig_ManCleanup( pNew );
669 Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
670 // check the resulting AIG
671 if ( !Aig_ManCheck(pNew) )
672 printf( "Dar_ManBalance(): The check has failed.\n" );
673 return pNew;
674 }
675
676 /**Function*************************************************************
677
678 Synopsis [Reproduces script "compress2".]
679
680 Description []
681
682 SideEffects []
683
684 SeeAlso []
685
686 ***********************************************************************/
Dar_ManBalanceXor(Aig_Man_t * pAig,int fExor,int fUpdateLevel,int fVerbose)687 Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
688 {
689 Aig_Man_t * pAigXor, * pRes;
690 if ( fExor )
691 {
692 pAigXor = Aig_ManDupExor( pAig );
693 if ( fVerbose )
694 Dar_BalancePrintStats( pAigXor );
695 pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
696 Aig_ManStop( pAigXor );
697 }
698 else
699 {
700 pRes = Dar_ManBalance( pAig, fUpdateLevel );
701 }
702 return pRes;
703 }
704
705 /**Function*************************************************************
706
707 Synopsis [Inserts a new node in the order by levels.]
708
709 Description []
710
711 SideEffects []
712
713 SeeAlso []
714
715 ***********************************************************************/
Dar_BalancePrintStats(Aig_Man_t * p)716 void Dar_BalancePrintStats( Aig_Man_t * p )
717 {
718 Vec_Ptr_t * vSuper;
719 Aig_Obj_t * pObj, * pTemp;
720 int i, k;
721 if ( Aig_ManExorNum(p) == 0 )
722 {
723 printf( "There is no EXOR gates.\n" );
724 return;
725 }
726 Aig_ManForEachExor( p, pObj, i )
727 {
728 Aig_ObjFanin0(pObj)->fMarkA = 1;
729 Aig_ObjFanin1(pObj)->fMarkA = 1;
730 assert( !Aig_ObjFaninC0(pObj) );
731 assert( !Aig_ObjFaninC1(pObj) );
732 }
733 vSuper = Vec_PtrAlloc( 1000 );
734 Aig_ManForEachExor( p, pObj, i )
735 {
736 if ( pObj->fMarkA && pObj->nRefs == 1 )
737 continue;
738 Vec_PtrClear( vSuper );
739 Dar_BalanceCone_rec( pObj, pObj, vSuper );
740 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
741 pTemp->fMarkB = 0;
742 if ( Vec_PtrSize(vSuper) < 3 )
743 continue;
744 printf( " %d(", Vec_PtrSize(vSuper) );
745 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
746 printf( " %d", pTemp->Level );
747 printf( " )" );
748 }
749 Vec_PtrFree( vSuper );
750 Aig_ManForEachObj( p, pObj, i )
751 pObj->fMarkA = 0;
752 printf( "\n" );
753 }
754
755 ////////////////////////////////////////////////////////////////////////
756 /// END OF FILE ///
757 ////////////////////////////////////////////////////////////////////////
758
759
760 ABC_NAMESPACE_IMPL_END
761
762