src/base/abci/abcDsd.c File Reference

#include "abc.h"
#include "dsd.h"
Include dependency graph for abcDsd.c:

Go to the source code of this file.

Functions

static Abc_Ntk_t * Abc_NtkDsdInternal (Abc_Ntk_t *pNtk, bool fVerbose, bool fPrint, bool fShort)
static void Abc_NtkDsdConstruct (Dsd_Manager_t *pManDsd, Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew)
static Abc_Obj_t * Abc_NtkDsdConstructNode (Dsd_Manager_t *pManDsd, Dsd_Node_t *pNodeDsd, Abc_Ntk_t *pNtkNew, int *pCounters)
static Vec_Ptr_t * Abc_NtkCollectNodesForDsd (Abc_Ntk_t *pNtk)
static void Abc_NodeDecompDsdAndMux (Abc_Obj_t *pNode, Vec_Ptr_t *vNodes, Dsd_Manager_t *pManDsd, bool fRecursive, int *pCounters)
static bool Abc_NodeIsForDsd (Abc_Obj_t *pNode)
static int Abc_NodeFindMuxVar (DdManager *dd, DdNode *bFunc, int nVars)
Abc_Ntk_t * Abc_NtkDsdGlobal (Abc_Ntk_t *pNtk, bool fVerbose, bool fPrint, bool fShort)
int Abc_NtkDsdLocal (Abc_Ntk_t *pNtk, bool fVerbose, bool fRecursive)

Function Documentation

void Abc_NodeDecompDsdAndMux ( Abc_Obj_t *  pNode,
Vec_Ptr_t *  vNodes,
Dsd_Manager_t *  pManDsd,
bool  fRecursive,
int *  pCounters 
) [static]

Function*************************************************************

Synopsis [Performs decomposition of one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file abcDsd.c.

00384 {
00385     DdManager * dd = pNode->pNtk->pManFunc;
00386     Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC;
00387     Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd;
00388     int i, nNodesDsd, iVar, fCompl;
00389 
00390     // try disjoint support decomposition
00391     pNodeDsd = Dsd_DecomposeOne( pManDsd, pNode->pData );
00392     fCompl   = Dsd_IsComplement( pNodeDsd );
00393     pNodeDsd = Dsd_Regular( pNodeDsd );
00394 
00395     // determine what decomposition to use   
00396     if ( !fRecursive || Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) )
00397     { // perform DSD
00398 
00399         // set the inputs
00400         Abc_ObjForEachFanin( pNode, pFanin, i )
00401         {
00402             pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
00403             Dsd_NodeSetMark( pFaninDsd, (int)pFanin );
00404         }
00405 
00406         // construct the intermediate nodes
00407         ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd );
00408         for ( i = 0; i < nNodesDsd; i++ )
00409         {
00410             pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk, pCounters );
00411             if ( Abc_NodeIsForDsd(pRoot) && fRecursive )
00412                 Vec_PtrPush( vNodes, pRoot );
00413         }
00414         free( ppNodesDsd );
00415 
00416         // remove the current fanins
00417         Abc_ObjRemoveFanins( pNode );
00418         // add fanin to the root
00419         Abc_ObjAddFanin( pNode, pRoot );
00420         // update the function to be that of buffer
00421         Cudd_RecursiveDeref( dd, pNode->pData );
00422         pNode->pData = Cudd_NotCond( dd->vars[0], fCompl ); Cudd_Ref( pNode->pData );
00423     }
00424     else // perform MUX-decomposition
00425     {
00426         // get the cofactoring variable
00427         iVar = Abc_NodeFindMuxVar( dd, pNode->pData, Abc_ObjFaninNum(pNode) );
00428         pNodeC = Abc_ObjFanin( pNode, iVar );
00429 
00430         // get the negative cofactor
00431         pNode1 = Abc_NtkCloneObj( pNode );
00432         pNode1->pData = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(dd->vars[iVar]) );  Cudd_Ref( pNode1->pData );
00433         Abc_NodeMinimumBase( pNode1 );
00434         if ( Abc_NodeIsForDsd(pNode1) )
00435             Vec_PtrPush( vNodes, pNode1 );
00436 
00437         // get the positive cofactor
00438         pNode2 = Abc_NtkCloneObj( pNode );
00439         pNode2->pData = Cudd_Cofactor( dd, pNode->pData, dd->vars[iVar] );            Cudd_Ref( pNode2->pData );
00440         Abc_NodeMinimumBase( pNode2 );
00441         if ( Abc_NodeIsForDsd(pNode2) )
00442             Vec_PtrPush( vNodes, pNode2 );
00443 
00444         // remove the current fanins
00445         Abc_ObjRemoveFanins( pNode );
00446         // add new fanins
00447         Abc_ObjAddFanin( pNode, pNodeC );
00448         Abc_ObjAddFanin( pNode, pNode2 );
00449         Abc_ObjAddFanin( pNode, pNode1 );
00450         // update the function to be that of MUX
00451         Cudd_RecursiveDeref( dd, pNode->pData );
00452         pNode->pData = Cudd_bddIte( dd, dd->vars[0], dd->vars[1], dd->vars[2] );    Cudd_Ref( pNode->pData );
00453     }
00454 }

int Abc_NodeFindMuxVar ( DdManager *  dd,
DdNode *  bFunc,
int  nVars 
) [static]

Function*************************************************************

Synopsis [Determines a cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 506 of file abcDsd.c.

00507 {
00508         DdNode * bVar, * bCof0, * bCof1;
00509         int SuppSumMin = 1000000;
00510         int i, nSSD, nSSQ, iVar;
00511 
00512 //      printf( "\n\nCofactors:\n\n" );
00513         iVar = -1;
00514         for ( i = 0; i < nVars; i++ )
00515         {
00516                 bVar = dd->vars[i];
00517 
00518                 bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) );  Cudd_Ref( bCof0 );
00519                 bCof1 = Cudd_Cofactor( dd, bFunc,          bVar  );  Cudd_Ref( bCof1 );
00520 
00521 //              nodD = Cudd_DagSize(bCof0);
00522 //              nodQ = Cudd_DagSize(bCof1);
00523 //              printf( "+%02d: D=%2d. Q=%2d.  ", i, nodD, nodQ );
00524 //              printf( "S=%2d. D=%2d.  ", nodD + nodQ, abs(nodD-nodQ) );
00525 
00526                 nSSD = Cudd_SupportSize( dd, bCof0 );
00527                 nSSQ = Cudd_SupportSize( dd, bCof1 );
00528 
00529 //              printf( "SD=%2d. SQ=%2d.  ", nSSD, nSSQ );
00530 //              printf( "S=%2d. D=%2d.  ", nSSD + nSSQ, abs(nSSD - nSSQ) );
00531 //              printf( "Cost=%3d. ", Cost(nodD,nodQ,nSSD,nSSQ) );
00532 //              printf( "\n" );
00533 
00534                 Cudd_RecursiveDeref( dd, bCof0 );
00535                 Cudd_RecursiveDeref( dd, bCof1 );
00536 
00537                 if ( SuppSumMin > nSSD + nSSQ )
00538                 {
00539                          SuppSumMin = nSSD + nSSQ;
00540                          iVar = i;
00541                 }
00542         }
00543     return iVar;
00544 }

bool Abc_NodeIsForDsd ( Abc_Obj_t *  pNode  )  [static]

Function*************************************************************

Synopsis [Checks if the node should be decomposed by DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 467 of file abcDsd.c.

00468 {
00469     DdManager * dd = pNode->pNtk->pManFunc;
00470 //    DdNode * bFunc, * bFunc0, * bFunc1;
00471     assert( Abc_ObjIsNode(pNode) );
00472 //    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
00473 //        return 1;
00474 //    return 0;
00475 
00476 /*
00477     // this does not catch things like a(b+c), which should be decomposed
00478     for ( bFunc = Cudd_Regular(pNode->pData); !cuddIsConstant(bFunc); )
00479     {
00480         bFunc0 = Cudd_Regular( cuddE(bFunc) );
00481         bFunc1 = cuddT(bFunc);
00482         if ( bFunc0 == b1 )
00483             bFunc = bFunc1;
00484         else if ( bFunc1 == b1 || bFunc0 == bFunc1 )
00485             bFunc = bFunc0;
00486         else
00487             return 1;
00488     }
00489 */
00490     if ( Abc_ObjFaninNum(pNode) > 2 )
00491         return 1;
00492     return 0;
00493 }

Vec_Ptr_t * Abc_NtkCollectNodesForDsd ( Abc_Ntk_t *  pNtk  )  [static]

Function*************************************************************

Synopsis [Collects the nodes that may need decomposition.]

Description [The nodes that do not need decomposition are those whose BDD has more internal nodes than the support size.]

SideEffects []

SeeAlso []

Definition at line 358 of file abcDsd.c.

00359 {
00360     Vec_Ptr_t * vNodes;
00361     Abc_Obj_t * pNode;
00362     int i;
00363     vNodes = Vec_PtrAlloc( 100 );
00364     Abc_NtkForEachNode( pNtk, pNode, i )
00365     {
00366         if ( Abc_NodeIsForDsd(pNode) )
00367             Vec_PtrPush( vNodes, pNode );
00368     }
00369     return vNodes;
00370 }

void Abc_NtkDsdConstruct ( Dsd_Manager_t *  pManDsd,
Abc_Ntk_t *  pNtk,
Abc_Ntk_t *  pNtkNew 
) [static]

Function*************************************************************

Synopsis [Constructs the decomposed network.]

Description []

SideEffects []

SeeAlso []

Definition at line 156 of file abcDsd.c.

00157 {
00158     Dsd_Node_t ** ppNodesDsd;
00159     Dsd_Node_t * pNodeDsd;
00160     Abc_Obj_t * pNode, * pNodeNew, * pDriver;
00161     int i, nNodesDsd;
00162 
00163     // save the CI nodes in the DSD nodes
00164     Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) );
00165     Abc_NtkForEachCi( pNtk, pNode, i )
00166     {
00167         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
00168         Dsd_NodeSetMark( pNodeDsd, (int)pNode->pCopy );
00169     }
00170 
00171     // collect DSD nodes in DFS order (leaves and const1 are not collected)
00172     ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
00173     for ( i = 0; i < nNodesDsd; i++ )
00174         Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew, NULL );
00175     free( ppNodesDsd );
00176 
00177     // set the pointers to the CO drivers
00178     Abc_NtkForEachCo( pNtk, pNode, i )
00179     {
00180         pDriver = Abc_ObjFanin0( pNode );
00181         if ( !Abc_ObjIsNode(pDriver) )
00182             continue;
00183         if ( !Abc_AigNodeIsAnd(pDriver) )
00184             continue;
00185         pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
00186         pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
00187         assert( !Abc_ObjIsComplement(pNodeNew) );
00188         pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) );
00189     }
00190 }

Abc_Obj_t * Abc_NtkDsdConstructNode ( Dsd_Manager_t *  pManDsd,
Dsd_Node_t *  pNodeDsd,
Abc_Ntk_t *  pNtkNew,
int *  pCounters 
) [static]

Function*************************************************************

Synopsis [Performs DSD using the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file abcDsd.c.

00204 {
00205     DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
00206     DdManager * ddNew = pNtkNew->pManFunc;
00207     Dsd_Node_t * pFaninDsd;
00208     Abc_Obj_t * pNodeNew, * pFanin;
00209     DdNode * bLocal, * bTemp, * bVar;
00210     Dsd_Type_t Type;
00211     int i, nDecs;
00212 
00213     // create the new node
00214     pNodeNew = Abc_NtkCreateNode( pNtkNew );
00215     // add the fanins
00216     Type  = Dsd_NodeReadType( pNodeDsd );
00217     nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
00218     assert( nDecs > 1 );
00219     for ( i = 0; i < nDecs; i++ )
00220     {
00221         pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
00222         pFanin     = (Abc_Obj_t *)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
00223         Abc_ObjAddFanin( pNodeNew, pFanin );
00224         assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
00225     }
00226 
00227     // create the local function depending on the type of the node
00228     ddNew = pNtkNew->pManFunc;
00229     switch ( Type )
00230     {
00231         case DSD_NODE_CONST1:
00232         {
00233             bLocal = ddNew->one; Cudd_Ref( bLocal );
00234             break;
00235         }
00236         case DSD_NODE_OR:
00237         {
00238             bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
00239             for ( i = 0; i < nDecs; i++ )
00240             {
00241                 pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
00242                 bVar   = Cudd_NotCond( ddNew->vars[i], Dsd_IsComplement(pFaninDsd) );
00243                 bLocal = Cudd_bddOr( ddNew, bTemp = bLocal, bVar );               Cudd_Ref( bLocal );
00244                 Cudd_RecursiveDeref( ddNew, bTemp );
00245             }
00246             break;
00247         }
00248         case DSD_NODE_EXOR:
00249         {
00250             bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
00251             for ( i = 0; i < nDecs; i++ )
00252             {
00253                 bLocal = Cudd_bddXor( ddNew, bTemp = bLocal, ddNew->vars[i] );    Cudd_Ref( bLocal );
00254                 Cudd_RecursiveDeref( ddNew, bTemp );
00255             }
00256             break;
00257         }
00258         case DSD_NODE_PRIME:
00259         {
00260             if ( pCounters )
00261             {
00262                 if ( nDecs < 10 )
00263                     pCounters[nDecs]++;
00264                 else
00265                     pCounters[10]++;
00266             }
00267             bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
00268             bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
00269 /*
00270 if ( nDecs == 3 )
00271 {
00272 Extra_bddPrint( ddDsd, bTemp );
00273 printf( "\n" );
00274 }
00275 */
00276             Cudd_RecursiveDeref( ddDsd, bTemp );
00277             // bLocal is now in the new BDD manager
00278             break;
00279         }
00280         default:
00281         {
00282             assert( 0 );
00283             break;
00284         }
00285     }
00286     pNodeNew->pData = bLocal;
00287     Dsd_NodeSetMark( pNodeDsd, (int)pNodeNew );
00288     return pNodeNew;
00289 }

Abc_Ntk_t* Abc_NtkDsdGlobal ( Abc_Ntk_t *  pNtk,
bool  fVerbose,
bool  fPrint,
bool  fShort 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Derives the DSD network.]

Description [Takes the strashed network (pNtk), derives global BDDs for the combinational outputs of this network, and decomposes these BDDs using disjoint support decomposition. Finally, constructs and return a new network, which is topologically equivalent to the decomposition tree. Allocates and frees a new BDD manager and a new DSD manager.]

SideEffects []

SeeAlso []

Definition at line 56 of file abcDsd.c.

00057 {
00058     DdManager * dd;
00059     Abc_Ntk_t * pNtkNew;
00060     assert( Abc_NtkIsStrash(pNtk) );
00061     dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
00062     if ( dd == NULL )
00063         return NULL;
00064     if ( fVerbose )
00065         printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
00066     // transform the result of mapping into a BDD network
00067     pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
00068     Extra_StopManager( dd );
00069     if ( pNtkNew == NULL )
00070         return NULL;
00071     // copy EXDC network
00072     if ( pNtk->pExdc )
00073         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
00074     if ( !Abc_NtkCheck( pNtkNew ) )
00075     {
00076         printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
00077         Abc_NtkDelete( pNtkNew );
00078         return NULL;
00079     }
00080     return pNtkNew;
00081 }

Abc_Ntk_t * Abc_NtkDsdInternal ( Abc_Ntk_t *  pNtk,
bool  fVerbose,
bool  fPrint,
bool  fShort 
) [static]

CFile****************************************************************

FileName [abcDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Decomposes the network using disjoint-support decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
abcDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS ///

Function*************************************************************

Synopsis [Constructs the decomposed network.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file abcDsd.c.

00095 {
00096     char ** ppNamesCi, ** ppNamesCo;
00097     Vec_Ptr_t * vFuncsGlob;
00098     Dsd_Manager_t * pManDsd;
00099     Abc_Ntk_t * pNtkNew;
00100     DdManager * dd;
00101     Abc_Obj_t * pObj;
00102     int i;
00103 
00104     // complement the global functions
00105     vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
00106     Abc_NtkForEachCo( pNtk, pObj, i )
00107         Vec_PtrPush( vFuncsGlob, Cudd_NotCond(Abc_ObjGlobalBdd(pObj), Abc_ObjFaninC0(pObj)) );
00108 
00109     // perform the decomposition
00110     dd = Abc_NtkGlobalBddMan(pNtk);
00111     pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
00112     Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
00113     Vec_PtrFree( vFuncsGlob );
00114     Abc_NtkFreeGlobalBdds( pNtk, 0 );
00115     if ( pManDsd == NULL )
00116     {
00117         Cudd_Quit( dd );
00118         return NULL;
00119     }
00120 
00121     // start the new network
00122     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
00123     // make sure the new manager has enough inputs
00124     Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
00125     // put the results into the new network (save new CO drivers in old CO drivers)
00126     Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
00127     // finalize the new network
00128     Abc_NtkFinalize( pNtk, pNtkNew );
00129     // fix the problem with complemented and duplicated CO edges
00130     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
00131     if ( fPrint )
00132     {
00133         ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
00134         ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 );
00135         Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 );
00136         free( ppNamesCi );
00137         free( ppNamesCo );
00138     }
00139 
00140     // stop the DSD manager
00141     Dsd_ManagerStop( pManDsd );
00142     return pNtkNew;
00143 }

int Abc_NtkDsdLocal ( Abc_Ntk_t *  pNtk,
bool  fVerbose,
bool  fRecursive 
)

Function*************************************************************

Synopsis [Recursively decomposes internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file abcDsd.c.

00308 {
00309     Dsd_Manager_t * pManDsd;
00310     DdManager * dd = pNtk->pManFunc;
00311     Vec_Ptr_t * vNodes;
00312     int i;
00313     int pCounters[11] = {0};
00314 
00315     assert( Abc_NtkIsBddLogic(pNtk) );
00316 
00317     // make the network minimum base
00318     Abc_NtkMinimumBase( pNtk );
00319 
00320     // start the DSD manager
00321     pManDsd = Dsd_ManagerStart( dd, dd->size, 0 );
00322 
00323     // collect nodes for decomposition
00324     vNodes = Abc_NtkCollectNodesForDsd( pNtk );
00325     for ( i = 0; i < vNodes->nSize; i++ )
00326         Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd, fRecursive, pCounters );
00327     Vec_PtrFree( vNodes );
00328 
00329     printf( "Number of non-decomposable functions:\n" );
00330     for ( i = 3; i < 10; i++ )
00331         printf( "Inputs = %d.  Functions = %6d.\n", i, pCounters[i] );
00332     printf( "Inputs > %d.  Functions = %6d.\n", 9, pCounters[10] );
00333 
00334     // stop the DSD manager
00335     Dsd_ManagerStop( pManDsd );
00336 
00337     // make sure everything is okay
00338     if ( !Abc_NtkCheck( pNtk ) )
00339     {
00340         printf( "Abc_NtkDsdRecursive: The network check has failed.\n" );
00341         return 0;
00342     }
00343     return 1;
00344 }

Generated on Tue Jan 5 12:18:35 2010 for abc70930 by  doxygen 1.6.1