ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
abcLutmin.c
Go to the documentation of this file.
1
20
21#include "base/abc/abc.h"
22
23#ifdef ABC_USE_CUDD
24#include "bdd/extrab/extraBdd.h"
25#endif
26
27ABC_NAMESPACE_IMPL_START
28
29
30/*
31 Implememented here is the algorithm for minimal-LUT decomposition
32 described in the paper: T. Sasao et al. "On the number of LUTs
33 to implement logic functions", To appear in Proc. IWLS'09.
34*/
35
39
43
44#ifdef ABC_USE_CUDD
45
57int Abc_ObjCheckAbsorb( Abc_Obj_t * pObj, Abc_Obj_t * pPivot, int nLutSize, Vec_Ptr_t * vFanins )
58{
59 Abc_Obj_t * pFanin;
60 int i;
61 assert( Abc_ObjIsNode(pObj) && Abc_ObjIsNode(pPivot) );
62 // add fanins of the node
63 Vec_PtrClear( vFanins );
64 Abc_ObjForEachFanin( pObj, pFanin, i )
65 if ( pFanin != pPivot )
66 Vec_PtrPush( vFanins, pFanin );
67 // add fanins of the fanin
68 Abc_ObjForEachFanin( pPivot, pFanin, i )
69 {
70 Vec_PtrPushUnique( vFanins, pFanin );
71 if ( Vec_PtrSize(vFanins) > nLutSize )
72 return 0;
73 }
74 return 1;
75}
76
88void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize )
89{
90 Vec_Int_t * vCounts;
91 Vec_Ptr_t * vFanins;
92 Abc_Obj_t * pObj, * pFanin;
93 int i, k, Counter = 0, Counter2 = 0;
94 abctime clk = Abc_Clock();
95 vCounts = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
96 vFanins = Vec_PtrAlloc( 100 );
97 Abc_NtkForEachNode( pNtk, pObj, i )
98 Abc_ObjForEachFanin( pObj, pFanin, k )
99 if ( Abc_ObjIsNode(pFanin) && Abc_ObjCheckAbsorb( pObj, pFanin, nLutSize, vFanins ) )
100 {
101 Vec_IntAddToEntry( vCounts, Abc_ObjId(pFanin), 1 );
102 Counter++;
103 }
104 Vec_PtrFree( vFanins );
105 Abc_NtkForEachNode( pNtk, pObj, i )
106 if ( Vec_IntEntry(vCounts, Abc_ObjId(pObj)) == Abc_ObjFanoutNum(pObj) )
107 {
108// printf( "%d ", Abc_ObjId(pObj) );
109 Counter2++;
110 }
111 printf( "Absorted = %6d. (%6.2f %%) Fully = %6d. (%6.2f %%) ",
112 Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk),
113 Counter2, 100.0 * Counter2 / Abc_NtkNodeNum(pNtk) );
114 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
115 Vec_IntFree( vCounts );
116}
117
129Abc_Obj_t * Abc_NtkBddMux21( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanins[] )
130{
131 DdManager * dd = (DdManager *)pNtkNew->pManFunc;
132 Abc_Obj_t * pNode;
133 DdNode * bSpin, * bCof0, * bCof1;
134 pNode = Abc_NtkCreateNode( pNtkNew );
135 Abc_ObjAddFanin( pNode, pFanins[0] );
136 Abc_ObjAddFanin( pNode, pFanins[1] );
137 Abc_ObjAddFanin( pNode, pFanins[2] );
138 bSpin = Cudd_bddIthVar(dd, 0);
139 bCof0 = Cudd_bddIthVar(dd, 1);
140 bCof1 = Cudd_bddIthVar(dd, 2);
141 pNode->pData = Cudd_bddIte( dd, bSpin, bCof1, bCof0 ); Cudd_Ref( (DdNode *)pNode->pData );
142 return pNode;
143}
144
156Abc_Obj_t * Abc_NtkBddMux411( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanins[] )
157{
158 DdManager * dd = (DdManager *)pNtkNew->pManFunc;
159 Abc_Obj_t * pNode;
160 DdNode * bSpin, * bCof0, * bCof1;
161 pNode = Abc_NtkCreateNode( pNtkNew );
162 Abc_ObjAddFanin( pNode, pFanins[0] );
163 Abc_ObjAddFanin( pNode, pFanins[1] );
164 Abc_ObjAddFanin( pNode, pFanins[2] );
165 Abc_ObjAddFanin( pNode, pFanins[3] );
166 Abc_ObjAddFanin( pNode, pFanins[4] );
167 Abc_ObjAddFanin( pNode, pFanins[5] );
168 bSpin = Cudd_bddIthVar(dd, 1);
169 bCof0 = Cudd_bddIte( dd, bSpin, Cudd_bddIthVar(dd, 3), Cudd_bddIthVar(dd, 2) ); Cudd_Ref( bCof0 );
170 bCof1 = Cudd_bddIte( dd, bSpin, Cudd_bddIthVar(dd, 5), Cudd_bddIthVar(dd, 4) ); Cudd_Ref( bCof1 );
171 bSpin = Cudd_bddIthVar(dd, 0);
172 pNode->pData = Cudd_bddIte( dd, bSpin, bCof1, bCof0 ); Cudd_Ref( (DdNode *)pNode->pData );
173 Cudd_RecursiveDeref( dd, bCof0 );
174 Cudd_RecursiveDeref( dd, bCof1 );
175 return pNode;
176}
177
189Abc_Obj_t * Abc_NtkBddMux412( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanins[] )
190{
191 DdManager * dd = (DdManager *)pNtkNew->pManFunc;
192 Abc_Obj_t * pNodeBot, * pNodeTop;
193 DdNode * bSpin, * bCof0, * bCof1;
194 // bottom node
195 pNodeBot = Abc_NtkCreateNode( pNtkNew );
196 Abc_ObjAddFanin( pNodeBot, pFanins[0] );
197 Abc_ObjAddFanin( pNodeBot, pFanins[1] );
198 Abc_ObjAddFanin( pNodeBot, pFanins[2] );
199 Abc_ObjAddFanin( pNodeBot, pFanins[3] );
200 bSpin = Cudd_bddIthVar(dd, 0);
201 bCof0 = Cudd_bddIte( dd, Cudd_bddIthVar(dd, 1), Cudd_bddIthVar(dd, 3), Cudd_bddIthVar(dd, 2) ); Cudd_Ref( bCof0 );
202 bCof1 = Cudd_bddIthVar(dd, 1);
203 pNodeBot->pData = Cudd_bddIte( dd, bSpin, bCof1, bCof0 ); Cudd_Ref( (DdNode *)pNodeBot->pData );
204 Cudd_RecursiveDeref( dd, bCof0 );
205 // top node
206 pNodeTop = Abc_NtkCreateNode( pNtkNew );
207 Abc_ObjAddFanin( pNodeTop, pFanins[0] );
208 Abc_ObjAddFanin( pNodeTop, pNodeBot );
209 Abc_ObjAddFanin( pNodeTop, pFanins[4] );
210 Abc_ObjAddFanin( pNodeTop, pFanins[5] );
211 bSpin = Cudd_bddIthVar(dd, 0);
212 bCof0 = Cudd_bddIthVar(dd, 1);
213 bCof1 = Cudd_bddIte( dd, Cudd_bddIthVar(dd, 1), Cudd_bddIthVar(dd, 3), Cudd_bddIthVar(dd, 2) ); Cudd_Ref( bCof1 );
214 pNodeTop->pData = Cudd_bddIte( dd, bSpin, bCof1, bCof0 ); Cudd_Ref( (DdNode *)pNodeTop->pData );
215 Cudd_RecursiveDeref( dd, bCof1 );
216 return pNodeTop;
217}
218
230Abc_Obj_t * Abc_NtkBddMux412a( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanins[] )
231{
232 DdManager * dd = (DdManager *)pNtkNew->pManFunc;
233 Abc_Obj_t * pNodeBot, * pNodeTop;
234 DdNode * bSpin, * bCof0, * bCof1;
235 // bottom node
236 pNodeBot = Abc_NtkCreateNode( pNtkNew );
237 Abc_ObjAddFanin( pNodeBot, pFanins[1] );
238 Abc_ObjAddFanin( pNodeBot, pFanins[2] );
239 Abc_ObjAddFanin( pNodeBot, pFanins[3] );
240 bSpin = Cudd_bddIthVar(dd, 0);
241 bCof0 = Cudd_bddIthVar(dd, 1);
242 bCof1 = Cudd_bddIthVar(dd, 2);
243 pNodeBot->pData = Cudd_bddIte( dd, bSpin, bCof1, bCof0 ); Cudd_Ref( (DdNode *)pNodeBot->pData );
244 // top node
245 pNodeTop = Abc_NtkCreateNode( pNtkNew );
246 Abc_ObjAddFanin( pNodeTop, pFanins[0] );
247 Abc_ObjAddFanin( pNodeTop, pFanins[1] );
248 Abc_ObjAddFanin( pNodeTop, pNodeBot );
249 Abc_ObjAddFanin( pNodeTop, pFanins[4] );
250 Abc_ObjAddFanin( pNodeTop, pFanins[5] );
251 bSpin = Cudd_bddIthVar(dd, 0);
252 bCof0 = Cudd_bddIthVar(dd, 2);
253 bCof1 = Cudd_bddIte( dd, Cudd_bddIthVar(dd, 1), Cudd_bddIthVar(dd, 4), Cudd_bddIthVar(dd, 3) ); Cudd_Ref( bCof1 );
254 pNodeTop->pData = Cudd_bddIte( dd, bSpin, bCof1, bCof0 ); Cudd_Ref( (DdNode *)pNodeTop->pData );
255 Cudd_RecursiveDeref( dd, bCof1 );
256 return pNodeTop;
257}
258
270Abc_Obj_t * Abc_NtkBddMux413( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanins[] )
271{
272 Abc_Obj_t * pNodesBot[3], * pNodesTop[3];
273 // left bottom
274 pNodesBot[0] = pFanins[1];
275 pNodesBot[1] = pFanins[2];
276 pNodesBot[2] = pFanins[3];
277 pNodesTop[1] = Abc_NtkBddMux21( pNtkNew, pNodesBot );
278 // right bottom
279 pNodesBot[0] = pFanins[1];
280 pNodesBot[1] = pFanins[4];
281 pNodesBot[2] = pFanins[5];
282 pNodesTop[2] = Abc_NtkBddMux21( pNtkNew, pNodesBot );
283 // top node
284 pNodesTop[0] = pFanins[0];
285 return Abc_NtkBddMux21( pNtkNew, pNodesTop );
286}
287
299DdNode * Abc_NtkBddCofactors_rec( DdManager * dd, DdNode * bNode, int iCof, int iLevel, int nLevels )
300{
301 DdNode * bNode0, * bNode1;
302 if ( Cudd_IsConstant(bNode) || iLevel == nLevels )
303 return bNode;
304 if ( Cudd_ReadPerm( dd, Cudd_NodeReadIndex(bNode) ) > iLevel )
305 {
306 bNode0 = bNode;
307 bNode1 = bNode;
308 }
309 else if ( Cudd_IsComplement(bNode) )
310 {
311 bNode0 = Cudd_Not(cuddE(Cudd_Regular(bNode)));
312 bNode1 = Cudd_Not(cuddT(Cudd_Regular(bNode)));
313 }
314 else
315 {
316 bNode0 = cuddE(bNode);
317 bNode1 = cuddT(bNode);
318 }
319 if ( (iCof >> (nLevels-1-iLevel)) & 1 )
320 return Abc_NtkBddCofactors_rec( dd, bNode1, iCof, iLevel + 1, nLevels );
321 return Abc_NtkBddCofactors_rec( dd, bNode0, iCof, iLevel + 1, nLevels );
322}
323
335Vec_Ptr_t * Abc_NtkBddCofactors( DdManager * dd, DdNode * bNode, int Level )
336{
337 Vec_Ptr_t * vCofs;
338 int i, nCofs = (1<<Level);
339 assert( Level > 0 && Level < 10 );
340 vCofs = Vec_PtrAlloc( 8 );
341 for ( i = 0; i < nCofs; i++ )
342 Vec_PtrPush( vCofs, Abc_NtkBddCofactors_rec( dd, bNode, i, 0, Level ) );
343 return vCofs;
344}
345
357static int Vec_PtrSortCompare( void ** pp1, void ** pp2 )
358{
359 if ( *pp1 < *pp2 )
360 return -1;
361 if ( *pp1 > *pp2 )
362 return 1;
363 return 0;
364}
365
377Abc_Obj_t * Abc_NtkCreateCofLut( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bCof, Abc_Obj_t * pNode, int Level )
378{
379 int fVerbose = 0;
380 DdNode * bFuncNew;
381 Abc_Obj_t * pNodeNew;
382 int i;
383 assert( Abc_ObjFaninNum(pNode) > Level );
384 // create a new node
385 pNodeNew = Abc_NtkCreateNode( pNtkNew );
386 // add the fanins in the order, in which they appear in the reordered manager
387 for ( i = Level; i < Abc_ObjFaninNum(pNode); i++ )
388 Abc_ObjAddFanin( pNodeNew, Abc_ObjFanin(pNode, i)->pCopy );
389if ( fVerbose )
390{
391Extra_bddPrint( dd, bCof );
392printf( "\n" );
393printf( "\n" );
394}
395 // transfer the function
396 bFuncNew = Extra_bddMove( dd, bCof, -Level ); Cudd_Ref( bFuncNew );
397if ( fVerbose )
398{
399Extra_bddPrint( dd, bFuncNew );
400printf( "\n" );
401printf( "\n" );
402}
403 pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFuncNew ); Cudd_Ref( (DdNode *)pNodeNew->pData );
404//Extra_bddPrint( pNtkNew->pManFunc, pNodeNew->pData );
405//printf( "\n" );
406//printf( "\n" );
407 Cudd_RecursiveDeref( dd, bFuncNew );
408 return pNodeNew;
409}
410
422Abc_Obj_t * Abc_NtkBddCurtis( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vCofs, Vec_Ptr_t * vUniq )
423{
424 DdManager * ddOld = (DdManager *)pNode->pNtk->pManFunc;
425 DdManager * ddNew = (DdManager *)pNtkNew->pManFunc;
426 DdNode * bCof, * bUniq, * bMint, * bTemp, * bFunc, * bBits[10], ** pbCodeVars;
427 Abc_Obj_t * pNodeNew = NULL, * pNodeBS[10];
428 int nLutSize = Abc_Base2Log( Vec_PtrSize(vCofs) );
429 int nBits = Abc_Base2Log( Vec_PtrSize(vUniq) );
430 int b, c, u, i;
431 assert( nBits + 2 <= nLutSize );
432 assert( nLutSize < Abc_ObjFaninNum(pNode) );
433 // start BDDs for the decomposed blocks
434 for ( b = 0; b < nBits; b++ )
435 bBits[b] = Cudd_ReadLogicZero(ddNew), Cudd_Ref( bBits[b] );
436 // add each bound set minterm to one of the blocks
437 Vec_PtrForEachEntry( DdNode *, vCofs, bCof, c )
438 {
439 Vec_PtrForEachEntry( DdNode *, vUniq, bUniq, u )
440 if ( bUniq == bCof )
441 break;
442 assert( u < Vec_PtrSize(vUniq) );
443 for ( b = 0; b < nBits; b++ )
444 {
445 if ( ((u >> b) & 1) == 0 )
446 continue;
447 bMint = Extra_bddBitsToCube( ddNew, c, nLutSize, ddNew->vars, 1 ); Cudd_Ref( bMint );
448 bBits[b] = Cudd_bddOr( ddNew, bTemp = bBits[b], bMint ); Cudd_Ref( bBits[b] );
449 Cudd_RecursiveDeref( ddNew, bTemp );
450 Cudd_RecursiveDeref( ddNew, bMint );
451 }
452 }
453 // create bound set nodes
454 for ( b = 0; b < nBits; b++ )
455 {
456 pNodeBS[b] = Abc_NtkCreateNode( pNtkNew );
457 for ( i = 0; i < nLutSize; i++ )
458 Abc_ObjAddFanin( pNodeBS[b], Abc_ObjFanin(pNode, i)->pCopy );
459 pNodeBS[b]->pData = bBits[b]; // takes ref
460 }
461 // create composition node
462 pNodeNew = Abc_NtkCreateNode( pNtkNew );
463 // add free set variables first
464 for ( i = nLutSize; i < Abc_ObjFaninNum(pNode); i++ )
465 Abc_ObjAddFanin( pNodeNew, Abc_ObjFanin(pNode, i)->pCopy );
466 // add code bit variables next
467 for ( b = 0; b < nBits; b++ )
468 Abc_ObjAddFanin( pNodeNew, pNodeBS[b] );
469 // derive function of the composition node
470 bFunc = Cudd_ReadLogicZero(ddNew); Cudd_Ref( bFunc );
471 pbCodeVars = ddNew->vars + Abc_ObjFaninNum(pNode) - nLutSize;
472 Vec_PtrForEachEntry( DdNode *, vUniq, bUniq, u )
473 {
474 bUniq = Extra_bddMove( ddOld, bUniq, -nLutSize ); Cudd_Ref( bUniq );
475 bUniq = Extra_TransferLevelByLevel( ddOld, ddNew, bTemp = bUniq ); Cudd_Ref( bUniq );
476 Cudd_RecursiveDeref( ddOld, bTemp );
477
478 bMint = Extra_bddBitsToCube( ddNew, u, nBits, pbCodeVars, 0 ); Cudd_Ref( bMint );
479 bMint = Cudd_bddAnd( ddNew, bTemp = bMint, bUniq ); Cudd_Ref( bMint );
480 Cudd_RecursiveDeref( ddNew, bTemp );
481 Cudd_RecursiveDeref( ddNew, bUniq );
482
483 bFunc = Cudd_bddOr( ddNew, bTemp = bFunc, bMint ); Cudd_Ref( bFunc );
484 Cudd_RecursiveDeref( ddNew, bTemp );
485 Cudd_RecursiveDeref( ddNew, bMint );
486 }
487 pNodeNew->pData = bFunc; // takes ref
488 return pNodeNew;
489}
490
502Abc_Obj_t * Abc_NtkBddFindCofactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int nLutSize )
503{
504 Abc_Obj_t * pNodeBot, * pNodeTop;
505 DdManager * ddOld = (DdManager *)pNode->pNtk->pManFunc;
506 DdManager * ddNew = (DdManager *)pNtkNew->pManFunc;
507 DdNode * bCof0 = NULL, * bCof1 = NULL, * bSupp, * bTemp, * bVar;
508 DdNode * bCof0n, * bCof1n;
509 int i, iCof, iFreeVar, fCof1Smaller = -1;
510 assert( Abc_ObjFaninNum(pNode) == nLutSize + 1 );
511 for ( iCof = 0; iCof < Abc_ObjFaninNum(pNode); iCof++ )
512 {
513 bVar = Cudd_bddIthVar( ddOld, iCof );
514 bCof0 = Cudd_Cofactor( ddOld, (DdNode *)pNode->pData, Cudd_Not(bVar) ); Cudd_Ref( bCof0 );
515 bCof1 = Cudd_Cofactor( ddOld, (DdNode *)pNode->pData, bVar ); Cudd_Ref( bCof1 );
516 if ( Cudd_SupportSize( ddOld, bCof0 ) <= nLutSize - 2 )
517 {
518 fCof1Smaller = 0;
519 break;
520 }
521 if ( Cudd_SupportSize( ddOld, bCof1 ) <= nLutSize - 2 )
522 {
523 fCof1Smaller = 1;
524 break;
525 }
526 Cudd_RecursiveDeref( ddOld, bCof0 );
527 Cudd_RecursiveDeref( ddOld, bCof1 );
528 }
529 if ( iCof == Abc_ObjFaninNum(pNode) )
530 return NULL;
531 // find unused variable
532 bSupp = Cudd_Support( ddOld, fCof1Smaller? bCof1 : bCof0 ); Cudd_Ref( bSupp );
533 iFreeVar = -1;
534 for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
535 {
536 assert( i == Cudd_ReadPerm(ddOld, i) );
537 if ( i == iCof )
538 continue;
539 for ( bTemp = bSupp; !Cudd_IsConstant(bTemp); bTemp = cuddT(bTemp) )
540 if ( i == (int)Cudd_NodeReadIndex(bTemp) )
541 break;
542 if ( Cudd_IsConstant(bTemp) )
543 {
544 iFreeVar = i;
545 break;
546 }
547 }
548 assert( iFreeVar != iCof && iFreeVar < Abc_ObjFaninNum(pNode) );
549 Cudd_RecursiveDeref( ddOld, bSupp );
550 // transfer the cofactors
551 bCof0n = Extra_TransferLevelByLevel( ddOld, ddNew, bCof0 ); Cudd_Ref( bCof0n );
552 bCof1n = Extra_TransferLevelByLevel( ddOld, ddNew, bCof1 ); Cudd_Ref( bCof1n );
553 Cudd_RecursiveDeref( ddOld, bCof0 );
554 Cudd_RecursiveDeref( ddOld, bCof1 );
555 // create bottom node
556 pNodeBot = Abc_NtkCreateNode( pNtkNew );
557 for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
558 Abc_ObjAddFanin( pNodeBot, Abc_ObjFanin(pNode, i)->pCopy );
559 pNodeBot->pData = fCof1Smaller? bCof0n : bCof1n;
560 // create top node
561 pNodeTop = Abc_NtkCreateNode( pNtkNew );
562 for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
563 if ( i == iFreeVar )
564 Abc_ObjAddFanin( pNodeTop, pNodeBot );
565 else
566 Abc_ObjAddFanin( pNodeTop, Abc_ObjFanin(pNode, i)->pCopy );
567 // derive the new function
568 pNodeTop->pData = Cudd_bddIte( ddNew,
569 Cudd_bddIthVar(ddNew, iCof),
570 fCof1Smaller? bCof1n : Cudd_bddIthVar(ddNew, iFreeVar),
571 fCof1Smaller? Cudd_bddIthVar(ddNew, iFreeVar) : bCof0n );
572 Cudd_Ref( (DdNode *)pNodeTop->pData );
573 Cudd_RecursiveDeref( ddNew, fCof1Smaller? bCof1n : bCof0n );
574 return pNodeTop;
575}
576
577
589int Abc_NtkBddNodeCompareByLevel( DdNode ** pp1, DdNode ** pp2 )
590{
591 return (*pp1)->Id - (*pp2)->Id;
592}
593Vec_Ptr_t * Abc_NtkBddCollectByLevel( DdManager * dd, DdNode * aFunc )
594{
595 DdGen *gen; DdNode *node; int i;
596 Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 );
597 Cudd_ForeachNode( dd, aFunc, gen, node )
598 Vec_PtrPush( vNodes, node ), node->Id = Cudd_ReadPerm( dd, (int)node->index );
599 Vec_PtrSort( vNodes, (int (*)(const void *, const void *))Abc_NtkBddNodeCompareByLevel );
600 Vec_PtrForEachEntry( DdNode *, vNodes, node, i )
601 node->Id = i;
602 return vNodes;
603}
604void Abc_NtkBddCollectPrint3( DdManager * dd, DdNode * aFunc )
605{
606 Vec_Ptr_t * vNodes = Abc_NtkBddCollectByLevel( dd, aFunc );
607 Vec_PtrPrintPointers( vNodes );
608 Vec_PtrFree( vNodes );
609}
610
622
623Vec_Ptr_t * Abc_NtkBddFetchNodes( DdManager * dd, DdNode * aFunc )
624{
625 Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 );
626 DdGen *gen; DdNode *node;
627 Cudd_ForeachNode( dd, aFunc, gen, node)
628 Vec_PtrPush(vNodes, node), node->Id = 0;
629 return vNodes;
630}
631void Abc_NtkBddCleanNodes( DdManager * dd, DdNode * aFunc )
632{
633 DdGen *gen; DdNode *node;
634 Cudd_ForeachNode( dd, aFunc, gen, node)
635 node->Id = 0;
636}
637void Abc_NtkBddCollectPtr_rec( DdManager * dd, DdNode * aFunc, Vec_Ptr_t * vNodes )
638{
639 if ( aFunc->Id )
640 return;
641 if ( !cuddIsConstant(aFunc) ) {
642 Abc_NtkBddCollectPtr_rec( dd, cuddE(aFunc), vNodes );
643 Abc_NtkBddCollectPtr_rec( dd, cuddT(aFunc), vNodes );
644 }
645 aFunc->Id = Vec_PtrSize(vNodes) + 1;
646 Vec_PtrPush(vNodes, aFunc);
647}
648Vec_Ptr_t * Abc_NtkBddCollectPtr( DdManager * dd, DdNode * aFunc )
649{
650 Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 );
651 Abc_NtkBddCleanNodes( dd, aFunc );
652 Abc_NtkBddCollectPtr_rec( dd, aFunc, vNodes );
653 return vNodes;
654}
655void Abc_NtkBddCollectPrint2( DdManager * dd, DdNode * aFunc )
656{
657 Vec_Ptr_t * vNodes = Abc_NtkBddCollectPtr( dd, aFunc );
658 Vec_PtrPrintPointers( vNodes );
659 Vec_PtrFree( vNodes );
660}
661
673
674static inline word Abc_Bdd2Word( DdNode * f ) { union { DdNode * f; word w; } v; v.f = f; return v.w; }
675static inline DdNode * Abc_Word2Bdd( word w ) { union { DdNode * f; word w; } v; v.w = w; return v.f; }
676
677static inline int Abc_Bdd2Int( DdNode * F, DdNode * f ) { return (int)(Abc_Bdd2Word(F) ^ Abc_Bdd2Word(f)) >> 3; }
678static inline DdNode * Abc_Int2Bdd( DdNode * F, int diff ) { return Abc_Word2Bdd(Abc_Bdd2Word(F) ^ (word)(diff << 3)); }
679
680static inline int Abc_BddIndex( DdManager * dd, DdNode * f ) { return cuddIsConstant(f) ? dd->size : (int)f->index; }
681static inline int Abc_BddLevel( DdManager * dd, DdNode * f ) { return cuddIsConstant(f) ? dd->size : Cudd_ReadPerm(dd, (int)f->index); }
682
683void Abc_NtkBddCollectInt_rec( DdManager * dd, DdNode * aRef, DdNode * aFunc, Vec_Wec_t * vNodes )
684{
685 if ( Cudd_IsComplement(aFunc->next) )
686 return;
687 aFunc->next = Cudd_Not(aFunc->next);
688 if ( !cuddIsConstant(aFunc) ) {
689 Abc_NtkBddCollectInt_rec( dd, aRef, cuddE(aFunc), vNodes );
690 Abc_NtkBddCollectInt_rec( dd, aRef, cuddT(aFunc), vNodes );
691 }
692 //assert( Abc_Bdd2Int(aRef, aFunc) % 8 == 0 );
693 Vec_WecPush( vNodes, Abc_BddLevel(dd, aFunc), Abc_Bdd2Int(aRef, aFunc) );
694}
695Vec_Wec_t * Abc_NtkBddCollectInt( DdManager * dd, DdNode * aFunc )
696{
697 Vec_Wec_t * vNodes = Vec_WecStart( dd->size+1 );
698 Abc_NtkBddCollectInt_rec( dd, aFunc, aFunc, vNodes );
699 extern void ddClearFlag2( DdNode * f );
700 ddClearFlag2( aFunc );
701 return vNodes;
702}
703void Abc_NtkBddCollectPrint( DdManager * dd, DdNode * aFunc )
704{
705 Vec_Wec_t * vNodes = Abc_NtkBddCollectInt( dd, aFunc );
706 Vec_WecPrint( vNodes, 0 );
707 Vec_WecFree( vNodes );
708}
709
721Vec_Int_t * Abc_NtkBddCollectHighest( DdManager * dd, DdNode * aFunc, Vec_Wec_t * vNodes )
722{
723 Vec_Int_t * vRes = Vec_IntStartFull( Vec_WecMaxEntry(vNodes)+1 );
724 Vec_Int_t * vLevel; int i, k, Obj, * pEntry;
725 Vec_WecForEachLevelStop( vNodes, vLevel, i, dd->size )
726 Vec_IntForEachEntry( vLevel, Obj, k ) {
727 DdNode * aNode = Abc_Int2Bdd(aFunc, Obj);
728 pEntry = Vec_IntEntryP( vRes, Abc_Bdd2Int(aFunc, cuddE(aNode)) );
729 if ( *pEntry == -1 ) *pEntry = i;
730 pEntry = Vec_IntEntryP( vRes, Abc_Bdd2Int(aFunc, cuddT(aNode)) );
731 if ( *pEntry == -1 ) *pEntry = i;
732 }
733 return vRes;
734}
735void Abc_NtkBddCollectProfile( DdManager * dd, DdNode * aFunc, Vec_Wec_t * vNodes, int * pProf )
736{
737 memset( pProf, 0, sizeof(int)*(dd->size+1) );
738 Vec_Int_t * vHighest = Abc_NtkBddCollectHighest( dd, aFunc, vNodes );
739 Vec_Int_t * vLevel; int i, k, Obj;
740 pProf[0] = 1;
741 Vec_WecForEachLevelStart( vNodes, vLevel, i, 1 )
742 Vec_IntForEachEntry( vLevel, Obj, k ) {
743 int lev, Start = Vec_IntEntry( vHighest, Obj );
744 for ( lev = Start+1; lev <= i; lev++ )
745 pProf[lev]++;
746 }
747 printf( " Size = %5d ", Vec_IntSize(vHighest) );
748 Vec_IntFree( vHighest );
749}
750void Abc_NtkBddTestProfile( DdManager * dd, DdNode * aFunc )
751{
752 Vec_Wec_t * vNodes = Abc_NtkBddCollectInt( dd, aFunc );
753 int i, Total = 0, Profile[100]; assert( dd->size < 100 );
754 Abc_NtkBddCollectProfile( dd, aFunc, vNodes, Profile );
755 printf( " " );
756 for ( i = 0; i <= dd->size; i++ )
757 printf( "%3d", Profile[i] ), Total += Profile[i];
758 printf( " Total = %d\n", Total );
759 Vec_WecFree( vNodes );
760}
761Vec_Wec_t * Abc_NtkBddCollectCofs( DdManager * dd, DdNode * aFunc, Vec_Wec_t * vNodes )
762{
763 Vec_Wec_t * vCofs = Vec_WecStart( dd->size+1 );
764 Vec_Int_t * vHighest = Abc_NtkBddCollectHighest( dd, aFunc, vNodes );
765 Vec_Int_t * vLevel; int i, k, Obj;
766 Vec_WecPush( vCofs, 0, 0 );
767 Vec_WecForEachLevelStart( vNodes, vLevel, i, 1 )
768 Vec_IntForEachEntry( vLevel, Obj, k ) {
769 int lev, Start = Vec_IntEntry( vHighest, Obj );
770 for ( lev = Start+1; lev <= i; lev++ )
771 Vec_WecPush( vCofs, lev, Obj );
772 }
773 Vec_IntFree( vHighest );
774 return vCofs;
775}
776Vec_Wec_t * Abc_NtkBddCollecInfo1( DdManager * dd, DdNode * aFunc )
777{
778 Vec_Wec_t * vInfo = Vec_WecStart( dd->size );
779 Vec_Wec_t * vNodes = Abc_NtkBddCollectInt( dd, aFunc );
780 Vec_Wec_t * vCofs = Abc_NtkBddCollectCofs( dd, aFunc, vNodes );
781 Vec_Int_t * vLevel; int i, k, Obj;
782 for ( int a = 0; a < dd->size; a++ ) {
783 word Sign = (word)1 << a;
784 for ( int n = 0; n < 2; n++ ) {
785 word Value = (word)n << a;
786 Vec_WecForEachLevel( vNodes, vLevel, i )
787 Vec_IntForEachEntry( vLevel, Obj, k )
788 Abc_Int2Bdd(aFunc, Obj)->Id = 0;
789 aFunc->Id = 1;
790 //printf( " %c %d : ", 'a'+a, n );
791 //printf( " %2d", 1 );
792 if ( n == 0 )
793 Vec_IntPush( Vec_WecEntry(vInfo, a), 1 );
794 Vec_WecForEachLevelStop( vNodes, vLevel, i, dd->size ) {
795 Vec_IntForEachEntry( vLevel, Obj, k ) {
796 DdNode * aNode = Abc_Int2Bdd(aFunc, Obj);
797 if ( aNode->Id == 0 )
798 continue;
799 if ( !((Sign >> i) & 1) || ((Value >> i) & 1) == 0 )
800 cuddE(aNode)->Id |= 1;
801 if ( !((Sign >> i) & 1) || ((Value >> i) & 1) == 1 )
802 cuddT(aNode)->Id |= 1;
803 }
804 Vec_Int_t * vCof = Vec_WecEntry(vCofs, i+1);
805 int Counter = 0;
806 Vec_IntForEachEntry( vCof, Obj, k )
807 Counter += (int)Abc_Int2Bdd(aFunc, Obj)->Id;
808 if ( n == 0 )
809 Vec_IntPush( Vec_WecEntry(vInfo, a), Counter );
810 else {
811 int * pEntry = Vec_IntEntryP( Vec_WecEntry(vInfo, a), i+1 );
812 *pEntry = Abc_MaxInt( *pEntry, Counter );
813 }
814 //printf( " %2d", Counter );
815 }
816 //printf( "\n" );
817 }
818 }
819 Vec_WecFree( vCofs );
820 Vec_WecFree( vNodes );
821 return vInfo;
822}
823Vec_Wec_t * Abc_NtkBddCollecInfo2( DdManager * dd, DdNode * aFunc )
824{
825 Vec_Wec_t * vInfo = Vec_WecStart( dd->size*(dd->size-1)/2 );
826 Vec_Wec_t * vNodes = Abc_NtkBddCollectInt( dd, aFunc );
827 Vec_Wec_t * vCofs = Abc_NtkBddCollectCofs( dd, aFunc, vNodes );
828 Vec_Int_t * vLevel; int i, k, Obj, c = 0;
829 for ( int a = 0; a < dd->size; a++ )
830 for ( int b = a+1; b < dd->size; b++ ) {
831 Vec_Int_t * vInfo1 = Vec_WecEntry(vInfo, c++);
832 word Sign = ((word)1 << a) | ((word)1 << b);
833 for ( int n = 0; n < 4; n++ ) {
834 word Value = ((word)(n & 1) << a) | ((word)((n >> 1) & 1) << b);
835 Vec_WecForEachLevel( vNodes, vLevel, i )
836 Vec_IntForEachEntry( vLevel, Obj, k )
837 Abc_Int2Bdd(aFunc, Obj)->Id = 0;
838 aFunc->Id = 1;
839 if ( n == 0 )
840 Vec_IntPush( vInfo1, 1 );
841 Vec_WecForEachLevelStop( vNodes, vLevel, i, dd->size ) {
842 Vec_IntForEachEntry( vLevel, Obj, k ) {
843 DdNode * aNode = Abc_Int2Bdd(aFunc, Obj);
844 if ( aNode->Id == 0 )
845 continue;
846 if ( !((Sign >> i) & 1) || ((Value >> i) & 1) == 0 )
847 cuddE(aNode)->Id |= 1;
848 if ( !((Sign >> i) & 1) || ((Value >> i) & 1) == 1 )
849 cuddT(aNode)->Id |= 1;
850 }
851 Vec_Int_t * vCof = Vec_WecEntry(vCofs, i+1);
852 int Counter = 0;
853 Vec_IntForEachEntry( vCof, Obj, k )
854 Counter += (int)Abc_Int2Bdd(aFunc, Obj)->Id;
855 if ( n == 0 )
856 Vec_IntPush( vInfo1, Counter );
857 else {
858 int * pEntry = Vec_IntEntryP( vInfo1, i+1 );
859 *pEntry = Abc_MaxInt( *pEntry, Counter );
860 }
861 }
862 }
863 }
864 assert( c == Vec_WecSize(vInfo) );
865 Vec_WecFree( vCofs );
866 Vec_WecFree( vNodes );
867 return vInfo;
868}
869Vec_Wec_t * Abc_NtkBddCollecInfo3( DdManager * dd, DdNode * aFunc )
870{
871 Vec_Wec_t * vInfo = Vec_WecStart( dd->size*(dd->size-1)*(dd->size-2)/6 );
872 Vec_Wec_t * vNodes = Abc_NtkBddCollectInt( dd, aFunc );
873 Vec_Wec_t * vCofs = Abc_NtkBddCollectCofs( dd, aFunc, vNodes );
874 Vec_Int_t * vLevel; int i, k, Obj, d = 0;
875 for ( int a = 0; a < dd->size; a++ )
876 for ( int b = a+1; b < dd->size; b++ )
877 for ( int c = b+1; c < dd->size; c++ ) {
878 Vec_Int_t * vInfo1 = Vec_WecEntry(vInfo, d++);
879 word Sign = ((word)1 << a) | ((word)1 << b) | ((word)1 << c);
880 for ( int n = 0; n < 8; n++ ) {
881 word Value = ((word)(n & 1) << a) | ((word)((n >> 1) & 1) << b) | ((word)((n >> 2) & 1) << c);
882 Vec_WecForEachLevel( vNodes, vLevel, i )
883 Vec_IntForEachEntry( vLevel, Obj, k )
884 Abc_Int2Bdd(aFunc, Obj)->Id = 0;
885 aFunc->Id = 1;
886 if ( n == 0 )
887 Vec_IntPush( vInfo1, 1 );
888 Vec_WecForEachLevelStop( vNodes, vLevel, i, dd->size ) {
889 Vec_IntForEachEntry( vLevel, Obj, k ) {
890 DdNode * aNode = Abc_Int2Bdd(aFunc, Obj);
891 if ( aNode->Id == 0 )
892 continue;
893 if ( !((Sign >> i) & 1) || ((Value >> i) & 1) == 0 )
894 cuddE(aNode)->Id |= 1;
895 if ( !((Sign >> i) & 1) || ((Value >> i) & 1) == 1 )
896 cuddT(aNode)->Id |= 1;
897 }
898 Vec_Int_t * vCof = Vec_WecEntry(vCofs, i+1);
899 int Counter = 0;
900 Vec_IntForEachEntry( vCof, Obj, k )
901 Counter += (int)Abc_Int2Bdd(aFunc, Obj)->Id;
902 if ( n == 0 )
903 Vec_IntPush( vInfo1, Counter );
904 else {
905 int * pEntry = Vec_IntEntryP( vInfo1, i+1 );
906 *pEntry = Abc_MaxInt( *pEntry, Counter );
907 }
908 }
909 }
910 }
911 assert( d == Vec_WecSize(vInfo) );
912 Vec_WecFree( vCofs );
913 Vec_WecFree( vNodes );
914 return vInfo;
915}
916void Abc_NtkBddPrintInfo1( Vec_Wec_t * vInfo, Vec_Wec_t * vCofs )
917{
918 Vec_Int_t * vLevel; int i, k, Obj;
919 printf( "Cofactor counts:\n" );
920 printf( " : " );
921 Vec_WecForEachLevel( vCofs, vLevel, i )
922 printf( " %2d", i );
923 printf( "\n" );
924 printf( " : " );
925 Vec_WecForEachLevel( vCofs, vLevel, i )
926 printf( " %2d", Vec_IntSize(vLevel) );
927 printf( "\n" );
928 Vec_WecForEachLevel( vInfo, vLevel, i ) {
929 printf( "%2d %c : ", i, 'a'+i );
930 Vec_IntForEachEntry( vLevel, Obj, k )
931 if ( k <= i )
932 printf( " -" );
933 else
934 printf( " %2d", Obj );
935 printf( "\n" );
936 }
937}
938void Abc_NtkBddPrintInfo2( Vec_Wec_t * vInfo, Vec_Wec_t * vCofs )
939{
940 Vec_Int_t * vLevel; int i, k, Obj;
941 printf( "Cofactor counts:\n" );
942 printf( " : " );
943 Vec_WecForEachLevel( vCofs, vLevel, i )
944 printf( " %2d", i );
945 printf( "\n" );
946 printf( " : " );
947 Vec_WecForEachLevel( vCofs, vLevel, i )
948 printf( " %2d", Vec_IntSize(vLevel) );
949 printf( "\n" );
950 int c = 0, Limit = Vec_IntSize(Vec_WecEntry(vInfo, 0))-1;
951 for ( int a = 0; a < Limit; a++ )
952 for ( int b = a+1; b < Limit; b++ ) {
953 Vec_Int_t * vLevel = Vec_WecEntry(vInfo, c++);
954 printf( " %c%c : ", 'a'+a, 'a'+b );
955 int Limit = Abc_MaxInt(a,b);
956 Vec_IntForEachEntry( vLevel, Obj, k )
957 if ( k <= Limit )
958 printf( " -" );
959 else
960 printf( " %2d", Obj );
961 printf( "\n" );
962 }
963 assert( c == Vec_WecSize(vInfo) );
964}
965void Abc_NtkBddPrintInfo3( Vec_Wec_t * vInfo, Vec_Wec_t * vCofs )
966{
967 Vec_Int_t * vLevel; int i, k, Obj;
968 printf( "Cofactor counts:\n" );
969 printf( " : " );
970 Vec_WecForEachLevel( vCofs, vLevel, i )
971 printf( " %2d", i );
972 printf( "\n" );
973 printf( " : " );
974 Vec_WecForEachLevel( vCofs, vLevel, i )
975 printf( " %2d", Vec_IntSize(vLevel) );
976 printf( "\n" );
977 int d = 0, Limit = Vec_IntSize(Vec_WecEntry(vInfo, 0))-1;
978 for ( int a = 0; a < Limit; a++ )
979 for ( int b = a+1; b < Limit; b++ )
980 for ( int c = b+1; c < Limit; c++ ) {
981 Vec_Int_t * vLevel = Vec_WecEntry(vInfo, d++);
982 printf( " %c%c%c : ", 'a'+a, 'a'+b, 'a'+c );
983 int Limit = Abc_MaxInt(a,Abc_MaxInt(b,c));
984 Vec_IntForEachEntry( vLevel, Obj, k )
985 if ( k <= Limit )
986 printf( " -" );
987 else
988 printf( " %2d", Obj );
989 printf( "\n" );
990 }
991 assert( d == Vec_WecSize(vInfo) );
992}
993
994void Abc_NtkBddDecExploreOne( DdManager * dd, DdNode * bFunc, int iOrder )
995{
996 DdManager * ddNew = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
997 int i, * pProfile = ABC_CALLOC( int, dd->size + 100 );
998 Cudd_AutodynEnable( ddNew, CUDD_REORDER_SYMM_SIFT );
999 Vec_Int_t * vPerm = Vec_IntStartNatural( dd->size ); if ( iOrder ) Vec_IntRandomizeOrder( vPerm );
1000 Vec_Int_t * vPermInv = Vec_IntInvert( vPerm, -1 );
1001 DdNode * bFuncNew = Extra_TransferPermute( dd, ddNew, bFunc, Vec_IntArray(vPerm) ); Cudd_Ref(bFuncNew);
1002 if ( iOrder ) Cudd_ReduceHeap( ddNew, CUDD_REORDER_SYMM_SIFT, 1 );
1003 Vec_IntFree( vPerm );
1004 DdNode * aFuncNew = Cudd_BddToAdd( ddNew, bFuncNew ); Cudd_Ref( aFuncNew );
1005 //Extra_ProfileWidth( ddNew, aFuncNew, pProfile, -1 );
1006 if ( iOrder )
1007 printf( "Random order %2d: ", iOrder );
1008 else
1009 printf( "Natural order: " );
1010 printf( "BDD size = %3d ", Cudd_DagSize(aFuncNew) );
1011 for ( i = 0; i < dd->size; i++ )
1012 printf( " %c", 'a' + Vec_IntEntry(vPermInv, ddNew->invperm[i]) );
1013 printf( "\n" );
1014 //Abc_NtkBddTestProfile( ddNew, aFuncNew );
1015
1016 Vec_Wec_t * vNodes = Abc_NtkBddCollectInt( ddNew, aFuncNew );
1017 printf( "Nodes by level:\n" );
1018 Vec_WecPrint( vNodes, 0 );
1019 Vec_Wec_t * vCofs = Abc_NtkBddCollectCofs( ddNew, aFuncNew, vNodes );
1020 printf( "Cofactors by level:\n" );
1021 Vec_WecPrint( vCofs, 0 );
1022 Vec_Wec_t * vInfo1 = Abc_NtkBddCollecInfo1( ddNew, aFuncNew );
1023 Abc_NtkBddPrintInfo1( vInfo1, vCofs );
1024 Vec_Wec_t * vInfo2 = Abc_NtkBddCollecInfo2( ddNew, aFuncNew );
1025 Abc_NtkBddPrintInfo2( vInfo2, vCofs );
1026 Vec_Wec_t * vInfo3 = Abc_NtkBddCollecInfo3( ddNew, aFuncNew );
1027 Abc_NtkBddPrintInfo3( vInfo3, vCofs );
1028 printf( "\n" );
1029 Vec_WecFree( vNodes );
1030 Vec_WecFree( vCofs );
1031 Vec_WecFree( vInfo1 );
1032 Vec_WecFree( vInfo2 );
1033 Vec_WecFree( vInfo3 );
1034
1035 Cudd_RecursiveDeref( ddNew, aFuncNew );
1036 Cudd_RecursiveDeref( ddNew, bFuncNew );
1037 Cudd_Quit( ddNew );
1038 ABC_FREE( pProfile );
1039}
1040void Abc_NtkBddDecExplore( Abc_Obj_t * pNode )
1041{
1042 DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
1043 DdNode * bFunc = (DdNode *)pNode->pData;
1044 int i; Abc_Random(1);
1045 if ( Abc_ObjIsNode(pNode) )
1046 for ( i = 0; i < 4; i++ )
1047 Abc_NtkBddDecExploreOne( dd, bFunc, i );
1048}
1049
1061Abc_Obj_t * Abc_NtkBddDecompose( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int nLutSize, int fVerbose )
1062{
1063 Vec_Ptr_t * vCofs, * vUniq;
1064 DdManager * dd = (DdManager *)pNode->pNtk->pManFunc;
1065 DdNode * bCof;
1066 Abc_Obj_t * pNodeNew = NULL;
1067 Abc_Obj_t * pCofs[20];
1068 int i;
1069 assert( Abc_ObjFaninNum(pNode) > nLutSize );
1070 // try to decompose with two LUTs (the best case for Supp = LutSize + 1)
1071 if ( Abc_ObjFaninNum(pNode) == nLutSize + 1 )
1072 {
1073
1074 pNodeNew = Abc_NtkBddFindCofactor( pNtkNew, pNode, nLutSize );
1075 if ( pNodeNew != NULL )
1076 {
1077 if ( fVerbose )
1078 printf( "Decomposing %d-input node %d using MUX.\n",
1079 Abc_ObjFaninNum(pNode), Abc_ObjId(pNode) );
1080 return pNodeNew;
1081 }
1082
1083 }
1084 // cofactor w.r.t. the bound set variables
1085 vCofs = Abc_NtkBddCofactors( dd, (DdNode *)pNode->pData, nLutSize );
1086 vUniq = Vec_PtrDup( vCofs );
1087 Vec_PtrUniqify( vUniq, (int (*)(const void *, const void *))Vec_PtrSortCompare );
1088 // only perform decomposition which it is support reducing with two less vars
1089 if( Vec_PtrSize(vUniq) > (1 << (nLutSize-2)) )
1090 {
1091 Vec_PtrFree( vCofs );
1092 vCofs = Abc_NtkBddCofactors( dd, (DdNode *)pNode->pData, 2 );
1093 if ( fVerbose )
1094 printf( "Decomposing %d-input node %d using cofactoring with %d cofactors (myu = %d).\n",
1095 Abc_ObjFaninNum(pNode), Abc_ObjId(pNode), Vec_PtrSize(vCofs), Vec_PtrSize(vUniq) );
1096 // implement the cofactors
1097 pCofs[0] = Abc_ObjFanin(pNode, 0)->pCopy;
1098 pCofs[1] = Abc_ObjFanin(pNode, 1)->pCopy;
1099 Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
1100 pCofs[2+i] = Abc_NtkCreateCofLut( pNtkNew, dd, bCof, pNode, 2 );
1101 if ( nLutSize == 4 )
1102 pNodeNew = Abc_NtkBddMux412( pNtkNew, pCofs );
1103 else if ( nLutSize == 5 )
1104 pNodeNew = Abc_NtkBddMux412a( pNtkNew, pCofs );
1105 else if ( nLutSize == 6 )
1106 pNodeNew = Abc_NtkBddMux411( pNtkNew, pCofs );
1107 else assert( 0 );
1108 }
1109 // alternative decompose using MUX-decomposition
1110 else
1111 {
1112 if ( fVerbose )
1113 printf( "Decomposing %d-input node %d using Curtis with %d unique columns.\n",
1114 Abc_ObjFaninNum(pNode), Abc_ObjId(pNode), Vec_PtrSize(vUniq) );
1115 pNodeNew = Abc_NtkBddCurtis( pNtkNew, pNode, vCofs, vUniq );
1116 }
1117 Vec_PtrFree( vCofs );
1118 Vec_PtrFree( vUniq );
1119 return pNodeNew;
1120}
1121
1133void Abc_NtkLutminConstruct( Abc_Ntk_t * pNtkClp, Abc_Ntk_t * pNtkDec, int nLutSize, int fVerbose )
1134{
1135 Vec_Ptr_t * vNodes;
1136 Abc_Obj_t * pNode, * pFanin;
1137 int i, k;
1138 vNodes = Abc_NtkDfs( pNtkClp, 0 );
1139 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
1140 {
1141 if ( Abc_ObjFaninNum(pNode) <= nLutSize )
1142 {
1143 pNode->pCopy = Abc_NtkDupObj( pNtkDec, pNode, 0 );
1144 Abc_ObjForEachFanin( pNode, pFanin, k )
1145 Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
1146 }
1147 else
1148 pNode->pCopy = Abc_NtkBddDecompose( pNtkDec, pNode, nLutSize, fVerbose );
1149 }
1150 Vec_PtrFree( vNodes );
1151}
1152
1164Abc_Ntk_t * Abc_NtkLutminInt( Abc_Ntk_t * pNtk, int nLutSize, int fReorder, int fVerbose )
1165{
1166 extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
1167 Abc_Ntk_t * pNtkDec;
1168 // minimize BDDs
1169 if ( fReorder )
1170 Abc_NtkBddReorder( pNtk, 0 );
1171 // decompose one output at a time
1172 pNtkDec = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
1173 // make sure the new manager has enough inputs
1174 Cudd_bddIthVar( (DdManager *)pNtkDec->pManFunc, Abc_NtkGetFaninMax(pNtk) );
1175 // put the results into the new network (save new CO drivers in old CO drivers)
1176 Abc_NtkLutminConstruct( pNtk, pNtkDec, nLutSize, fVerbose );
1177 // finalize the new network
1178 Abc_NtkFinalize( pNtk, pNtkDec );
1179 // make the network minimum base
1180 Abc_NtkMinimumBase( pNtkDec );
1181 return pNtkDec;
1182}
1183
1195Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fReorder, int fVerbose )
1196{
1197 extern int Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
1198 Abc_Ntk_t * pNtkNew, * pTemp;
1199 int i;
1200 if ( nLutSize < 4 )
1201 {
1202 printf( "The LUT count (%d) should be at least 4.\n", nLutSize );
1203 return NULL;
1204 }
1205 if ( nLutSize > 6 )
1206 {
1207 printf( "The LUT count (%d) should not exceed 6.\n", nLutSize );
1208 return NULL;
1209 }
1210 // create internal representation
1211 if ( Abc_NtkIsStrash(pNtkInit) )
1212 pNtkNew = Abc_NtkDup( pNtkInit );
1213 else
1214 pNtkNew = Abc_NtkStrash( pNtkInit, 0, 1, 0 );
1215 // collapse the network
1216 pNtkNew = Abc_NtkCollapse( pTemp = pNtkNew, 10000, 0, fReorder, 0, 0, 0 );
1217 Abc_NtkDelete( pTemp );
1218 if ( pNtkNew == NULL )
1219 return NULL;
1220 // convert it to BDD
1221 if ( !Abc_NtkIsBddLogic(pNtkNew) )
1222 Abc_NtkToBdd( pNtkNew );
1223 // iterate decomposition
1224 for ( i = 0; Abc_NtkGetFaninMax(pNtkNew) > nLutSize; i++ )
1225 {
1226 if ( fVerbose )
1227 printf( "*** Iteration %d:\n", i+1 );
1228 if ( fVerbose )
1229 printf( "Decomposing network with %d nodes and %d max fanin count for K = %d.\n",
1230 Abc_NtkNodeNum(pNtkNew), Abc_NtkGetFaninMax(pNtkNew), nLutSize );
1231 pNtkNew = Abc_NtkLutminInt( pTemp = pNtkNew, nLutSize, fReorder, fVerbose );
1232 Abc_NtkDelete( pTemp );
1233 }
1234 // fix the problem with complemented and duplicated CO edges
1235 Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
1236 // merge functionally equivalent nodes
1237 Abc_NtkFraigSweep( pNtkNew, 1, 0, 0, 0 );
1238 // make sure everything is okay
1239 if ( !Abc_NtkCheck( pNtkNew ) )
1240 {
1241 printf( "Abc_NtkLutmin: The network check has failed.\n" );
1242 return 0;
1243 }
1244 return pNtkNew;
1245}
1246
1247#else
1248
1249Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtkInit, int nLutSize, int fReorder, int fVerbose ) { return NULL; }
1250void Abc_NtkBddDecExplore( Abc_Obj_t * pNode ) {}
1251
1252#endif
1253
1257
1258
1259ABC_NAMESPACE_IMPL_END
1260
Abc_NtkBddReorder
void Abc_NtkBddReorder(Abc_Ntk_t *pNtk, int fVerbose)
DECLARATIONS ///.
Definition abcReorder.c:107
Abc_NtkLutmin
ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Abc_NtkLutmin(Abc_Ntk_t *pNtkInit, int nLutSize, int fReorder, int fVerbose)
DECLARATIONS ///.
Definition abcLutmin.c:1249
Abc_NtkBddDecExplore
void Abc_NtkBddDecExplore(Abc_Obj_t *pNode)
Definition abcLutmin.c:1250
Abc_NtkFraigSweep
int Abc_NtkFraigSweep(Abc_Ntk_t *pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose)
FUNCTION DEFINITIONS ///.
Definition abcSweep.c:62
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkGetFaninMax
ABC_DLL int Abc_NtkGetFaninMax(Abc_Ntk_t *pNtk)
Definition abcUtil.c:486
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition abcFanio.c:84
Abc_NtkDupObj
ABC_DLL Abc_Obj_t * Abc_NtkDupObj(Abc_Ntk_t *pNtkNew, Abc_Obj_t *pObj, int fCopyName)
Definition abcObj.c:342
Abc_NtkDfs
ABC_DLL Vec_Ptr_t * Abc_NtkDfs(Abc_Ntk_t *pNtk, int fCollectAll)
Definition abcDfs.c:82
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition abcCheck.c:64
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_NtkCollapse
ABC_DLL Abc_Ntk_t * Abc_NtkCollapse(Abc_Ntk_t *pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose)
DECLARATIONS ///.
Definition abcCollapse.c:250
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NtkFinalize
ABC_DLL void Abc_NtkFinalize(Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
Definition abcNtk.c:355
ABC_NTK_LOGIC
@ ABC_NTK_LOGIC
Definition abc.h:57
Abc_NtkLogicMakeSimpleCos
ABC_DLL int Abc_NtkLogicMakeSimpleCos(Abc_Ntk_t *pNtk, int fDuplicate)
Definition abcUtil.c:1080
Abc_NtkStrash
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition abcStrash.c:265
Abc_NtkMinimumBase
ABC_DLL int Abc_NtkMinimumBase(Abc_Ntk_t *pNtk)
DECLARATIONS ///.
Definition abcMinBase.c:892
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition abcNtk.c:1421
ABC_FUNC_BDD
@ ABC_FUNC_BDD
Definition abc.h:66
Abc_NtkStartFrom
ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom(Abc_Ntk_t *pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func)
Definition abcNtk.c:157
Abc_NtkDup
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition abcNtk.c:472
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition abc.h:464
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Abc_Random
unsigned Abc_Random(int fReset)
Definition utilSort.c:1004
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_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
ddClearFlag2
void ddClearFlag2(DdNode *f)
Definition extraBddMisc.c:1724
Extra_bddBitsToCube
DdNode * Extra_bddBitsToCube(DdManager *dd, int Code, int CodeWidth, DdNode **pbVars, int fMsbFirst)
Definition extraBddMisc.c:730
Extra_TransferPermute
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition extraBddMisc.c:87
Extra_bddPrint
void Extra_bddPrint(DdManager *dd, DdNode *F)
Definition extraBddMisc.c:246
Extra_bddMove
DdNode * Extra_bddMove(DdManager *dd, DdNode *bF, int nVars)
Definition extraBddMisc.c:187
Extra_TransferLevelByLevel
DdNode * Extra_TransferLevelByLevel(DdManager *ddSource, DdManager *ddDestination, DdNode *f)
Definition extraBddMisc.c:112
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_::pNtk
Abc_Ntk_t * pNtk
Definition abc.h:130
Abc_Obj_t_::Id
int Id
Definition abc.h:132
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition abc.h:148
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_WecForEachLevelStart
#define Vec_WecForEachLevelStart(vGlob, vVec, i, LevelStart)
Definition vecWec.h:59
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_WecForEachLevelStop
#define Vec_WecForEachLevelStop(vGlob, vVec, i, LevelStop)
Definition vecWec.h:61