1 /**CFile****************************************************************
2
3 FileName [abcReconv.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Computation of reconvergence-driven cuts.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcReconv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22
23 #ifdef ABC_USE_CUDD
24 #include "bdd/extrab/extraBdd.h"
25 #endif
26
27 ABC_NAMESPACE_IMPL_START
28
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 struct Abc_ManCut_t_
35 {
36 // user specified parameters
37 int nNodeSizeMax; // the limit on the size of the supernode
38 int nConeSizeMax; // the limit on the size of the containing cone
39 int nNodeFanStop; // the limit on the size of the supernode
40 int nConeFanStop; // the limit on the size of the containing cone
41 // internal parameters
42 Vec_Ptr_t * vNodeLeaves; // fanins of the collapsed node (the cut)
43 Vec_Ptr_t * vConeLeaves; // fanins of the containing cone
44 Vec_Ptr_t * vVisited; // the visited nodes
45 Vec_Vec_t * vLevels; // the data structure to compute TFO nodes
46 Vec_Ptr_t * vNodesTfo; // the nodes in the TFO of the cut
47 };
48
49 static int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit );
50 static int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit );
51 static void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
52
53 ////////////////////////////////////////////////////////////////////////
54 /// FUNCTION DEFINITIONS ///
55 ////////////////////////////////////////////////////////////////////////
56
57 /**Function*************************************************************
58
59 Synopsis [Unmarks the TFI cone.]
60
61 Description []
62
63 SideEffects []
64
65 SeeAlso []
66
67 ***********************************************************************/
Abc_NodesMark(Vec_Ptr_t * vVisited)68 static inline void Abc_NodesMark( Vec_Ptr_t * vVisited )
69 {
70 Abc_Obj_t * pNode;
71 int i;
72 Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
73 pNode->fMarkA = 1;
74 }
75
76 /**Function*************************************************************
77
78 Synopsis [Unmarks the TFI cone.]
79
80 Description []
81
82 SideEffects []
83
84 SeeAlso []
85
86 ***********************************************************************/
Abc_NodesUnmark(Vec_Ptr_t * vVisited)87 static inline void Abc_NodesUnmark( Vec_Ptr_t * vVisited )
88 {
89 Abc_Obj_t * pNode;
90 int i;
91 Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
92 pNode->fMarkA = 0;
93 }
94
95 /**Function*************************************************************
96
97 Synopsis [Unmarks the TFI cone.]
98
99 Description []
100
101 SideEffects []
102
103 SeeAlso []
104
105 ***********************************************************************/
Abc_NodesUnmarkB(Vec_Ptr_t * vVisited)106 static inline void Abc_NodesUnmarkB( Vec_Ptr_t * vVisited )
107 {
108 Abc_Obj_t * pNode;
109 int i;
110 Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
111 pNode->fMarkB = 0;
112 }
113
114 /**Function*************************************************************
115
116 Synopsis [Evaluate the cost of removing the node from the set of leaves.]
117
118 Description [Returns the number of new leaves that will be brought in.
119 Returns large number if the node cannot be removed from the set of leaves.]
120
121 SideEffects []
122
123 SeeAlso []
124
125 ***********************************************************************/
Abc_NodeGetLeafCostOne(Abc_Obj_t * pNode,int nFaninLimit)126 static inline int Abc_NodeGetLeafCostOne( Abc_Obj_t * pNode, int nFaninLimit )
127 {
128 int Cost;
129 // make sure the node is in the construction zone
130 assert( pNode->fMarkB == 1 );
131 // cannot expand over the PI node
132 if ( Abc_ObjIsCi(pNode) )
133 return 999;
134 // get the cost of the cone
135 Cost = (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
136 // always accept if the number of leaves does not increase
137 if ( Cost < 2 )
138 return Cost;
139 // skip nodes with many fanouts
140 if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
141 return 999;
142 // return the number of nodes that will be on the leaves if this node is removed
143 return Cost;
144 }
145
146 /**Function*************************************************************
147
148 Synopsis [Evaluate the cost of removing the node from the set of leaves.]
149
150 Description [Returns the number of new leaves that will be brought in.
151 Returns large number if the node cannot be removed from the set of leaves.]
152
153 SideEffects []
154
155 SeeAlso []
156
157 ***********************************************************************/
Abc_NodeGetLeafCostTwo(Abc_Obj_t * pNode,int nFaninLimit,Abc_Obj_t ** ppLeafToAdd,Abc_Obj_t ** pNodeToMark1,Abc_Obj_t ** pNodeToMark2)158 static inline int Abc_NodeGetLeafCostTwo( Abc_Obj_t * pNode, int nFaninLimit,
159 Abc_Obj_t ** ppLeafToAdd, Abc_Obj_t ** pNodeToMark1, Abc_Obj_t ** pNodeToMark2 )
160 {
161 Abc_Obj_t * pFanin0, * pFanin1, * pTemp;
162 Abc_Obj_t * pGrand, * pGrandToAdd;
163 // make sure the node is in the construction zone
164 assert( pNode->fMarkB == 1 );
165 // cannot expand over the PI node
166 if ( Abc_ObjIsCi(pNode) )
167 return 999;
168 // skip nodes with many fanouts
169 // if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
170 // return 999;
171 // get the children
172 pFanin0 = Abc_ObjFanin0(pNode);
173 pFanin1 = Abc_ObjFanin1(pNode);
174 assert( !pFanin0->fMarkB && !pFanin1->fMarkB );
175 // count the number of unique grandchildren that will be included
176 // return infinite cost if this number if more than 1
177 if ( Abc_ObjIsCi(pFanin0) && Abc_ObjIsCi(pFanin1) )
178 return 999;
179 // consider the special case when a non-CI fanin can be dropped
180 if ( !Abc_ObjIsCi(pFanin0) && Abc_ObjFanin0(pFanin0)->fMarkB && Abc_ObjFanin1(pFanin0)->fMarkB )
181 {
182 *ppLeafToAdd = pFanin1;
183 *pNodeToMark1 = pFanin0;
184 *pNodeToMark2 = NULL;
185 return 1;
186 }
187 if ( !Abc_ObjIsCi(pFanin1) && Abc_ObjFanin0(pFanin1)->fMarkB && Abc_ObjFanin1(pFanin1)->fMarkB )
188 {
189 *ppLeafToAdd = pFanin0;
190 *pNodeToMark1 = pFanin1;
191 *pNodeToMark2 = NULL;
192 return 1;
193 }
194
195 // make the first node CI if any
196 if ( Abc_ObjIsCi(pFanin1) )
197 pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
198 // consider the first node
199 pGrandToAdd = NULL;
200 if ( Abc_ObjIsCi(pFanin0) )
201 {
202 *pNodeToMark1 = NULL;
203 pGrandToAdd = pFanin0;
204 }
205 else
206 {
207 *pNodeToMark1 = pFanin0;
208 pGrand = Abc_ObjFanin0(pFanin0);
209 if ( !pGrand->fMarkB )
210 {
211 if ( pGrandToAdd && pGrandToAdd != pGrand )
212 return 999;
213 pGrandToAdd = pGrand;
214 }
215 pGrand = Abc_ObjFanin1(pFanin0);
216 if ( !pGrand->fMarkB )
217 {
218 if ( pGrandToAdd && pGrandToAdd != pGrand )
219 return 999;
220 pGrandToAdd = pGrand;
221 }
222 }
223 // consider the second node
224 *pNodeToMark2 = pFanin1;
225 pGrand = Abc_ObjFanin0(pFanin1);
226 if ( !pGrand->fMarkB )
227 {
228 if ( pGrandToAdd && pGrandToAdd != pGrand )
229 return 999;
230 pGrandToAdd = pGrand;
231 }
232 pGrand = Abc_ObjFanin1(pFanin1);
233 if ( !pGrand->fMarkB )
234 {
235 if ( pGrandToAdd && pGrandToAdd != pGrand )
236 return 999;
237 pGrandToAdd = pGrand;
238 }
239 assert( pGrandToAdd != NULL );
240 *ppLeafToAdd = pGrandToAdd;
241 return 1;
242 }
243
244
245 /**Function*************************************************************
246
247 Synopsis [Finds a fanin-limited, reconvergence-driven cut for the node.]
248
249 Description []
250
251 SideEffects []
252
253 SeeAlso []
254
255 ***********************************************************************/
Abc_NodeFindCut(Abc_ManCut_t * p,Abc_Obj_t * pRoot,int fContain)256 Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, int fContain )
257 {
258 Abc_Obj_t * pNode;
259 int i;
260
261 assert( !Abc_ObjIsComplement(pRoot) );
262 assert( Abc_ObjIsNode(pRoot) );
263
264 // start the visited nodes and mark them
265 Vec_PtrClear( p->vVisited );
266 Vec_PtrPush( p->vVisited, pRoot );
267 Vec_PtrPush( p->vVisited, Abc_ObjFanin0(pRoot) );
268 Vec_PtrPush( p->vVisited, Abc_ObjFanin1(pRoot) );
269 pRoot->fMarkB = 1;
270 Abc_ObjFanin0(pRoot)->fMarkB = 1;
271 Abc_ObjFanin1(pRoot)->fMarkB = 1;
272
273 // start the cut
274 Vec_PtrClear( p->vNodeLeaves );
275 Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin0(pRoot) );
276 Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin1(pRoot) );
277
278 // compute the cut
279 while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vNodeLeaves, p->nNodeSizeMax, p->nNodeFanStop ) );
280 assert( Vec_PtrSize(p->vNodeLeaves) <= p->nNodeSizeMax );
281
282 // return if containing cut is not requested
283 if ( !fContain )
284 {
285 // unmark both fMarkA and fMarkB in tbe TFI
286 Abc_NodesUnmarkB( p->vVisited );
287 return p->vNodeLeaves;
288 }
289
290 //printf( "\n\n\n" );
291 // compute the containing cut
292 assert( p->nNodeSizeMax < p->nConeSizeMax );
293 // copy the current boundary
294 Vec_PtrClear( p->vConeLeaves );
295 Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodeLeaves, pNode, i )
296 Vec_PtrPush( p->vConeLeaves, pNode );
297 // compute the containing cut
298 while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vConeLeaves, p->nConeSizeMax, p->nConeFanStop ) );
299 assert( Vec_PtrSize(p->vConeLeaves) <= p->nConeSizeMax );
300 // unmark TFI using fMarkA and fMarkB
301 Abc_NodesUnmarkB( p->vVisited );
302 return p->vNodeLeaves;
303 }
304
305 /**Function*************************************************************
306
307 Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]
308
309 Description [This procedure looks at the current leaves and tries to change
310 one leaf at a time in such a way that the cut grows as little as possible.
311 In evaluating the fanins, this procedure looks only at their immediate
312 predecessors (this is why it is called a one-level construction procedure).]
313
314 SideEffects []
315
316 SeeAlso []
317
318 ***********************************************************************/
Abc_NodeBuildCutLevelOne_int(Vec_Ptr_t * vVisited,Vec_Ptr_t * vLeaves,int nSizeLimit,int nFaninLimit)319 int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit )
320 {
321 Abc_Obj_t * pNode, * pFaninBest, * pNext;
322 int CostBest, CostCur, i;
323 // find the best fanin
324 CostBest = 100;
325 pFaninBest = NULL;
326 //printf( "Evaluating fanins of the cut:\n" );
327 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
328 {
329 CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
330 //printf( " Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
331 // if ( CostBest > CostCur ) // performance improvement: expand the variable with the smallest level
332 if ( CostBest > CostCur ||
333 (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
334 {
335 CostBest = CostCur;
336 pFaninBest = pNode;
337 }
338 if ( CostBest == 0 )
339 break;
340 }
341 if ( pFaninBest == NULL )
342 return 0;
343 // return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
344
345 assert( CostBest < 3 );
346 if ( vLeaves->nSize - 1 + CostBest > nSizeLimit )
347 return 0;
348 // return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
349
350 assert( Abc_ObjIsNode(pFaninBest) );
351 // remove the node from the array
352 Vec_PtrRemove( vLeaves, pFaninBest );
353 //printf( "Removing fanin %s.\n", Abc_ObjName(pFaninBest) );
354
355 // add the left child to the fanins
356 pNext = Abc_ObjFanin0(pFaninBest);
357 if ( !pNext->fMarkB )
358 {
359 //printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
360 pNext->fMarkB = 1;
361 Vec_PtrPush( vLeaves, pNext );
362 Vec_PtrPush( vVisited, pNext );
363 }
364 // add the right child to the fanins
365 pNext = Abc_ObjFanin1(pFaninBest);
366 if ( !pNext->fMarkB )
367 {
368 //printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
369 pNext->fMarkB = 1;
370 Vec_PtrPush( vLeaves, pNext );
371 Vec_PtrPush( vVisited, pNext );
372 }
373 assert( vLeaves->nSize <= nSizeLimit );
374 // keep doing this
375 return 1;
376 }
377
378 /**Function*************************************************************
379
380 Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]
381
382 Description [This procedure looks at the current leaves and tries to change
383 one leaf at a time in such a way that the cut grows as little as possible.
384 In evaluating the fanins, this procedure looks across two levels of fanins
385 (this is why it is called a two-level construction procedure).]
386
387 SideEffects []
388
389 SeeAlso []
390
391 ***********************************************************************/
Abc_NodeBuildCutLevelTwo_int(Vec_Ptr_t * vVisited,Vec_Ptr_t * vLeaves,int nFaninLimit)392 int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit )
393 {
394 Abc_Obj_t * pNode = NULL, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
395 int CostCur = 0, i;
396 // find the best fanin
397 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
398 {
399 CostCur = Abc_NodeGetLeafCostTwo( pNode, nFaninLimit, &pLeafToAdd, &pNodeToMark1, &pNodeToMark2 );
400 if ( CostCur < 2 )
401 break;
402 }
403 if ( CostCur > 2 )
404 return 0;
405 // remove the node from the array
406 Vec_PtrRemove( vLeaves, pNode );
407 // add the node to the leaves
408 if ( pLeafToAdd )
409 {
410 assert( !pLeafToAdd->fMarkB );
411 pLeafToAdd->fMarkB = 1;
412 Vec_PtrPush( vLeaves, pLeafToAdd );
413 Vec_PtrPush( vVisited, pLeafToAdd );
414 }
415 // mark the other nodes
416 if ( pNodeToMark1 )
417 {
418 assert( !pNodeToMark1->fMarkB );
419 pNodeToMark1->fMarkB = 1;
420 Vec_PtrPush( vVisited, pNodeToMark1 );
421 }
422 if ( pNodeToMark2 )
423 {
424 assert( !pNodeToMark2->fMarkB );
425 pNodeToMark2->fMarkB = 1;
426 Vec_PtrPush( vVisited, pNodeToMark2 );
427 }
428 // keep doing this
429 return 1;
430 }
431
432
433 /**Function*************************************************************
434
435 Synopsis [Get the nodes contained in the cut.]
436
437 Description []
438
439 SideEffects []
440
441 SeeAlso []
442
443 ***********************************************************************/
Abc_NodeConeCollect(Abc_Obj_t ** ppRoots,int nRoots,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vVisited,int fIncludeFanins)444 void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited, int fIncludeFanins )
445 {
446 Abc_Obj_t * pTemp;
447 int i;
448 // mark the fanins of the cone
449 Abc_NodesMark( vLeaves );
450 // collect the nodes in the DFS order
451 Vec_PtrClear( vVisited );
452 // add the fanins
453 if ( fIncludeFanins )
454 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pTemp, i )
455 Vec_PtrPush( vVisited, pTemp );
456 // add other nodes
457 for ( i = 0; i < nRoots; i++ )
458 Abc_NodeConeMarkCollect_rec( ppRoots[i], vVisited );
459 // unmark both sets
460 Abc_NodesUnmark( vLeaves );
461 Abc_NodesUnmark( vVisited );
462 }
463
464 /**Function*************************************************************
465
466 Synopsis [Marks the TFI cone.]
467
468 Description []
469
470 SideEffects []
471
472 SeeAlso []
473
474 ***********************************************************************/
Abc_NodeConeMarkCollect_rec(Abc_Obj_t * pNode,Vec_Ptr_t * vVisited)475 void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
476 {
477 if ( pNode->fMarkA == 1 )
478 return;
479 // visit transitive fanin
480 if ( Abc_ObjIsNode(pNode) )
481 {
482 Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
483 Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
484 }
485 assert( pNode->fMarkA == 0 );
486 pNode->fMarkA = 1;
487 Vec_PtrPush( vVisited, pNode );
488 }
489
490 #ifdef ABC_USE_CUDD
491
492 /**Function*************************************************************
493
494 Synopsis [Returns BDD representing the logic function of the cone.]
495
496 Description []
497
498 SideEffects []
499
500 SeeAlso []
501
502 ***********************************************************************/
Abc_NodeConeBdd(DdManager * dd,DdNode ** pbVars,Abc_Obj_t * pRoot,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vVisited)503 DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
504 {
505 Abc_Obj_t * pNode;
506 DdNode * bFunc0, * bFunc1, * bFunc = NULL;
507 int i;
508 // get the nodes in the cut without fanins in the DFS order
509 Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 );
510 // set the elementary BDDs
511 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
512 pNode->pCopy = (Abc_Obj_t *)pbVars[i];
513 // compute the BDDs for the collected nodes
514 Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
515 {
516 assert( !Abc_ObjIsPi(pNode) );
517 bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, (int)Abc_ObjFaninC0(pNode) );
518 bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, (int)Abc_ObjFaninC1(pNode) );
519 bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
520 pNode->pCopy = (Abc_Obj_t *)bFunc;
521 }
522 assert(bFunc);
523 Cudd_Ref( bFunc );
524 // dereference the intermediate ones
525 Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
526 Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
527 Cudd_Deref( bFunc );
528 return bFunc;
529 }
530
531 /**Function*************************************************************
532
533 Synopsis [Returns BDD representing the transition relation of the cone.]
534
535 Description []
536
537 SideEffects []
538
539 SeeAlso []
540
541 ***********************************************************************/
Abc_NodeConeDcs(DdManager * dd,DdNode ** pbVarsX,DdNode ** pbVarsY,Vec_Ptr_t * vLeaves,Vec_Ptr_t * vRoots,Vec_Ptr_t * vVisited)542 DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited )
543 {
544 DdNode * bFunc0, * bFunc1, * bFunc, * bTrans, * bTemp, * bCube, * bResult;
545 Abc_Obj_t * pNode;
546 int i;
547 // get the nodes in the cut without fanins in the DFS order
548 Abc_NodeConeCollect( (Abc_Obj_t **)vRoots->pArray, vRoots->nSize, vLeaves, vVisited, 0 );
549 // set the elementary BDDs
550 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
551 pNode->pCopy = (Abc_Obj_t *)pbVarsX[i];
552 // compute the BDDs for the collected nodes
553 Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
554 {
555 bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, (int)Abc_ObjFaninC0(pNode) );
556 bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, (int)Abc_ObjFaninC1(pNode) );
557 bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc );
558 pNode->pCopy = (Abc_Obj_t *)bFunc;
559 }
560 // compute the transition relation of the cone
561 bTrans = b1; Cudd_Ref( bTrans );
562 Vec_PtrForEachEntry( Abc_Obj_t *, vRoots, pNode, i )
563 {
564 bFunc = Cudd_bddXnor( dd, (DdNode *)pNode->pCopy, pbVarsY[i] ); Cudd_Ref( bFunc );
565 bTrans = Cudd_bddAnd( dd, bTemp = bTrans, bFunc ); Cudd_Ref( bTrans );
566 Cudd_RecursiveDeref( dd, bTemp );
567 Cudd_RecursiveDeref( dd, bFunc );
568 }
569 // dereference the intermediate ones
570 Vec_PtrForEachEntry( Abc_Obj_t *, vVisited, pNode, i )
571 Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
572 // compute don't-cares
573 bCube = Extra_bddComputeRangeCube( dd, vRoots->nSize, vRoots->nSize + vLeaves->nSize ); Cudd_Ref( bCube );
574 bResult = Cudd_bddExistAbstract( dd, bTrans, bCube ); Cudd_Ref( bResult );
575 bResult = Cudd_Not( bResult );
576 Cudd_RecursiveDeref( dd, bCube );
577 Cudd_RecursiveDeref( dd, bTrans );
578 Cudd_Deref( bResult );
579 return bResult;
580 }
581
582 #endif
583
584 /**Function*************************************************************
585
586 Synopsis [Starts the resynthesis manager.]
587
588 Description []
589
590 SideEffects []
591
592 SeeAlso []
593
594 ***********************************************************************/
Abc_NtkManCutStart(int nNodeSizeMax,int nConeSizeMax,int nNodeFanStop,int nConeFanStop)595 Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop )
596 {
597 Abc_ManCut_t * p;
598 p = ABC_ALLOC( Abc_ManCut_t, 1 );
599 memset( p, 0, sizeof(Abc_ManCut_t) );
600 p->vNodeLeaves = Vec_PtrAlloc( 100 );
601 p->vConeLeaves = Vec_PtrAlloc( 100 );
602 p->vVisited = Vec_PtrAlloc( 100 );
603 p->vLevels = Vec_VecAlloc( 100 );
604 p->vNodesTfo = Vec_PtrAlloc( 100 );
605 p->nNodeSizeMax = nNodeSizeMax;
606 p->nConeSizeMax = nConeSizeMax;
607 p->nNodeFanStop = nNodeFanStop;
608 p->nConeFanStop = nConeFanStop;
609 return p;
610 }
611
612 /**Function*************************************************************
613
614 Synopsis [Stops the resynthesis manager.]
615
616 Description []
617
618 SideEffects []
619
620 SeeAlso []
621
622 ***********************************************************************/
Abc_NtkManCutStop(Abc_ManCut_t * p)623 void Abc_NtkManCutStop( Abc_ManCut_t * p )
624 {
625 Vec_PtrFree( p->vNodeLeaves );
626 Vec_PtrFree( p->vConeLeaves );
627 Vec_PtrFree( p->vVisited );
628 Vec_VecFree( p->vLevels );
629 Vec_PtrFree( p->vNodesTfo );
630 ABC_FREE( p );
631 }
632
633 /**Function*************************************************************
634
635 Synopsis [Returns the leaves of the cone.]
636
637 Description []
638
639 SideEffects []
640
641 SeeAlso []
642
643 ***********************************************************************/
Abc_NtkManCutReadCutLarge(Abc_ManCut_t * p)644 Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
645 {
646 return p->vConeLeaves;
647 }
648
649 /**Function*************************************************************
650
651 Synopsis [Returns the leaves of the cone.]
652
653 Description []
654
655 SideEffects []
656
657 SeeAlso []
658
659 ***********************************************************************/
Abc_NtkManCutReadCutSmall(Abc_ManCut_t * p)660 Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p )
661 {
662 return p->vNodeLeaves;
663 }
664
665 /**Function*************************************************************
666
667 Synopsis [Returns the leaves of the cone.]
668
669 Description []
670
671 SideEffects []
672
673 SeeAlso []
674
675 ***********************************************************************/
Abc_NtkManCutReadVisited(Abc_ManCut_t * p)676 Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
677 {
678 return p->vVisited;
679 }
680
681
682
683 /**Function*************************************************************
684
685 Synopsis [Collects the TFO of the cut in the topological order.]
686
687 Description [TFO of the cut is defined as a set of nodes, for which the cut
688 is a cut, that is, every path from the collected nodes to the CIs goes through
689 a node in the cut. The nodes are collected if their level does not exceed
690 the given number (LevelMax). The nodes are returned in the topological order.
691 If the root node is given, its MFFC is marked, so that the collected nodes
692 do not contain any nodes in the MFFC.]
693
694 SideEffects []
695
696 SeeAlso []
697
698 ***********************************************************************/
Abc_NodeCollectTfoCands(Abc_ManCut_t * p,Abc_Obj_t * pRoot,Vec_Ptr_t * vLeaves,int LevelMax)699 Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int LevelMax )
700 {
701 Abc_Ntk_t * pNtk = pRoot->pNtk;
702 Vec_Ptr_t * vVec;
703 Abc_Obj_t * pNode, * pFanout;
704 int i, k, v, LevelMin;
705 assert( Abc_NtkIsStrash(pNtk) );
706
707 // assuming that the structure is clean
708 Vec_VecForEachLevel( p->vLevels, vVec, i )
709 assert( vVec->nSize == 0 );
710
711 // put fanins into the structure while labeling them
712 Abc_NtkIncrementTravId( pNtk );
713 LevelMin = -1;
714 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
715 {
716 if ( pNode->Level > (unsigned)LevelMax )
717 continue;
718 Abc_NodeSetTravIdCurrent( pNode );
719 Vec_VecPush( p->vLevels, pNode->Level, pNode );
720 if ( LevelMin < (int)pNode->Level )
721 LevelMin = pNode->Level;
722 }
723 assert( LevelMin >= 0 );
724
725 // mark MFFC
726 if ( pRoot )
727 Abc_NodeMffcLabelAig( pRoot );
728
729 // go through the levels up
730 Vec_PtrClear( p->vNodesTfo );
731 Vec_VecForEachEntryStart( Abc_Obj_t *, p->vLevels, pNode, i, k, LevelMin )
732 {
733 if ( i > LevelMax )
734 break;
735 // if the node is not marked, it is not a fanin
736 if ( !Abc_NodeIsTravIdCurrent(pNode) )
737 {
738 // check if it belongs to the TFO
739 if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) ||
740 !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
741 continue;
742 // save the node in the TFO and label it
743 Vec_PtrPush( p->vNodesTfo, pNode );
744 Abc_NodeSetTravIdCurrent( pNode );
745 }
746 // go through the fanouts and add them to the structure if they meet the conditions
747 Abc_ObjForEachFanout( pNode, pFanout, v )
748 {
749 // skip if fanout is a CO or its level exceeds
750 if ( Abc_ObjIsCo(pFanout) || pFanout->Level > (unsigned)LevelMax )
751 continue;
752 // skip if it is already added or if it is in MFFC
753 if ( Abc_NodeIsTravIdCurrent(pFanout) )
754 continue;
755 // add it to the structure but do not mark it (until tested later)
756 Vec_VecPushUnique( p->vLevels, pFanout->Level, pFanout );
757 }
758 }
759
760 // clear the levelized structure
761 Vec_VecForEachLevelStart( p->vLevels, vVec, i, LevelMin )
762 {
763 if ( i > LevelMax )
764 break;
765 Vec_PtrClear( vVec );
766 }
767 return p->vNodesTfo;
768 }
769
770 ////////////////////////////////////////////////////////////////////////
771 /// END OF FILE ///
772 ////////////////////////////////////////////////////////////////////////
773
774
775 ABC_NAMESPACE_IMPL_END
776
777