diff options
Diffstat (limited to 'src/bdd/dsd/dsdLocal.c')
| -rw-r--r-- | src/bdd/dsd/dsdLocal.c | 337 |
1 files changed, 0 insertions, 337 deletions
diff --git a/src/bdd/dsd/dsdLocal.c b/src/bdd/dsd/dsdLocal.c deleted file mode 100644 index 6dd6e7d1..00000000 --- a/src/bdd/dsd/dsdLocal.c +++ /dev/null @@ -1,337 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsdLocal.c] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [Deriving the local function of the DSD node.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsdLocal.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "dsdInt.h" - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// STATIC VARIABLES /// -//////////////////////////////////////////////////////////////////////// - -static DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bFunc, st_table * pCache, - int * pVar2Form, int * pForm2Var, DdNode * pbCube0[], DdNode * pbCube1[] ); -static DdNode * Extra_bddNodePointedByCube( DdManager * dd, DdNode * bF, DdNode * bC ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Returns the local function of the DSD node. ] - - Description [The local function is computed using the global function - of the node and the global functions of the formal inputs. The resulting - local function is mapped using the topmost N variables of the manager. - The number of variables N is equal to the number of formal inputs.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ) -{ - int * pForm2Var; // the mapping of each formal input into its first var - int * pVar2Form; // the mapping of each var into its formal inputs - int i, iVar, iLev, * pPermute; - DdNode ** pbCube0, ** pbCube1; - DdNode * bFunc, * bRes, * bTemp; - st_table * pCache; - - pPermute = ALLOC( int, dd->size ); - pVar2Form = ALLOC( int, dd->size ); - pForm2Var = ALLOC( int, dd->size ); - - pbCube0 = ALLOC( DdNode *, dd->size ); - pbCube1 = ALLOC( DdNode *, dd->size ); - - // remap the global function in such a way that - // the support variables of each formal input are adjacent - iLev = 0; - for ( i = 0; i < pNode->nDecs; i++ ) - { - pForm2Var[i] = dd->invperm[i]; - for ( bTemp = pNode->pDecs[i]->S; bTemp != b1; bTemp = cuddT(bTemp) ) - { - iVar = dd->invperm[iLev]; - pPermute[bTemp->index] = iVar; - pVar2Form[iVar] = i; - iLev++; - } - - // collect the cubes representing each assignment - pbCube0[i] = Extra_bddGetOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) ); - Cudd_Ref( pbCube0[i] ); - pbCube1[i] = Extra_bddGetOneCube( dd, pNode->pDecs[i]->G ); - Cudd_Ref( pbCube1[i] ); - } - - // remap the function - bFunc = Cudd_bddPermute( dd, pNode->G, pPermute ); Cudd_Ref( bFunc ); - // remap the cube - for ( i = 0; i < pNode->nDecs; i++ ) - { - pbCube0[i] = Cudd_bddPermute( dd, bTemp = pbCube0[i], pPermute ); Cudd_Ref( pbCube0[i] ); - Cudd_RecursiveDeref( dd, bTemp ); - pbCube1[i] = Cudd_bddPermute( dd, bTemp = pbCube1[i], pPermute ); Cudd_Ref( pbCube1[i] ); - Cudd_RecursiveDeref( dd, bTemp ); - } - - // remap the function - pCache = st_init_table(st_ptrcmp,st_ptrhash); - bRes = Extra_dsdRemap( dd, bFunc, pCache, pVar2Form, pForm2Var, pbCube0, pbCube1 ); Cudd_Ref( bRes ); - st_free_table( pCache ); - - Cudd_RecursiveDeref( dd, bFunc ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - Cudd_RecursiveDeref( dd, pbCube0[i] ); - Cudd_RecursiveDeref( dd, pbCube1[i] ); - } -/* -//////////// - // permute the function once again - // in such a way that i-th var stood for i-th formal input - for ( i = 0; i < dd->size; i++ ) - pPermute[i] = -1; - for ( i = 0; i < pNode->nDecs; i++ ) - pPermute[dd->invperm[i]] = i; - bRes = Cudd_bddPermute( dd, bTemp = bRes, pPermute ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bTemp ); -//////////// -*/ - FREE(pPermute); - FREE(pVar2Form); - FREE(pForm2Var); - FREE(pbCube0); - FREE(pbCube1); - - Cudd_Deref( bRes ); - return bRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_dsdRemap( DdManager * dd, DdNode * bF, st_table * pCache, - int * pVar2Form, int * pForm2Var, DdNode * pbCube0[], DdNode * pbCube1[] ) -{ - DdNode * bFR, * bF0, * bF1; - DdNode * bRes0, * bRes1, * bRes; - int iForm; - - bFR = Cudd_Regular(bF); - if ( cuddIsConstant(bFR) ) - return bF; - - // check the hash-table - if ( bFR->ref != 1 ) - { - if ( st_lookup( pCache, (char *)bF, (char **)&bRes ) ) - return bRes; - } - - // get the formal input - iForm = pVar2Form[bFR->index]; - - // get the nodes pointed to by the cube - bF0 = Extra_bddNodePointedByCube( dd, bF, pbCube0[iForm] ); - bF1 = Extra_bddNodePointedByCube( dd, bF, pbCube1[iForm] ); - - // call recursively for these nodes - bRes0 = Extra_dsdRemap( dd, bF0, pCache, pVar2Form, pForm2Var, pbCube0, pbCube1 ); Cudd_Ref( bRes0 ); - bRes1 = Extra_dsdRemap( dd, bF1, pCache, pVar2Form, pForm2Var, pbCube0, pbCube1 ); Cudd_Ref( bRes1 ); - - // derive the result using ITE - bRes = Cudd_bddIte( dd, dd->vars[ pForm2Var[iForm] ], bRes1, bRes0 ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bRes0 ); - Cudd_RecursiveDeref( dd, bRes1 ); - - // add to the hash table - if ( bFR->ref != 1 ) - st_insert( pCache, (char *)bF, (char *)bRes ); - Cudd_Deref( bRes ); - return bRes; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Extra_bddNodePointedByCube( DdManager * dd, DdNode * bF, DdNode * bC ) -{ - DdNode * bFR, * bCR; - DdNode * bF0, * bF1; - DdNode * bC0, * bC1; - int LevelF, LevelC; - - assert( bC != b0 ); - if ( bC == b1 ) - return bF; - -// bRes = cuddCacheLookup2( dd, Extra_bddNodePointedByCube, bF, bC ); -// if ( bRes ) -// return bRes; - // there is no need for caching because this operation is very fast - // there will no gain reusing the results of this operations - // instead, it will flush CUDD cache of other useful entries - - - bFR = Cudd_Regular( bF ); - bCR = Cudd_Regular( bC ); - assert( !cuddIsConstant( bFR ) ); - - LevelF = dd->perm[bFR->index]; - LevelC = dd->perm[bCR->index]; - - if ( LevelF <= LevelC ) - { - if ( bFR != bF ) - { - bF0 = Cudd_Not( cuddE(bFR) ); - bF1 = Cudd_Not( cuddT(bFR) ); - } - else - { - bF0 = cuddE(bFR); - bF1 = cuddT(bFR); - } - } - else - { - bF0 = bF1 = bF; - } - - if ( LevelC <= LevelF ) - { - if ( bCR != bC ) - { - bC0 = Cudd_Not( cuddE(bCR) ); - bC1 = Cudd_Not( cuddT(bCR) ); - } - else - { - bC0 = cuddE(bCR); - bC1 = cuddT(bCR); - } - } - else - { - bC0 = bC1 = bC; - } - - assert( bC0 == b0 || bC1 == b0 ); - if ( bC0 == b0 ) - return Extra_bddNodePointedByCube( dd, bF1, bC1 ); - return Extra_bddNodePointedByCube( dd, bF0, bC0 ); -} - -#if 0 - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * dsdTreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode, int fRemap ) -{ - DdNode * bCof0, * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp; - int i; - int fAllBuffs = 1; - static int Permute[MAXINPUTS]; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->Type == DT_PRIME ); - - // transform the function of this block to depend on inputs - // corresponding to the formal inputs - - // first, substitute those inputs that have some blocks associated with them - // second, remap the inputs to the top of the manager (then, it is easy to output them) - - // start the function - bNewFunc = pNode->G; Cudd_Ref( bNewFunc ); - // go over all primary inputs - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pNode->pDecs[i]->Type != DT_BUF ) // remap only if it is not the buffer - { - bCube0 = Extra_bddFindOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) ); Cudd_Ref( bCube0 ); - bCof0 = Cudd_Cofactor( dd, bNewFunc, bCube0 ); Cudd_Ref( bCof0 ); - Cudd_RecursiveDeref( dd, bCube0 ); - - bCube1 = Extra_bddFindOneCube( dd, pNode->pDecs[i]->G ); Cudd_Ref( bCube1 ); - bCof1 = Cudd_Cofactor( dd, bNewFunc, bCube1 ); Cudd_Ref( bCof1 ); - Cudd_RecursiveDeref( dd, bCube1 ); - - Cudd_RecursiveDeref( dd, bNewFunc ); - - // use the variable in the i-th level of the manager -// bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 ); Cudd_Ref( bNewFunc ); - // use the first variale in the support of the component - bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 ); Cudd_Ref( bNewFunc ); - Cudd_RecursiveDeref( dd, bCof0 ); - Cudd_RecursiveDeref( dd, bCof1 ); - } - - if ( fRemap ) - { - // remap the function to the top of the manager - // remap the function to the first variables of the manager - for ( i = 0; i < pNode->nDecs; i++ ) - // Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i]; - Permute[ pNode->pDecs[i]->S->index ] = i; - - bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute ); Cudd_Ref( bNewFunc ); - Cudd_RecursiveDeref( dd, bTemp ); - } - - Cudd_Deref( bNewFunc ); - return bNewFunc; -} - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// |