From 4812c90424dfc40d26725244723887a2d16ddfd9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2007 08:01:00 -0700 Subject: Version abc71001 --- src/base/abci/abcDsd.c | 551 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 551 insertions(+) create mode 100644 src/base/abci/abcDsd.c (limited to 'src/base/abci/abcDsd.c') diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c new file mode 100644 index 00000000..c00a7d7c --- /dev/null +++ b/src/base/abci/abcDsd.c @@ -0,0 +1,551 @@ +/**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 $] + +***********************************************************************/ + +#include "abc.h" +#include "dsd.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +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 ); + +//////////////////////////////////////////////////////////////////////// +/// 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 [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ) +{ + DdManager * dd; + Abc_Ntk_t * pNtkNew; + assert( Abc_NtkIsStrash(pNtk) ); + dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose ); + if ( dd == NULL ) + return NULL; + if ( fVerbose ) + printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + // transform the result of mapping into a BDD network + pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort ); + Extra_StopManager( dd ); + if ( pNtkNew == NULL ) + return NULL; + // copy EXDC network + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkDsdGlobal: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Constructs the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort ) +{ + char ** ppNamesCi, ** ppNamesCo; + Vec_Ptr_t * vFuncsGlob; + Dsd_Manager_t * pManDsd; + Abc_Ntk_t * pNtkNew; + DdManager * dd; + Abc_Obj_t * pObj; + int i; + + // complement the global functions + vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + Vec_PtrPush( vFuncsGlob, Cudd_NotCond(Abc_ObjGlobalBdd(pObj), Abc_ObjFaninC0(pObj)) ); + + // perform the decomposition + dd = Abc_NtkGlobalBddMan(pNtk); + pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose ); + Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) ); + Vec_PtrFree( vFuncsGlob ); + Abc_NtkFreeGlobalBdds( pNtk, 0 ); + if ( pManDsd == NULL ) + { + Cudd_Quit( dd ); + return NULL; + } + + // start the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); + // make sure the new manager has enough inputs + Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 ); + // put the results into the new network (save new CO drivers in old CO drivers) + Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew ); + // finalize the new network + Abc_NtkFinalize( pNtk, pNtkNew ); + // fix the problem with complemented and duplicated CO edges + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + if ( fPrint ) + { + ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 ); + ppNamesCo = Abc_NtkCollectCioNames( pNtk, 1 ); + Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, fShort, -1 ); + free( ppNamesCi ); + free( ppNamesCo ); + } + + // stop the DSD manager + Dsd_ManagerStop( pManDsd ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Constructs the decomposed network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) +{ + Dsd_Node_t ** ppNodesDsd; + Dsd_Node_t * pNodeDsd; + Abc_Obj_t * pNode, * pNodeNew, * pDriver; + int i, nNodesDsd; + + // save the CI nodes in the DSD nodes + Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) ); + Abc_NtkForEachCi( pNtk, pNode, i ) + { + pNodeDsd = Dsd_ManagerReadInput( pManDsd, i ); + Dsd_NodeSetMark( pNodeDsd, (int)pNode->pCopy ); + } + + // collect DSD nodes in DFS order (leaves and const1 are not collected) + ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd ); + for ( i = 0; i < nNodesDsd; i++ ) + Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew, NULL ); + free( ppNodesDsd ); + + // set the pointers to the CO drivers + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pDriver = Abc_ObjFanin0( pNode ); + if ( !Abc_ObjIsNode(pDriver) ) + continue; + if ( !Abc_AigNodeIsAnd(pDriver) ) + continue; + pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i ); + pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) ); + assert( !Abc_ObjIsComplement(pNodeNew) ); + pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) ); + } +} + +/**Function************************************************************* + + Synopsis [Performs DSD using the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew, int * pCounters ) +{ + DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd ); + DdManager * ddNew = pNtkNew->pManFunc; + Dsd_Node_t * pFaninDsd; + Abc_Obj_t * pNodeNew, * pFanin; + DdNode * bLocal, * bTemp, * bVar; + Dsd_Type_t Type; + int i, nDecs; + + // create the new node + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + // add the fanins + Type = Dsd_NodeReadType( pNodeDsd ); + nDecs = Dsd_NodeReadDecsNum( pNodeDsd ); + assert( nDecs > 1 ); + for ( i = 0; i < nDecs; i++ ) + { + pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i ); + pFanin = (Abc_Obj_t *)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd)); + Abc_ObjAddFanin( pNodeNew, pFanin ); + assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) ); + } + + // create the local function depending on the type of the node + ddNew = pNtkNew->pManFunc; + switch ( Type ) + { + case DSD_NODE_CONST1: + { + bLocal = ddNew->one; Cudd_Ref( bLocal ); + break; + } + case DSD_NODE_OR: + { + bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal ); + for ( i = 0; i < nDecs; i++ ) + { + pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i ); + bVar = Cudd_NotCond( ddNew->vars[i], Dsd_IsComplement(pFaninDsd) ); + bLocal = Cudd_bddOr( ddNew, bTemp = bLocal, bVar ); Cudd_Ref( bLocal ); + Cudd_RecursiveDeref( ddNew, bTemp ); + } + break; + } + case DSD_NODE_EXOR: + { + bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal ); + for ( i = 0; i < nDecs; i++ ) + { + bLocal = Cudd_bddXor( ddNew, bTemp = bLocal, ddNew->vars[i] ); Cudd_Ref( bLocal ); + Cudd_RecursiveDeref( ddNew, bTemp ); + } + break; + } + case DSD_NODE_PRIME: + { + if ( pCounters ) + { + if ( nDecs < 10 ) + pCounters[nDecs]++; + else + pCounters[10]++; + } + bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd ); Cudd_Ref( bLocal ); + bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal ); +/* +if ( nDecs == 3 ) +{ +Extra_bddPrint( ddDsd, bTemp ); +printf( "\n" ); +} +*/ + Cudd_RecursiveDeref( ddDsd, bTemp ); + // bLocal is now in the new BDD manager + break; + } + default: + { + assert( 0 ); + break; + } + } + pNodeNew->pData = bLocal; + Dsd_NodeSetMark( pNodeDsd, (int)pNodeNew ); + return pNodeNew; +} + + + + + + +/**Function************************************************************* + + Synopsis [Recursively decomposes internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDsdLocal( Abc_Ntk_t * pNtk, bool fVerbose, bool fRecursive ) +{ + Dsd_Manager_t * pManDsd; + DdManager * dd = pNtk->pManFunc; + Vec_Ptr_t * vNodes; + int i; + int pCounters[11] = {0}; + + assert( Abc_NtkIsBddLogic(pNtk) ); + + // make the network minimum base + Abc_NtkMinimumBase( pNtk ); + + // start the DSD manager + pManDsd = Dsd_ManagerStart( dd, dd->size, 0 ); + + // collect nodes for decomposition + vNodes = Abc_NtkCollectNodesForDsd( pNtk ); + for ( i = 0; i < vNodes->nSize; i++ ) + Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd, fRecursive, pCounters ); + Vec_PtrFree( vNodes ); + + printf( "Number of non-decomposable functions:\n" ); + for ( i = 3; i < 10; i++ ) + printf( "Inputs = %d. Functions = %6d.\n", i, pCounters[i] ); + printf( "Inputs > %d. Functions = %6d.\n", 9, pCounters[10] ); + + // stop the DSD manager + Dsd_ManagerStop( pManDsd ); + + // make sure everything is okay + if ( !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkDsdRecursive: The network check has failed.\n" ); + return 0; + } + return 1; +} + +/**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 [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode; + int i; + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_NodeIsForDsd(pNode) ) + Vec_PtrPush( vNodes, pNode ); + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Performs decomposition of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive, int * pCounters ) +{ + DdManager * dd = pNode->pNtk->pManFunc; + Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC; + Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd; + int i, nNodesDsd, iVar, fCompl; + + // try disjoint support decomposition + pNodeDsd = Dsd_DecomposeOne( pManDsd, pNode->pData ); + fCompl = Dsd_IsComplement( pNodeDsd ); + pNodeDsd = Dsd_Regular( pNodeDsd ); + + // determine what decomposition to use + if ( !fRecursive || Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) ) + { // perform DSD + + // set the inputs + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + pFaninDsd = Dsd_ManagerReadInput( pManDsd, i ); + Dsd_NodeSetMark( pFaninDsd, (int)pFanin ); + } + + // construct the intermediate nodes + ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd ); + for ( i = 0; i < nNodesDsd; i++ ) + { + pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk, pCounters ); + if ( Abc_NodeIsForDsd(pRoot) && fRecursive ) + Vec_PtrPush( vNodes, pRoot ); + } + free( ppNodesDsd ); + + // remove the current fanins + Abc_ObjRemoveFanins( pNode ); + // add fanin to the root + Abc_ObjAddFanin( pNode, pRoot ); + // update the function to be that of buffer + Cudd_RecursiveDeref( dd, pNode->pData ); + pNode->pData = Cudd_NotCond( dd->vars[0], fCompl ); Cudd_Ref( pNode->pData ); + } + else // perform MUX-decomposition + { + // get the cofactoring variable + iVar = Abc_NodeFindMuxVar( dd, pNode->pData, Abc_ObjFaninNum(pNode) ); + pNodeC = Abc_ObjFanin( pNode, iVar ); + + // get the negative cofactor + pNode1 = Abc_NtkCloneObj( pNode ); + pNode1->pData = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(dd->vars[iVar]) ); Cudd_Ref( pNode1->pData ); + Abc_NodeMinimumBase( pNode1 ); + if ( Abc_NodeIsForDsd(pNode1) ) + Vec_PtrPush( vNodes, pNode1 ); + + // get the positive cofactor + pNode2 = Abc_NtkCloneObj( pNode ); + pNode2->pData = Cudd_Cofactor( dd, pNode->pData, dd->vars[iVar] ); Cudd_Ref( pNode2->pData ); + Abc_NodeMinimumBase( pNode2 ); + if ( Abc_NodeIsForDsd(pNode2) ) + Vec_PtrPush( vNodes, pNode2 ); + + // remove the current fanins + Abc_ObjRemoveFanins( pNode ); + // add new fanins + Abc_ObjAddFanin( pNode, pNodeC ); + Abc_ObjAddFanin( pNode, pNode2 ); + Abc_ObjAddFanin( pNode, pNode1 ); + // update the function to be that of MUX + Cudd_RecursiveDeref( dd, pNode->pData ); + pNode->pData = Cudd_bddIte( dd, dd->vars[0], dd->vars[1], dd->vars[2] ); Cudd_Ref( pNode->pData ); + } +} + +/**Function************************************************************* + + Synopsis [Checks if the node should be decomposed by DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsForDsd( Abc_Obj_t * pNode ) +{ + DdManager * dd = pNode->pNtk->pManFunc; +// DdNode * bFunc, * bFunc0, * bFunc1; + assert( Abc_ObjIsNode(pNode) ); +// if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) ) +// return 1; +// return 0; + +/* + // this does not catch things like a(b+c), which should be decomposed + for ( bFunc = Cudd_Regular(pNode->pData); !cuddIsConstant(bFunc); ) + { + bFunc0 = Cudd_Regular( cuddE(bFunc) ); + bFunc1 = cuddT(bFunc); + if ( bFunc0 == b1 ) + bFunc = bFunc1; + else if ( bFunc1 == b1 || bFunc0 == bFunc1 ) + bFunc = bFunc0; + else + return 1; + } +*/ + if ( Abc_ObjFaninNum(pNode) > 2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Determines a cofactoring variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars ) +{ + DdNode * bVar, * bCof0, * bCof1; + int SuppSumMin = 1000000; + int i, nSSD, nSSQ, iVar; + +// printf( "\n\nCofactors:\n\n" ); + iVar = -1; + for ( i = 0; i < nVars; i++ ) + { + bVar = dd->vars[i]; + + bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof0 ); + bCof1 = Cudd_Cofactor( dd, bFunc, bVar ); Cudd_Ref( bCof1 ); + +// nodD = Cudd_DagSize(bCof0); +// nodQ = Cudd_DagSize(bCof1); +// printf( "+%02d: D=%2d. Q=%2d. ", i, nodD, nodQ ); +// printf( "S=%2d. D=%2d. ", nodD + nodQ, abs(nodD-nodQ) ); + + nSSD = Cudd_SupportSize( dd, bCof0 ); + nSSQ = Cudd_SupportSize( dd, bCof1 ); + +// printf( "SD=%2d. SQ=%2d. ", nSSD, nSSQ ); +// printf( "S=%2d. D=%2d. ", nSSD + nSSQ, abs(nSSD - nSSQ) ); +// printf( "Cost=%3d. ", Cost(nodD,nodQ,nSSD,nSSQ) ); +// printf( "\n" ); + + Cudd_RecursiveDeref( dd, bCof0 ); + Cudd_RecursiveDeref( dd, bCof1 ); + + if ( SuppSumMin > nSSD + nSSQ ) + { + SuppSumMin = nSSD + nSSQ; + iVar = i; + } + } + return iVar; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3