ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
abcMinBase.c
Go to the documentation of this file.
1
20
21#include "abc.h"
22
23#ifdef ABC_USE_CUDD
24#include "bdd/extrab/extraBdd.h"
25#endif
26
27ABC_NAMESPACE_IMPL_START
28
29
33
34#ifdef ABC_USE_CUDD
35
36extern int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars );
37
41
53int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk )
54{
55 Abc_Obj_t * pNode;
56 int i, Counter;
57 assert( Abc_NtkIsBddLogic(pNtk) );
58 Counter = 0;
59 Abc_NtkForEachNode( pNtk, pNode, i )
60 Counter += Abc_NodeMinimumBase( pNode );
61 return Counter;
62}
63
75int Abc_NodeMinimumBase_buggy( Abc_Obj_t * pNode )
76{
77 Vec_Str_t * vSupport;
78 Vec_Ptr_t * vFanins;
79 DdNode * bTemp;
80 int i, nVars;
81
82 assert( Abc_NtkIsBddLogic(pNode->pNtk) );
83 assert( Abc_ObjIsNode(pNode) );
84
85 // compute support
86 vSupport = Vec_StrAlloc( 10 );
87 nVars = Abc_NodeSupport( Cudd_Regular(pNode->pData), vSupport, Abc_ObjFaninNum(pNode) );
88 if ( nVars == Abc_ObjFaninNum(pNode) )
89 {
90 Vec_StrFree( vSupport );
91 return 0;
92 }
93
94 // remove unused fanins
95 vFanins = Vec_PtrAlloc( Abc_ObjFaninNum(pNode) );
96 Abc_NodeCollectFanins( pNode, vFanins );
97 for ( i = 0; i < vFanins->nSize; i++ )
98 if ( vSupport->pArray[i] == 0 )
99 Abc_ObjDeleteFanin( pNode, (Abc_Obj_t *)vFanins->pArray[i] );
100 assert( nVars == Abc_ObjFaninNum(pNode) );
101
102 // update the function of the node
103 pNode->pData = Extra_bddRemapUp( (DdManager *)pNode->pNtk->pManFunc, bTemp = (DdNode *)pNode->pData ); Cudd_Ref( (DdNode *)pNode->pData );
104 Cudd_RecursiveDeref( (DdManager *)pNode->pNtk->pManFunc, bTemp );
105 Vec_PtrFree( vFanins );
106 Vec_StrFree( vSupport );
107 return 1;
108}
109
110int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
111{
112 DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
113 DdNode * bTemp, ** pbVars;
114 Vec_Str_t * vSupport;
115 int i, nVars, j, iFanin, iFanin2, k = 0;
116 int ddSize, fDupFanins = 0;
117
118 assert( Abc_NtkIsBddLogic(pNode->pNtk) );
119 assert( Abc_ObjIsNode(pNode) );
120
121 // compute support
122 vSupport = Vec_StrAlloc( 10 );
123 nVars = Abc_NodeSupport( Cudd_Regular(pNode->pData), vSupport, Abc_ObjFaninNum(pNode) );
124 if ( nVars == Abc_ObjFaninNum(pNode) )
125 {
126 Vec_StrFree( vSupport );
127 return 0;
128 }
129
130 // remove unused fanins.
131
132 // By default, every BDD variable stays equivalent to itself.
133 ddSize = Cudd_ReadSize( dd );
134 pbVars = ABC_CALLOC( DdNode *, ddSize );
135 for (i = 0; i < ddSize; i += 1 ) {
136 pbVars[i] = Cudd_bddIthVar( dd, i );
137 }
138 Vec_IntForEachEntry( &pNode->vFanins, iFanin, i )
139 {
140 Abc_Obj_t * pFanin = Abc_NtkObj( pNode->pNtk, iFanin );
141 if ( !Vec_StrEntry(vSupport, i) )
142 {
143 if ( !Vec_IntRemove( &pFanin->vFanouts, pNode->Id ) )
144 printf( "The obj %d is not found among the fanouts of obj %d ...\n", pNode->Id, iFanin );
145 continue;
146 }
147 Vec_IntForEachEntryStop( &pNode->vFanins, iFanin2, j, k )
148 if ( iFanin == iFanin2 )
149 break;
150 fDupFanins |= (int)(j < k);
151 if ( j == k )
152 Vec_IntWriteEntry( &pNode->vFanins, k++, iFanin );
153 else if ( !Vec_IntRemove( &pFanin->vFanouts, pNode->Id ) )
154 printf( "The obj %d is not found among the fanouts of obj %d ...\n", pNode->Id, iFanin );
155
156 // i-th variable becomes equivalent to j-th variable (can be itself)
157 pbVars[i] = Cudd_bddIthVar( dd, j );
158 }
159 Vec_IntShrink( &pNode->vFanins, k );
160
161 // update the function of the node
162 if ( ! Cudd_IsConstant((DdNode *) pNode->pData ) ) {
163 pNode->pData = Cudd_bddVectorCompose( dd, bTemp = (DdNode *)pNode->pData, pbVars );
164 Cudd_Ref( (DdNode *)pNode->pData );
165 Cudd_RecursiveDeref( dd, bTemp );
166 }
167 Vec_StrFree( vSupport );
168 ABC_FREE( pbVars );
169
170 // try again if node had duplicated fanins
171 if ( fDupFanins )
172 Abc_NodeMinimumBase( pNode );
173 return 1;
174}
175
187int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk )
188{
189 Abc_Obj_t * pNode;
190 int i, Counter;
191 assert( Abc_NtkIsBddLogic(pNtk) );
192 Counter = 0;
193 Abc_NtkForEachNode( pNtk, pNode, i )
194 Counter += Abc_NodeRemoveDupFanins( pNode );
195 return Counter;
196}
197
209int Abc_NodeRemoveDupFanins_int( Abc_Obj_t * pNode )
210{
211 Abc_Obj_t * pFanin1, * pFanin2;
212 int i, k;
213 assert( Abc_NtkIsBddLogic(pNode->pNtk) );
214 assert( Abc_ObjIsNode(pNode) );
215 // make sure fanins are not duplicated
216 Abc_ObjForEachFanin( pNode, pFanin2, i )
217 {
218 Abc_ObjForEachFanin( pNode, pFanin1, k )
219 {
220 if ( k >= i )
221 break;
222 if ( pFanin1 == pFanin2 )
223 {
224 DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
225 DdNode * bVar1 = Cudd_bddIthVar( dd, i );
226 DdNode * bVar2 = Cudd_bddIthVar( dd, k );
227 DdNode * bTrans, * bTemp;
228 bTrans = Cudd_bddXnor( dd, bVar1, bVar2 ); Cudd_Ref( bTrans );
229 pNode->pData = Cudd_bddAndAbstract( dd, bTemp = (DdNode *)pNode->pData, bTrans, bVar2 ); Cudd_Ref( (DdNode *)pNode->pData );
230 Cudd_RecursiveDeref( dd, bTemp );
231 Cudd_RecursiveDeref( dd, bTrans );
232 Abc_NodeMinimumBase( pNode );
233 return 1;
234 }
235 }
236 }
237 return 0;
238}
239
251int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode )
252{
253 int Counter = 0;
254 while ( Abc_NodeRemoveDupFanins_int(pNode) )
255 Counter++;
256 return Counter;
257}
269void Abc_NodeSupport_rec( DdNode * bFunc, Vec_Str_t * vSupport )
270{
271 if ( cuddIsConstant(bFunc) || Cudd_IsComplement(bFunc->next) )
272 return;
273 vSupport->pArray[ bFunc->index ] = 1;
274 Abc_NodeSupport_rec( cuddT(bFunc), vSupport );
275 Abc_NodeSupport_rec( Cudd_Regular(cuddE(bFunc)), vSupport );
276 bFunc->next = Cudd_Not(bFunc->next);
277}
278
290void Abc_NodeSupportClear_rec( DdNode * bFunc )
291{
292 if ( !Cudd_IsComplement(bFunc->next) )
293 return;
294 bFunc->next = Cudd_Regular(bFunc->next);
295 if ( cuddIsConstant(bFunc) )
296 return;
297 Abc_NodeSupportClear_rec( cuddT(bFunc) );
298 Abc_NodeSupportClear_rec( Cudd_Regular(cuddE(bFunc)) );
299}
300
312int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars )
313{
314 int Counter, i;
315 // compute the support by marking the BDD
316 Vec_StrFill( vSupport, nVars, 0 );
317 Abc_NodeSupport_rec( bFunc, vSupport );
318 // clear the marak
319 Abc_NodeSupportClear_rec( bFunc );
320 // get the number of support variables
321 Counter = 0;
322 for ( i = 0; i < nVars; i++ )
323 Counter += vSupport->pArray[i];
324 return Counter;
325}
326
327
328
340int Abc_NodeCheckDupFanin( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, int * piFanin )
341{
342 Abc_Obj_t * pObj;
343 int i, Counter = 0;
344 Abc_ObjForEachFanin( pFanout, pObj, i )
345 if ( pObj == pFanin )
346 {
347 if ( piFanin )
348 *piFanin = i;
349 Counter++;
350 }
351 return Counter;
352}
353
365int Abc_NodeCollapseSuppSize( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins )
366{
367 Abc_Obj_t * pObj;
368 int i;
369 Vec_PtrClear( vFanins );
370 Abc_ObjForEachFanin( pFanout, pObj, i )
371 if ( pObj != pFanin )
372 Vec_PtrPushUnique( vFanins, pObj );
373 Abc_ObjForEachFanin( pFanin, pObj, i )
374 Vec_PtrPushUnique( vFanins, pObj );
375 return Vec_PtrSize( vFanins );
376}
377
389int Abc_ObjFaninNumberNew( Vec_Ptr_t * vFanins, Abc_Obj_t * pFanin )
390{
391 Abc_Obj_t * pObj;
392 int i;
393 Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
394 if ( pObj == pFanin )
395 return i;
396 return -1;
397}
398
410int Abc_NodeCollapsePermMap( Abc_Obj_t * pNode, Abc_Obj_t * pSkip, Vec_Ptr_t * vFanins, int * pPerm )
411{
412 Abc_Obj_t * pFanin;
413 int i;
414 for ( i = 0; i < Vec_PtrSize(vFanins); i++ )
415 pPerm[i] = i;
416 Abc_ObjForEachFanin( pNode, pFanin, i )
417 {
418 if ( pFanin == pSkip )
419 continue;
420 pPerm[i] = Abc_ObjFaninNumberNew( vFanins, pFanin );
421 if ( pPerm[i] == -1 )
422 return 0;
423 }
424 return 1;
425}
426
427
428
440DdNode * Abc_NodeCollapseFunc( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
441{
442 DdManager * dd = (DdManager *)pFanin->pNtk->pManFunc;
443 DdNode * bVar, * bFunc0, * bFunc1, * bTemp, * bFanin, * bFanout;
444 int RetValue, nSize, iFanin;
445 // can only eliminate if fanin occurs in the fanin list of the fanout exactly once
446 if ( Abc_NodeCheckDupFanin( pFanin, pFanout, &iFanin ) != 1 )
447 return NULL;
448 // find the new number of fanins after collapsing
449 nSize = Abc_NodeCollapseSuppSize( pFanin, pFanout, vFanins );
450 bVar = Cudd_bddIthVar( dd, nSize - 1 );
451 assert( nSize <= dd->size );
452 // find the permutation after collapsing
453 RetValue = Abc_NodeCollapsePermMap( pFanin, NULL, vFanins, pPermFanin );
454 assert( RetValue );
455 RetValue = Abc_NodeCollapsePermMap( pFanout, pFanin, vFanins, pPermFanout );
456 assert( RetValue );
457 // cofactor the local function of the node
458 bVar = Cudd_bddIthVar( dd, iFanin );
459 bFunc0 = Cudd_Cofactor( dd, (DdNode *)pFanout->pData, Cudd_Not(bVar) ); Cudd_Ref( bFunc0 );
460 bFunc1 = Cudd_Cofactor( dd, (DdNode *)pFanout->pData, bVar ); Cudd_Ref( bFunc1 );
461 // find the permutation after collapsing
462 bFunc0 = Cudd_bddPermute( dd, bTemp = bFunc0, pPermFanout ); Cudd_Ref( bFunc0 );
463 Cudd_RecursiveDeref( dd, bTemp );
464 bFunc1 = Cudd_bddPermute( dd, bTemp = bFunc1, pPermFanout ); Cudd_Ref( bFunc1 );
465 Cudd_RecursiveDeref( dd, bTemp );
466 bFanin = Cudd_bddPermute( dd, (DdNode *)pFanin->pData, pPermFanin ); Cudd_Ref( bFanin );
467 // create the new function
468 bFanout = Cudd_bddIte( dd, bFanin, bFunc1, bFunc0 ); Cudd_Ref( bFanout );
469 Cudd_RecursiveDeref( dd, bFanin );
470 Cudd_RecursiveDeref( dd, bFunc1 );
471 Cudd_RecursiveDeref( dd, bFunc0 );
472 Cudd_Deref( bFanout );
473 return bFanout;
474}
475int Abc_NodeCollapse( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
476{
477 Abc_Obj_t * pFanoutNew, * pObj;
478 DdNode * bFanoutNew;
479 int i;
480 assert( Abc_NtkIsBddLogic(pFanin->pNtk) );
481 assert( Abc_ObjIsNode(pFanin) );
482 assert( Abc_ObjIsNode(pFanout) );
483 bFanoutNew = Abc_NodeCollapseFunc( pFanin, pFanout, vFanins, pPermFanin, pPermFanout );
484 if ( bFanoutNew == NULL )
485 return 0;
486 Cudd_Ref( bFanoutNew );
487 // create the new node
488 pFanoutNew = Abc_NtkCreateNode( pFanin->pNtk );
489 Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
490 Abc_ObjAddFanin( pFanoutNew, pObj );
491 pFanoutNew->pData = bFanoutNew;
492 // minimize the node
493 Abc_NodeMinimumBase( pFanoutNew );
494 // transfer the fanout
495 Abc_ObjTransferFanout( pFanout, pFanoutNew );
496 assert( Abc_ObjFanoutNum( pFanout ) == 0 );
497 Abc_NtkDeleteObj_rec( pFanout, 1 );
498 return 1;
499}
500int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose )
501{
502 extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
503 Vec_Ptr_t * vFanouts, * vFanins, * vNodes;
504 Abc_Obj_t * pNode, * pFanout;
505 int * pPermFanin, * pPermFanout;
506 int RetValue, i, k;
507 assert( nMaxSize > 0 );
508 assert( Abc_NtkIsLogic(pNtk) );
509 // convert network to BDD representation
510 if ( !Abc_NtkToBdd(pNtk) )
511 {
512 fprintf( stdout, "Converting to BDD has failed.\n" );
513 return 0;
514 }
515 // prepare nodes for sweeping
516 //Abc_NtkRemoveDupFanins( pNtk );
517 Abc_NtkMinimumBase( pNtk );
518 Abc_NtkCleanup( pNtk, 0 );
519 // get the nodes in the given order
520 vNodes = fReverse? Abc_NtkDfsReverse( pNtk ) : Abc_NtkDfs( pNtk, 0 );
521 // go through the nodes and decide is they can be eliminated
522 pPermFanin = ABC_ALLOC( int, nMaxSize + 1000 );
523 pPermFanout = ABC_ALLOC( int, nMaxSize + 1000 );
524 vFanins = Vec_PtrAlloc( 1000 );
525 vFanouts = Vec_PtrAlloc( 1000 );
526 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
527 {
528 if ( !Abc_ObjIsNode(pNode) ) // skip deleted nodes
529 continue;
530 if ( Abc_NodeFindCoFanout(pNode) != NULL )
531 continue;
532 if ( Abc_ObjFaninNum(pNode) > nMaxSize )
533 continue;
534 Abc_ObjForEachFanout( pNode, pFanout, k )
535 if ( Abc_NodeCollapseSuppSize(pNode, pFanout, vFanins) > nMaxSize )
536 break;
537 if ( k < Abc_ObjFanoutNum(pNode) )
538 continue;
539 // perform elimination
540 Abc_NodeCollectFanouts( pNode, vFanouts );
541 Vec_PtrForEachEntry( Abc_Obj_t *, vFanouts, pFanout, k )
542 {
543 if ( fVerbose )
544 printf( "Collapsing fanin %5d (supp =%2d) into fanout %5d (supp =%2d) ",
545 Abc_ObjId(pNode), Abc_ObjFaninNum(pNode), Abc_ObjId(pFanout), Abc_ObjFaninNum(pFanout) );
546 RetValue = Abc_NodeCollapse( pNode, pFanout, vFanins, pPermFanin, pPermFanout );
547 assert( RetValue );
548 if ( fVerbose )
549 {
550 Abc_Obj_t * pNodeNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk) - 1 );
551 if ( pNodeNew )
552 printf( "resulting in node %5d (supp =%2d).\n", Abc_ObjId(pNodeNew), Abc_ObjFaninNum(pNodeNew) );
553 }
554 }
555 }
556 Abc_NtkBddReorder( pNtk, 0 );
557 Vec_PtrFree( vFanins );
558 Vec_PtrFree( vFanouts );
559 Vec_PtrFree( vNodes );
560 ABC_FREE( pPermFanin );
561 ABC_FREE( pPermFanout );
562 return 1;
563}
564
565
566
578int Abc_NodeCountAppearances( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout )
579{
580 Hop_Man_t * pMan = (Hop_Man_t *)pFanin->pNtk->pManFunc;
581 int iFanin = Abc_NodeFindFanin( pFanout, pFanin );
582 assert( iFanin >= 0 && iFanin < Hop_ManPiNum(pMan) );
583 return Hop_ObjFanoutCount( (Hop_Obj_t *)pFanout->pData, Hop_IthVar(pMan, iFanin) );
584}
585int Abc_NodeCountAppearancesAll( Abc_Obj_t * pNode )
586{
587 Abc_Obj_t * pFanout;
588 int i, Count = 0;
589 Abc_ObjForEachFanout( pNode, pFanout, i )
590 Count += Abc_NodeCountAppearances( pNode, pFanout );
591 return Count;
592}
593
605Hop_Obj_t * Abc_NodeCollapseFunc1( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
606{
607 Hop_Man_t * pMan = (Hop_Man_t *)pFanin->pNtk->pManFunc;
608 Hop_Obj_t * bFanin, * bFanout;
609 int RetValue, nSize, iFanin;
610 // can only eliminate if fanin occurs in the fanin list of the fanout exactly once
611 if ( Abc_NodeCheckDupFanin( pFanin, pFanout, &iFanin ) != 1 )
612 return NULL;
613 // find the new number of fanins after collapsing
614 nSize = Abc_NodeCollapseSuppSize( pFanin, pFanout, vFanins );
615 Hop_IthVar( pMan, nSize ); // use additional var for fanin variable
616 assert( nSize + 1 <= Hop_ManPiNum(pMan) );
617 // find the permutation after collapsing
618 RetValue = Abc_NodeCollapsePermMap( pFanin, NULL, vFanins, pPermFanin );
619 assert( RetValue );
620 RetValue = Abc_NodeCollapsePermMap( pFanout, pFanin, vFanins, pPermFanout );
621 assert( RetValue );
622 // include fanin's variable
623 pPermFanout[iFanin] = nSize;
624 // create new function of fanin and fanout
625 bFanin = Hop_Permute( pMan, (Hop_Obj_t *)pFanin->pData, Abc_ObjFaninNum(pFanin), pPermFanin );
626 bFanout = Hop_Permute( pMan, (Hop_Obj_t *)pFanout->pData, Abc_ObjFaninNum(pFanout), pPermFanout );
627 // compose fanin into fanout
628 return Hop_Compose( pMan, bFanout, bFanin, nSize );
629}
630int Abc_NodeCollapse1( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
631{
632 Abc_Obj_t * pFanoutNew, * pObj;
633 Hop_Obj_t * bFanoutNew;
634 int i;
635 assert( Abc_NtkIsAigLogic(pFanin->pNtk) );
636 assert( Abc_ObjIsNode(pFanin) );
637 assert( Abc_ObjIsNode(pFanout) );
638 bFanoutNew = Abc_NodeCollapseFunc1( pFanin, pFanout, vFanins, pPermFanin, pPermFanout );
639 if ( bFanoutNew == NULL )
640 return 0;
641 // create the new node
642 pFanoutNew = Abc_NtkCreateNode( pFanin->pNtk );
643 Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
644 Abc_ObjAddFanin( pFanoutNew, pObj );
645 pFanoutNew->pData = bFanoutNew;
646 // transfer the fanout
647 Abc_ObjTransferFanout( pFanout, pFanoutNew );
648 assert( Abc_ObjFanoutNum( pFanout ) == 0 );
649 Abc_NtkDeleteObj_rec( pFanout, 1 );
650 return 1;
651}
652int Abc_NodeIsExor( Abc_Obj_t * pNode )
653{
654 Hop_Man_t * pMan;
655 word Truth;
656 if ( Abc_ObjFaninNum(pNode) < 3 || Abc_ObjFaninNum(pNode) > 6 )
657 return 0;
658 pMan = (Hop_Man_t *)pNode->pNtk->pManFunc;
659 Truth = Hop_ManComputeTruth6( pMan, (Hop_Obj_t *)pNode->pData, Abc_ObjFaninNum(pNode) );
660 if ( Truth == 0x6666666666666666 || Truth == 0x9999999999999999 ||
661 Truth == 0x9696969696969696 || Truth == 0x6969696969696969 ||
662 Truth == 0x6996699669966996 || Truth == 0x9669966996699669 ||
663 Truth == 0x9669699696696996 || Truth == 0x6996966969969669 ||
664 Truth == 0x6996966996696996 || Truth == 0x9669699669969669 )
665 return 1;
666 return 0;
667}
668int Abc_NtkEliminate1One( Abc_Ntk_t * pNtk, int ElimValue, int nMaxSize, int fReverse, int fVerbose )
669{
670 Vec_Ptr_t * vFanouts, * vFanins, * vNodes;
671 Abc_Obj_t * pNode, * pFanout;
672 int * pPermFanin, * pPermFanout;
673 int RetValue, i, k;
674 assert( nMaxSize > 0 );
675 assert( Abc_NtkIsLogic(pNtk) );
676 // convert network to BDD representation
677 if ( !Abc_NtkToAig(pNtk) )
678 {
679 fprintf( stdout, "Converting to AIG has failed.\n" );
680 return 0;
681 }
682 // get the nodes in the given order
683 vNodes = fReverse? Abc_NtkDfsReverse( pNtk ) : Abc_NtkDfs( pNtk, 0 );
684 // go through the nodes and decide is they can be eliminated
685 pPermFanin = ABC_ALLOC( int, nMaxSize + 1000 );
686 pPermFanout = ABC_ALLOC( int, nMaxSize + 1000 );
687 vFanins = Vec_PtrAlloc( 1000 );
688 vFanouts = Vec_PtrAlloc( 1000 );
689 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
690 {
691 if ( !Abc_ObjIsNode(pNode) ) // skip deleted nodes
692 continue;
693 if ( Abc_NodeFindCoFanout(pNode) != NULL )
694 continue;
695 if ( Abc_ObjFaninNum(pNode) > nMaxSize )
696 continue;
697 if ( Abc_NodeIsExor(pNode) )
698 continue;
699 // skip nodes with more than one fanout
700// if ( Abc_ObjFanoutNum(pNode) != 1 )
701// continue;
702 // skip nodes that appear in the FF of their fanout more than once
703 if ( Abc_NodeCountAppearancesAll( pNode ) > ElimValue + 2 )
704 continue;
705 Abc_ObjForEachFanout( pNode, pFanout, k )
706 if ( Abc_NodeCollapseSuppSize(pNode, pFanout, vFanins) > nMaxSize )
707 break;
708 if ( k < Abc_ObjFanoutNum(pNode) )
709 continue;
710 // perform elimination
711 Abc_NodeCollectFanouts( pNode, vFanouts );
712 Vec_PtrForEachEntry( Abc_Obj_t *, vFanouts, pFanout, k )
713 {
714 if ( fVerbose )
715 printf( "Collapsing fanin %5d (supp =%2d) into fanout %5d (supp =%2d) ",
716 Abc_ObjId(pNode), Abc_ObjFaninNum(pNode), Abc_ObjId(pFanout), Abc_ObjFaninNum(pFanout) );
717 RetValue = Abc_NodeCollapse1( pNode, pFanout, vFanins, pPermFanin, pPermFanout );
718 assert( RetValue );
719 if ( fVerbose )
720 {
721 Abc_Obj_t * pNodeNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk) - 1 );
722 if ( pNodeNew )
723 printf( "resulting in node %5d (supp =%2d).\n", Abc_ObjId(pNodeNew), Abc_ObjFaninNum(pNodeNew) );
724 }
725 }
726 }
727 Vec_PtrFree( vFanins );
728 Vec_PtrFree( vFanouts );
729 Vec_PtrFree( vNodes );
730 ABC_FREE( pPermFanin );
731 ABC_FREE( pPermFanout );
732 return 1;
733}
734int Abc_NtkEliminate1( Abc_Ntk_t * pNtk, int ElimValue, int nMaxSize, int nIterMax, int fReverse, int fVerbose )
735{
736 int i;
737 for ( i = 0; i < nIterMax; i++ )
738 {
739 int nNodes = Abc_NtkNodeNum(pNtk);
740// printf( "%d ", nNodes );
741 if ( !Abc_NtkEliminate1One(pNtk, ElimValue, nMaxSize, fReverse, fVerbose) )
742 return 0;
743 if ( nNodes == Abc_NtkNodeNum(pNtk) )
744 break;
745 }
746 return 1;
747}
748
760int Abc_ObjCompareByNumber( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
761{
762 return Abc_ObjRegular(*pp1)->iTemp - Abc_ObjRegular(*pp2)->iTemp;
763}
764void Abc_ObjSortInReverseOrder( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
765{
766 Vec_Ptr_t * vOrder;
767 Abc_Obj_t * pNode;
768 int i;
769 vOrder = Abc_NtkDfsReverse( pNtk );
770 Vec_PtrForEachEntry( Abc_Obj_t *, vOrder, pNode, i )
771 pNode->iTemp = i;
772 Vec_PtrSort( vNodes, (int (*)(const void *, const void *))Abc_ObjCompareByNumber );
773 Vec_PtrForEachEntry( Abc_Obj_t *, vOrder, pNode, i )
774 pNode->iTemp = 0;
775 Vec_PtrFree( vOrder );
776}
777
778
790int Abc_NtkEliminateSpecial( Abc_Ntk_t * pNtk, int nMaxSize, int fVerbose )
791{
792 extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
793 Vec_Ptr_t * vFanouts, * vFanins, * vNodes;
794 Abc_Obj_t * pNode, * pFanout;
795 int * pPermFanin, * pPermFanout;
796 int RetValue, i, k;
797 assert( nMaxSize > 0 );
798 assert( Abc_NtkIsLogic(pNtk) );
799
800
801 // convert network to BDD representation
802 if ( !Abc_NtkToBdd(pNtk) )
803 {
804 fprintf( stdout, "Converting to BDD has failed.\n" );
805 return 0;
806 }
807
808 // prepare nodes for sweeping
809 //Abc_NtkRemoveDupFanins( pNtk );
810 Abc_NtkMinimumBase( pNtk );
811 Abc_NtkCleanup( pNtk, 0 );
812
813 // convert network to SOPs
814 if ( !Abc_NtkToSop(pNtk, -1, ABC_INFINITY) )
815 {
816 fprintf( stdout, "Converting to SOP has failed.\n" );
817 return 0;
818 }
819
820 // collect info about the nodes to be eliminated
821 vNodes = Vec_PtrAlloc( 1000 );
822 Abc_NtkForEachNode( pNtk, pNode, i )
823 {
824 if ( Abc_ObjFanoutNum(pNode) != 1 )
825 continue;
826 pFanout = Abc_ObjFanout0(pNode);
827 if ( !Abc_ObjIsNode(pFanout) )
828 continue;
829 if ( Abc_SopGetCubeNum((char *)pNode->pData) != 1 )
830 continue;
831 if ( Abc_SopGetCubeNum((char *)pFanout->pData) != 1 )
832 continue;
833 // find the fanout's fanin
834 RetValue = Abc_NodeFindFanin( pFanout, pNode );
835 assert( RetValue >= 0 && RetValue < Abc_ObjFaninNum(pFanout) );
836 // both pNode and pFanout are AND/OR type nodes
837 if ( Abc_SopIsComplement((char *)pNode->pData) == Abc_SopGetIthCareLit((char *)pFanout->pData, RetValue) )
838 continue;
839 Vec_PtrPush( vNodes, pNode );
840 }
841 if ( Vec_PtrSize(vNodes) == 0 )
842 {
843 Vec_PtrFree( vNodes );
844 return 1;
845 }
846 Abc_ObjSortInReverseOrder( pNtk, vNodes );
847
848 // convert network to BDD representation
849 if ( !Abc_NtkToBdd(pNtk) )
850 {
851 fprintf( stdout, "Converting to BDD has failed.\n" );
852 return 0;
853 }
854
855 // go through the nodes and decide is they can be eliminated
856 pPermFanin = ABC_ALLOC( int, nMaxSize + 1000 );
857 pPermFanout = ABC_ALLOC( int, nMaxSize + 1000 );
858 vFanins = Vec_PtrAlloc( 1000 );
859 vFanouts = Vec_PtrAlloc( 1000 );
860 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
861 {
862 assert( Abc_ObjIsNode(pNode) );
863 assert( Abc_NodeFindCoFanout(pNode) == NULL );
864 // perform elimination
865 Abc_NodeCollectFanouts( pNode, vFanouts );
866 Vec_PtrForEachEntry( Abc_Obj_t *, vFanouts, pFanout, k )
867 {
868 if ( fVerbose )
869 printf( "Collapsing fanin %5d (supp =%2d) into fanout %5d (supp =%2d) ",
870 Abc_ObjId(pNode), Abc_ObjFaninNum(pNode), Abc_ObjId(pFanout), Abc_ObjFaninNum(pFanout) );
871 RetValue = Abc_NodeCollapse( pNode, pFanout, vFanins, pPermFanin, pPermFanout );
872 assert( RetValue );
873 if ( fVerbose )
874 {
875 Abc_Obj_t * pNodeNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk) - 1 );
876 if ( pNodeNew )
877 printf( "resulting in node %5d (supp =%2d).\n", Abc_ObjId(pNodeNew), Abc_ObjFaninNum(pNodeNew) );
878 }
879 }
880 }
881 Abc_NtkBddReorder( pNtk, 0 );
882 Vec_PtrFree( vFanins );
883 Vec_PtrFree( vFanouts );
884 Vec_PtrFree( vNodes );
885 ABC_FREE( pPermFanin );
886 ABC_FREE( pPermFanout );
887 return 1;
888}
889
890#else
891
892int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk ) { return 0; }
893int Abc_NodeMinimumBase( Abc_Obj_t * pNode ) { return 0; }
894int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk ) { return 0; }
895int Abc_NtkEliminateSpecial( Abc_Ntk_t * pNtk, int nMaxSize, int fVerbose ) { return 0; }
896int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose ) { return 0; }
897int Abc_NtkEliminate1( Abc_Ntk_t * pNtk, int ElimValue, int nMaxSize, int nIterMax, int fReverse, int fVerbose ) { return 0; }
898
899#endif
900
904
905
906ABC_NAMESPACE_IMPL_END
907
Abc_NtkBddReorder
void Abc_NtkBddReorder(Abc_Ntk_t *pNtk, int fVerbose)
DECLARATIONS ///.
Definition abcReorder.c:107
Abc_NodeMinimumBase
int Abc_NodeMinimumBase(Abc_Obj_t *pNode)
Definition abcMinBase.c:893
Abc_NtkEliminate
int Abc_NtkEliminate(Abc_Ntk_t *pNtk, int nMaxSize, int fReverse, int fVerbose)
Definition abcMinBase.c:896
Abc_NtkRemoveDupFanins
int Abc_NtkRemoveDupFanins(Abc_Ntk_t *pNtk)
Definition abcMinBase.c:894
Abc_NtkEliminateSpecial
int Abc_NtkEliminateSpecial(Abc_Ntk_t *pNtk, int nMaxSize, int fVerbose)
Definition abcMinBase.c:895
Abc_NtkMinimumBase
ABC_NAMESPACE_IMPL_START int Abc_NtkMinimumBase(Abc_Ntk_t *pNtk)
DECLARATIONS ///.
Definition abcMinBase.c:892
Abc_NtkEliminate1
int Abc_NtkEliminate1(Abc_Ntk_t *pNtk, int ElimValue, int nMaxSize, int nIterMax, int fReverse, int fVerbose)
Definition abcMinBase.c:897
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition abcFanio.c:84
Abc_NtkCleanup
ABC_DLL int Abc_NtkCleanup(Abc_Ntk_t *pNtk, int fVerbose)
Definition abcSweep.c:478
Abc_NtkDfs
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
Definition abcDfs.c:82
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
Abc_NtkToBdd
ABC_DLL int Abc_NtkToBdd(Abc_Ntk_t *pNtk)
Definition abcFunc.c:1299
Abc_ObjForEachFanout
#define Abc_ObjForEachFanout(pObj, pFanout, i)
Definition abc.h:529
Abc_NtkDeleteObj_rec
ABC_DLL void Abc_NtkDeleteObj_rec(Abc_Obj_t *pObj, int fOnlyNodes)
Definition abcObj.c:278
Abc_NodeCollectFanouts
ABC_DLL void Abc_NodeCollectFanouts(Abc_Obj_t *pNode, Vec_Ptr_t *vNodes)
Definition abcUtil.c:1647
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NodeRemoveDupFanins
ABC_DLL int Abc_NodeRemoveDupFanins(Abc_Obj_t *pNode)
Abc_ObjTransferFanout
ABC_DLL void Abc_ObjTransferFanout(Abc_Obj_t *pObjOld, Abc_Obj_t *pObjNew)
Definition abcFanio.c:292
Abc_ObjDeleteFanin
ABC_DLL void Abc_ObjDeleteFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition abcFanio.c:111
Abc_NodeCollectFanins
ABC_DLL void Abc_NodeCollectFanins(Abc_Obj_t *pNode, Vec_Ptr_t *vNodes)
Definition abcUtil.c:1627
Abc_NtkToAig
ABC_DLL int Abc_NtkToAig(Abc_Ntk_t *pNtk)
Definition abcFunc.c:1333
Abc_SopGetIthCareLit
ABC_DLL int Abc_SopGetIthCareLit(char *pSop, int i)
Definition abcSop.c:626
Abc_NtkToSop
ABC_DLL int Abc_NtkToSop(Abc_Ntk_t *pNtk, int fMode, int nCubeLimit)
Definition abcFunc.c:1261
Abc_SopIsComplement
ABC_DLL int Abc_SopIsComplement(char *pSop)
Definition abcSop.c:703
Abc_NodeFindCoFanout
ABC_DLL Abc_Obj_t * Abc_NodeFindCoFanout(Abc_Obj_t *pNode)
Definition abcUtil.c:812
Abc_SopGetCubeNum
ABC_DLL int Abc_SopGetCubeNum(char *pSop)
Definition abcSop.c:537
Abc_NtkDfsReverse
ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverse(Abc_Ntk_t *pNtk)
Definition abcDfs.c:221
Abc_NodeFindFanin
ABC_DLL int Abc_NodeFindFanin(Abc_Obj_t *pNode, Abc_Obj_t *pFanin)
Definition abcUtil.c:791
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition abc.h:464
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
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
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Extra_bddRemapUp
DdNode * Extra_bddRemapUp(DdManager *dd, DdNode *bF)
Definition extraBddMisc.c:145
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
Hop_Compose
Hop_Obj_t * Hop_Compose(Hop_Man_t *p, Hop_Obj_t *pRoot, Hop_Obj_t *pFunc, int iVar)
Definition hopDfs.c:415
Hop_Permute
Hop_Obj_t * Hop_Permute(Hop_Man_t *p, Hop_Obj_t *pRoot, int nRootVars, int *pPermute)
Definition hopDfs.c:563
Hop_IthVar
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition hopOper.c:63
Hop_ObjFanoutCount
int Hop_ObjFanoutCount(Hop_Obj_t *pObj, Hop_Obj_t *pPivot)
Definition hopDfs.c:310
Hop_ManComputeTruth6
word Hop_ManComputeTruth6(Hop_Man_t *p, Hop_Obj_t *pObj, int nVars)
Definition hopTruth.c:256
Hop_Obj_t
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition abc.h:191
Abc_Obj_t_::pData
void * pData
Definition abc.h:145
Abc_Obj_t_::vFanins
Vec_Int_t vFanins
Definition abc.h:143
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition abc.h:130
Abc_Obj_t_::Id
int Id
Definition abc.h:132
Abc_Obj_t_::iTemp
int iTemp
Definition abc.h:149
Abc_Obj_t_::vFanouts
Vec_Int_t vFanouts
Definition abc.h:144
Vec_Str_t_::pArray
char * pArray
Definition bblif.c:51
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStop
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition vecInt.h:58
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