diff options
Diffstat (limited to 'src/bdd/dsd')
| -rw-r--r-- | src/bdd/dsd/dsd.h | 129 | ||||
| -rw-r--r-- | src/bdd/dsd/dsdApi.c | 97 | ||||
| -rw-r--r-- | src/bdd/dsd/dsdCheck.c | 314 | ||||
| -rw-r--r-- | src/bdd/dsd/dsdInt.h | 91 | ||||
| -rw-r--r-- | src/bdd/dsd/dsdLocal.c | 337 | ||||
| -rw-r--r-- | src/bdd/dsd/dsdMan.c | 114 | ||||
| -rw-r--r-- | src/bdd/dsd/dsdProc.c | 1617 | ||||
| -rw-r--r-- | src/bdd/dsd/dsdTree.c | 1068 | ||||
| -rw-r--r-- | src/bdd/dsd/module.make | 6 |
9 files changed, 0 insertions, 3773 deletions
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h deleted file mode 100644 index b73b81ab..00000000 --- a/src/bdd/dsd/dsd.h +++ /dev/null @@ -1,129 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsd.h] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [External declarations of the package. - This fast BDD-based recursive algorithm for simple - (single-output) DSD is based on the following papers: - (1) V. Bertacco and M. Damiani, "Disjunctive decomposition of - logic functions," Proc. ICCAD '97, pp. 78-82. - (2) Y. Matsunaga, "An exact and efficient algorithm for disjunctive - decomposition", Proc. SASIMI '98, pp. 44-50. - The scope of detected decompositions is the same as in the paper: - T. Sasao and M. Matsuura, "DECOMPOS: An integrated system for - functional decomposition," Proc. IWLS '98, pp. 471-477.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsd.h,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __DSD_H__ -#define __DSD_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// TYPEDEF DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Dsd_Manager_t_ Dsd_Manager_t; -typedef struct Dsd_Node_t_ Dsd_Node_t; -typedef enum Dsd_Type_t_ Dsd_Type_t; - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -// types of DSD nodes -enum Dsd_Type_t_ { - DSD_NODE_NONE = 0, - DSD_NODE_CONST1 = 1, - DSD_NODE_BUF = 2, - DSD_NODE_OR = 3, - DSD_NODE_EXOR = 4, - DSD_NODE_PRIME = 5, -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -// complementation and testing for pointers for decomposition entries -#define Dsd_IsComplement(p) (((int)((unsigned long) (p) & 01))) -#define Dsd_Regular(p) ((Dsd_Node_t *)((unsigned long)(p) & ~01)) -#define Dsd_Not(p) ((Dsd_Node_t *)((unsigned long)(p) ^ 01)) -#define Dsd_NotCond(p,c) ((Dsd_Node_t *)((unsigned long)(p) ^ (c))) - -//////////////////////////////////////////////////////////////////////// -/// ITERATORS /// -//////////////////////////////////////////////////////////////////////// - -// iterator through the transitions -#define Dsd_NodeForEachChild( Node, Index, Child ) \ - for ( Index = 0; \ - Index < Dsd_NodeReadDecsNum(Node) && \ - ((Child = Dsd_NodeReadDec(Node,Index))>=0); \ - Index++ ) - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== dsdApi.c =======================================================*/ -extern Dsd_Type_t Dsd_NodeReadType( Dsd_Node_t * p ); -extern DdNode * Dsd_NodeReadFunc( Dsd_Node_t * p ); -extern DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p ); -extern Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p ); -extern Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ); -extern int Dsd_NodeReadDecsNum( Dsd_Node_t * p ); -extern int Dsd_NodeReadMark( Dsd_Node_t * p ); -extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); -extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ); -extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ); -extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ); -extern Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ); -/*=== dsdMan.c =======================================================*/ -extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ); -extern void Dsd_ManagerStop( Dsd_Manager_t * dMan ); -/*=== dsdProc.c =======================================================*/ -extern void Dsd_Decompose( Dsd_Manager_t * dMan, DdNode ** pbFuncs, int nFuncs ); -extern Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc ); -/*=== dsdTree.c =======================================================*/ -extern void Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax ); -extern void Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax ); -extern int Dsd_TreeGetAigCost( Dsd_Node_t * pNode ); -extern int Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * dMan ); -extern int Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot ); -extern int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan ); -extern int Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot ); -extern int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, int * pVars ); -extern Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes ); -extern Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ); -extern void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output ); -extern void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ); -/*=== dsdLocal.c =======================================================*/ -extern DdNode * Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c deleted file mode 100644 index d1c90e23..00000000 --- a/src/bdd/dsd/dsdApi.c +++ /dev/null @@ -1,97 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsdApi.c] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [Implementation of API functions.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsdApi.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "dsdInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [APIs of the DSD node.] - - Description [The node's type can be retrieved by calling - Dsd_NodeReadType(). The type is one of the following: constant 1 node, - the buffer (or the elementary variable), OR gate, EXOR gate, or - PRIME function (a non-DSD-decomposable function with more than two - inputs). The return value of Dsd_NodeReadFunc() is the global function - of the DSD node. The return value of Dsd_NodeReadSupp() is the support - of the global function of the DSD node. The array of DSD nodes - returned by Dsd_NodeReadDecs() is the array of decomposition nodes for - the formal inputs of the given node. The number of decomposition entries - returned by Dsd_NodeReadDecsNum() is the number of formal inputs. - The mark is explained below.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Type_t Dsd_NodeReadType( Dsd_Node_t * p ) { return p->Type; } -DdNode * Dsd_NodeReadFunc( Dsd_Node_t * p ) { return p->G; } -DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p ) { return p->S; } -Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p ) { return p->pDecs; } -Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ) { return p->pDecs[i]; } -int Dsd_NodeReadDecsNum( Dsd_Node_t * p ) { return p->nDecs; } -int Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; } - -/**Function************************************************************* - - Synopsis [APIs of the DSD node.] - - Description [This API allows the user to set the integer mark in the - given DSD node. The mark is guaranteed to persist as long as the - calls to the decomposition are not performed. In any case, the mark - is useful to associate the node with some temporary information, such - as its number in the DFS ordered list of the DSD nodes or its number in - the BLIF file that it being written.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; } - -/**Function************************************************************* - - Synopsis [APIs of the DSD manager.] - - Description [Allows the use to get hold of an individual leave of - the DSD tree (Dsd_ManagerReadInput) or an individual root of the - decomposition tree (Dsd_ManagerReadRoot). The root may have the - complemented attribute.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i ) { return pMan->pRoots[i]; } -Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } -Dsd_Node_t * Dsd_ManagerReadConst1( Dsd_Manager_t * pMan ) { return pMan->pConst1; } -DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan ) { return pMan->dd; } - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c deleted file mode 100644 index 58b824d2..00000000 --- a/src/bdd/dsd/dsdCheck.c +++ /dev/null @@ -1,314 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsdCheck.c] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [Procedures to check the identity of root functions.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsdCheck.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "dsdInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Dsd_Cache_t_ Dds_Cache_t; -typedef struct Dsd_Entry_t_ Dsd_Entry_t; - -struct Dsd_Cache_t_ -{ - Dsd_Entry_t * pTable; - int nTableSize; - int nSuccess; - int nFailure; -}; - -struct Dsd_Entry_t_ -{ - DdNode * bX[5]; -}; - -static Dds_Cache_t * pCache; - -static int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function******************************************************************** - - Synopsis [(Re)allocates the local cache.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Dsd_CheckCacheAllocate( int nEntries ) -{ - int nRequested; - - pCache = ALLOC( Dds_Cache_t, 1 ); - memset( pCache, 0, sizeof(Dds_Cache_t) ); - - // check what is the size of the current cache - nRequested = Cudd_Prime( nEntries ); - if ( pCache->nTableSize != nRequested ) - { // the current size is different - // deallocate the old, allocate the new - if ( pCache->nTableSize ) - Dsd_CheckCacheDeallocate(); - // allocate memory for the hash table - pCache->nTableSize = nRequested; - pCache->pTable = ALLOC( Dsd_Entry_t, nRequested ); - } - // otherwise, there is no need to allocate, just clean - Dsd_CheckCacheClear(); -// printf( "\nThe number of allocated cache entries = %d.\n\n", pCache->nTableSize ); -} - -/**Function******************************************************************** - - Synopsis [Deallocates the local cache.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Dsd_CheckCacheDeallocate() -{ - free( pCache->pTable ); - free( pCache ); -} - -/**Function******************************************************************** - - Synopsis [Clears the local cache.] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -void Dsd_CheckCacheClear() -{ - int i; - for ( i = 0; i < pCache->nTableSize; i++ ) - pCache->pTable[0].bX[0] = NULL; -} - - -/**Function******************************************************************** - - Synopsis [Checks whether it is true that bF1(bC1=0) == bF2(bC2=0).] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Dsd_CheckRootFunctionIdentity( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 ) -{ - int RetValue; -// pCache->nSuccess = 0; -// pCache->nFailure = 0; - RetValue = Dsd_CheckRootFunctionIdentity_rec(dd, bF1, bF2, bC1, bC2); -// printf( "Cache success = %d. Cache failure = %d.\n", pCache->nSuccess, pCache->nFailure ); - return RetValue; -} - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Dsd_CheckRootFunctionIdentity().] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 ) -{ - unsigned HKey; - - // if either bC1 or bC2 is zero, the test is true -// if ( bC1 == b0 || bC2 == b0 ) return 1; - assert( bC1 != b0 ); - assert( bC2 != b0 ); - - // if both bC1 and bC2 are one - perform comparison - if ( bC1 == b1 && bC2 == b1 ) return (int)( bF1 == bF2 ); - - if ( bF1 == b0 ) - return Cudd_bddLeq( dd, bC2, Cudd_Not(bF2) ); - - if ( bF1 == b1 ) - return Cudd_bddLeq( dd, bC2, bF2 ); - - if ( bF2 == b0 ) - return Cudd_bddLeq( dd, bC1, Cudd_Not(bF1) ); - - if ( bF2 == b1 ) - return Cudd_bddLeq( dd, bC1, bF1 ); - - // otherwise, keep expanding - - // check cache -// HKey = _Hash( ((unsigned)bF1), ((unsigned)bF2), ((unsigned)bC1), ((unsigned)bC2) ); - HKey = hashKey4( bF1, bF2, bC1, bC2, pCache->nTableSize ); - if ( pCache->pTable[HKey].bX[0] == bF1 && - pCache->pTable[HKey].bX[1] == bF2 && - pCache->pTable[HKey].bX[2] == bC1 && - pCache->pTable[HKey].bX[3] == bC2 ) - { - pCache->nSuccess++; - return (int)pCache->pTable[HKey].bX[4]; // the last bit records the result (yes/no) - } - else - { - - // determine the top variables - int RetValue; - DdNode * bA[4] = { bF1, bF2, bC1, bC2 }; // arguments - DdNode * bAR[4] = { Cudd_Regular(bF1), Cudd_Regular(bF2), Cudd_Regular(bC1), Cudd_Regular(bC2) }; // regular arguments - int CurLevel[4] = { cuddI(dd,bAR[0]->index), cuddI(dd,bAR[1]->index), cuddI(dd,bAR[2]->index), cuddI(dd,bAR[3]->index) }; - int TopLevel = CUDD_CONST_INDEX; - int i; - DdNode * bE[4], * bT[4]; - DdNode * bF1next, * bF2next, * bC1next, * bC2next; - - pCache->nFailure++; - - // determine the top level - for ( i = 0; i < 4; i++ ) - if ( TopLevel > CurLevel[i] ) - TopLevel = CurLevel[i]; - - // compute the cofactors - for ( i = 0; i < 4; i++ ) - if ( TopLevel == CurLevel[i] ) - { - if ( bA[i] != bAR[i] ) // complemented - { - bE[i] = Cudd_Not(cuddE(bAR[i])); - bT[i] = Cudd_Not(cuddT(bAR[i])); - } - else - { - bE[i] = cuddE(bAR[i]); - bT[i] = cuddT(bAR[i]); - } - } - else - bE[i] = bT[i] = bA[i]; - - // solve subproblems - // three cases are possible - - // (1) the top var belongs to both C1 and C2 - // in this case, any cofactor of F1 and F2 will do, - // as long as the corresponding cofactor of C1 and C2 is not equal to 0 - if ( TopLevel == CurLevel[2] && TopLevel == CurLevel[3] ) - { - if ( bE[2] != b0 ) // C1 - { - bF1next = bE[0]; - bC1next = bE[2]; - } - else - { - bF1next = bT[0]; - bC1next = bT[2]; - } - if ( bE[3] != b0 ) // C2 - { - bF2next = bE[1]; - bC2next = bE[3]; - } - else - { - bF2next = bT[1]; - bC2next = bT[3]; - } - RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bF1next, bF2next, bC1next, bC2next ); - } - // (2) the top var belongs to either C1 or C2 - // in this case normal splitting of cofactors - else if ( TopLevel == CurLevel[2] && TopLevel != CurLevel[3] ) - { - if ( bE[2] != b0 ) // C1 - { - bF1next = bE[0]; - bC1next = bE[2]; - } - else - { - bF1next = bT[0]; - bC1next = bT[2]; - } - // split around this variable - RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bF1next, bE[1], bC1next, bE[3] ); - if ( RetValue == 1 ) // test another branch; otherwise, there is no need to test - RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bF1next, bT[1], bC1next, bT[3] ); - } - else if ( TopLevel != CurLevel[2] && TopLevel == CurLevel[3] ) - { - if ( bE[3] != b0 ) // C2 - { - bF2next = bE[1]; - bC2next = bE[3]; - } - else - { - bF2next = bT[1]; - bC2next = bT[3]; - } - // split around this variable - RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bE[0], bF2next, bE[2], bC2next ); - if ( RetValue == 1 ) // test another branch; otherwise, there is no need to test - RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bT[0], bF2next, bT[2], bC2next ); - } - // (3) the top var does not belong to C1 and C2 - // in this case normal splitting of cofactors - else // if ( TopLevel != CurLevel[2] && TopLevel != CurLevel[3] ) - { - // split around this variable - RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bE[0], bE[1], bE[2], bE[3] ); - if ( RetValue == 1 ) // test another branch; otherwise, there is no need to test - RetValue = Dsd_CheckRootFunctionIdentity_rec( dd, bT[0], bT[1], bT[2], bT[3] ); - } - - // set cache - for ( i = 0; i < 4; i++ ) - pCache->pTable[HKey].bX[i] = bA[i]; - pCache->pTable[HKey].bX[4] = (DdNode*)RetValue; - - return RetValue; - } -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h deleted file mode 100644 index 62ce7e99..00000000 --- a/src/bdd/dsd/dsdInt.h +++ /dev/null @@ -1,91 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsdInt.h] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [Internal declarations of the package.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsdInt.h,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __DSD_INT_H__ -#define __DSD_INT_H__ - -#include "extra.h" -#include "dsd.h" - -//////////////////////////////////////////////////////////////////////// -/// TYPEDEF DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef unsigned char byte; - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -// DSD manager -struct Dsd_Manager_t_ -{ - DdManager * dd; // the BDD manager - st_table * Table; // the mapping of BDDs into their DEs - int nInputs; // the number of primary inputs - int nRoots; // the number of primary outputs - int nRootsAlloc;// the number of primary outputs - Dsd_Node_t ** pInputs; // the primary input nodes - Dsd_Node_t ** pRoots; // the primary output nodes - Dsd_Node_t * pConst1; // the constant node - int fVerbose; // the verbosity level -}; - -// DSD node -struct Dsd_Node_t_ -{ - Dsd_Type_t Type; // decomposition type - DdNode * G; // function of the node - DdNode * S; // support of this function - Dsd_Node_t ** pDecs; // pointer to structures for formal inputs - int Mark; // the mark used by CASE 4 of disjoint decomposition - short nDecs; // the number of formal inputs - short nVisits; // the counter of visits -}; - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -#define MAXINPUTS 1000 - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== dsdCheck.c =======================================================*/ -extern void Dsd_CheckCacheAllocate( int nEntries ); -extern void Dsd_CheckCacheDeallocate(); -extern void Dsd_CheckCacheClear(); -extern int Dsd_CheckRootFunctionIdentity( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 ); -/*=== dsdTree.c =======================================================*/ -extern Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum ); -extern void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode ); -extern void Dsd_TreeUnmark( Dsd_Manager_t * dMan ); -extern DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap ); - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - 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 /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c deleted file mode 100644 index 6e43f0f4..00000000 --- a/src/bdd/dsd/dsdMan.c +++ /dev/null @@ -1,114 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsdMan.c] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [APIs of the DSD manager.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsdMan.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "dsdInt.h" - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// API OF DSD MANAGER /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Starts the DSD manager.] - - Description [Takes the started BDD manager and the maximum support size - of the function to be DSD-decomposed. The manager should have at least as - many variables as there are variables in the support. The functions should - be expressed using the first nSuppSizeMax variables in the manager (these - may be ordered not necessarily on top of the manager).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ) -{ - Dsd_Manager_t * dMan; - Dsd_Node_t * pNode; - int i; - - assert( nSuppMax <= dd->size ); - - dMan = ALLOC( Dsd_Manager_t, 1 ); - memset( dMan, 0, sizeof(Dsd_Manager_t) ); - dMan->dd = dd; - dMan->nInputs = nSuppMax; - dMan->fVerbose = fVerbose; - dMan->nRoots = 0; - dMan->nRootsAlloc = 50; - dMan->pRoots = (Dsd_Node_t **) malloc( dMan->nRootsAlloc * sizeof(Dsd_Node_t *) ); - dMan->pInputs = (Dsd_Node_t **) malloc( dMan->nInputs * sizeof(Dsd_Node_t *) ); - - // create the primary inputs and insert them into the table - dMan->Table = st_init_table(st_ptrcmp, st_ptrhash); - for ( i = 0; i < dMan->nInputs; i++ ) - { - pNode = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, 0 ); - pNode->G = dd->vars[i]; Cudd_Ref( pNode->G ); - pNode->S = dd->vars[i]; Cudd_Ref( pNode->S ); - st_insert( dMan->Table, (char*)dd->vars[i], (char*)pNode ); - dMan->pInputs[i] = pNode; - } - pNode = Dsd_TreeNodeCreate( DSD_NODE_CONST1, 0, 0 ); - pNode->G = b1; Cudd_Ref( pNode->G ); - pNode->S = b1; Cudd_Ref( pNode->S ); - st_insert( dMan->Table, (char*)b1, (char*)pNode ); - dMan->pConst1 = pNode; - - Dsd_CheckCacheAllocate( 5000 ); - return dMan; -} - -/**Function************************************************************* - - Synopsis [Stops the DSD manager.] - - Description [Stopping the DSD manager automatically derefereces and - deallocates all the DSD nodes that were created during the life time - of the DSD manager. As a result, the user does not need to deref or - deallocate any DSD nodes or trees that are derived and placed in - the manager while it exists.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_ManagerStop( Dsd_Manager_t * dMan ) -{ - st_generator * gen; - Dsd_Node_t * pNode; - DdNode * bFunc; - // delete the nodes - st_foreach_item( dMan->Table, gen, (char**)&bFunc, (char**)&pNode ) - Dsd_TreeNodeDelete( dMan->dd, Dsd_Regular(pNode) ); - st_free_table(dMan->Table); - free( dMan->pInputs ); - free( dMan->pRoots ); - free( dMan ); - Dsd_CheckCacheDeallocate(); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c deleted file mode 100644 index 543ad387..00000000 --- a/src/bdd/dsd/dsdProc.c +++ /dev/null @@ -1,1617 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsdProc.c] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [The core procedures of the package.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsdProc.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "dsdInt.h" - - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// the most important procedures -void dsdKernelDecompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs ); -static Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * F ); - -// additional procedures -static Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity ); -static int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH ); -static void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor ); -static int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall ); - -// list copying -static void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize ); -static void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int Skipped ); - -// debugging procedures -static int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ); - -//////////////////////////////////////////////////////////////////////// -/// STATIC VARIABLES /// -//////////////////////////////////////////////////////////////////////// - -// the counter of marks -static int s_Mark; - -// debugging flag -static int s_Show = 0; -// temporary var used for debugging -static int Depth = 0; - -static int s_Loops1; -static int s_Loops2; -static int s_Loops3; -static int s_Pivot; -static int s_PivotNo; -static int s_Common; -static int s_CommonNo; - -static int s_Case4Calls; -static int s_Case4CallsSpecial; - -static int s_Case5; -static int s_Loops2Useless; - - -static int s_DecNodesTotal; -static int s_DecNodesUsed; - -// statistical variables -static int s_nDecBlocks; -static int s_nLiterals; -static int s_nExorGates; -static int s_nReusedBlocks; -static int s_nCascades; -static float s_nArea; -static float s_MaxDelay; -static long s_Time; -static int s_nInvertors; -static int s_nPrimeBlocks; - -static int HashSuccess = 0; -static int HashFailure = 0; - -static int s_CacheEntries; - - -//////////////////////////////////////////////////////////////////////// -/// DECOMPOSITION FUNCTIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs DSD for the array of functions represented by BDDs.] - - Description [This function takes the DSD manager, which should be - previously allocated by the call to Dsd_ManagerStart(). The resulting - DSD tree is stored in the DSD manager (pDsdMan->pRoots, pDsdMan->nRoots). - Access to the tree is through the APIs of the manager. The resulting - tree is a shared DSD DAG for the functions given in the array. For one - function the resulting DAG is always a tree. The root node pointers can - be complemented, as discussed in the literature referred to in "dsd.h". - This procedure can be called repeatedly for different functions. There is - no need to remove the decomposition tree after it is returned, because - the next call to the DSD manager will "recycle" the tree. The user should - not modify or dereference any data associated with the nodes of the - DSD trees (the user can only change the contents of a temporary - mark associated with each node by the calling to Dsd_NodeSetMark()). - All the decomposition trees and intermediate nodes will be removed when - the DSD manager is deallocated at the end by calling Dsd_ManagerStop().] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_Decompose( Dsd_Manager_t * pDsdMan, DdNode ** pbFuncs, int nFuncs ) -{ - DdManager * dd = pDsdMan->dd; - int i; - long clk; - Dsd_Node_t * pTemp; - int SumMaxGateSize = 0; - int nDecOutputs = 0; - int nCBFOutputs = 0; -/* -s_Loops1 = 0; -s_Loops2 = 0; -s_Loops3 = 0; -s_Case4Calls = 0; -s_Case4CallsSpecial = 0; -s_Case5 = 0; -s_Loops2Useless = 0; -*/ - // resize the number of roots in the manager - if ( pDsdMan->nRootsAlloc < nFuncs ) - { - if ( pDsdMan->nRootsAlloc > 0 ) - free( pDsdMan->pRoots ); - pDsdMan->nRootsAlloc = nFuncs; - pDsdMan->pRoots = (Dsd_Node_t **) malloc( pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) ); - } - - if ( pDsdMan->fVerbose ) - printf( "\nDecomposability statistics for individual outputs:\n" ); - - // set the counter of decomposition nodes - s_nDecBlocks = 0; - - // perform decomposition for all outputs - clk = clock(); - pDsdMan->nRoots = 0; - s_nCascades = 0; - for ( i = 0; i < nFuncs; i++ ) - { - int nLiteralsPrev; - int nDecBlocksPrev; - int nExorGatesPrev; - int nReusedBlocksPres; - int nCascades; - int MaxBlock; - int nPrimeBlocks; - long clk; - - clk = clock(); - nLiteralsPrev = s_nLiterals; - nDecBlocksPrev = s_nDecBlocks; - nExorGatesPrev = s_nExorGates; - nReusedBlocksPres = s_nReusedBlocks; - nPrimeBlocks = s_nPrimeBlocks; - - pDsdMan->pRoots[ pDsdMan->nRoots++ ] = dsdKernelDecompose_rec( pDsdMan, pbFuncs[i] ); - - Dsd_TreeNodeGetInfoOne( pDsdMan->pRoots[i], &nCascades, &MaxBlock ); - s_nCascades = ddMax( s_nCascades, nCascades ); - pTemp = Dsd_Regular(pDsdMan->pRoots[i]); - if ( pTemp->Type != DSD_NODE_PRIME || pTemp->nDecs != Extra_bddSuppSize(dd,pTemp->S) ) - nDecOutputs++; - if ( MaxBlock < 3 ) - nCBFOutputs++; - SumMaxGateSize += MaxBlock; - - if ( pDsdMan->fVerbose ) - { - printf("#%02d: ", i ); - printf("Ins=%2d. ", Cudd_SupportSize(dd,pbFuncs[i]) ); - printf("Gts=%3d. ", Dsd_TreeCountNonTerminalNodesOne( pDsdMan->pRoots[i] ) ); - printf("Pri=%3d. ", Dsd_TreeCountPrimeNodesOne( pDsdMan->pRoots[i] ) ); - printf("Max=%3d. ", MaxBlock ); - printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres ); - printf("Csc=%2d. ", nCascades ); - printf("T= %.2f s. ", (float)(clock()-clk)/(float)(CLOCKS_PER_SEC) ) ; - printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) ); - printf("\n"); - fflush( stdout ); - } - } - assert( pDsdMan->nRoots == nFuncs ); - - if ( pDsdMan->fVerbose ) - { - printf( "\n" ); - printf( "The cumulative decomposability statistics:\n" ); - printf( " Total outputs = %5d\n", nFuncs ); - printf( " Decomposable outputs = %5d\n", nDecOutputs ); - printf( " Completely decomposable outputs = %5d\n", nCBFOutputs ); - printf( " The sum of max gate sizes = %5d\n", SumMaxGateSize ); - printf( " Shared BDD size = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) ); - printf( " Decomposition entries = %5d\n", st_count( pDsdMan->Table ) ); - printf( " Pure decomposition time = %.2f sec\n", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) ); - } -/* - printf( "s_Loops1 = %d.\n", s_Loops1 ); - printf( "s_Loops2 = %d.\n", s_Loops2 ); - printf( "s_Loops3 = %d.\n", s_Loops3 ); - printf( "s_Case4Calls = %d.\n", s_Case4Calls ); - printf( "s_Case4CallsSpecial = %d.\n", s_Case4CallsSpecial ); - printf( "s_Case5 = %d.\n", s_Case5 ); - printf( "s_Loops2Useless = %d.\n", s_Loops2Useless ); -*/ -} - -/**Function************************************************************* - - Synopsis [Performs decomposition for one function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc ) -{ - return dsdKernelDecompose_rec( pDsdMan, bFunc ); -} - -/**Function************************************************************* - - Synopsis [The main function of this module. Recursive implementation of DSD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Node_t * dsdKernelDecompose_rec( Dsd_Manager_t * pDsdMan, DdNode * bFunc0 ) -{ - DdManager * dd = pDsdMan->dd; - DdNode * bLow; - DdNode * bLowR; - DdNode * bHigh; - - int VarInt; - DdNode * bVarCur; - Dsd_Node_t * pVarCurDE; - // works only if var indices start from 0!!! - DdNode * bSuppNew = NULL, * bTemp; - - int fContained; - int nSuppLH; - int nSuppL; - int nSuppH; - - - - // various decomposition nodes - Dsd_Node_t * pThis, * pL, * pH, * pLR, * pHR; - - Dsd_Node_t * pSmallR, * pLargeR; - Dsd_Node_t * pTableEntry; - - - // treat the complemented case - DdNode * bF = Cudd_Regular(bFunc0); - int fCompF = (int)(bF != bFunc0); - - // check cache - if ( st_lookup( pDsdMan->Table, (char*)bF, (char**)&pTableEntry ) ) - { // the entry is present - HashSuccess++; - return Dsd_NotCond( pTableEntry, fCompF ); - } - HashFailure++; - Depth++; - - // proceed to consider "four cases" - ////////////////////////////////////////////////////////////////////// - // TERMINAL CASES - CASES 1 and 2 - ////////////////////////////////////////////////////////////////////// - bLow = cuddE(bF); - bLowR = Cudd_Regular(bLow); - bHigh = cuddT(bF); - VarInt = bF->index; - bVarCur = dd->vars[VarInt]; - pVarCurDE = pDsdMan->pInputs[VarInt]; - // works only if var indices start from 0!!! - bSuppNew = NULL; - - if ( bLowR->index == CUDD_CONST_INDEX || bHigh->index == CUDD_CONST_INDEX ) - { // one of the cofactors in the constant - if ( bHigh == b1 ) // bHigh cannot be equal to b0, because then it will be complemented - if ( bLow == b0 ) // bLow cannot be equal to b1, because then the node will have bLow == bHigh - ///////////////////////////////////////////////////////////////// - // bLow == 0, bHigh == 1, F = x'&0 + x&1 = x - ///////////////////////////////////////////////////////////////// - { // create the elementary variable node - assert(0); // should be already in the hash table - pThis = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, s_nDecBlocks++ ); - pThis->pDecs[0] = NULL; - } - else // if ( bLow != constant ) - ///////////////////////////////////////////////////////////////// - // bLow != const, bHigh == 1, F = x'&bLow + x&1 = bLow + x --- DSD_NODE_OR(x,bLow) - ///////////////////////////////////////////////////////////////// - { - pL = dsdKernelDecompose_rec( pDsdMan, bLow ); - pLR = Dsd_Regular( pL ); - bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew); - if ( pLR->Type == DSD_NODE_OR && pL == pLR ) // OR and no complement - { // add to the components - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pL->nDecs+1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, pVarCurDE, pL->pDecs, pL->nDecs ); - } - else // all other cases - { // create a new 2-input OR-gate - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 ); - } - } - else // if ( bHigh != const ) // meaning that bLow should be a constant - { - pH = dsdKernelDecompose_rec( pDsdMan, bHigh ); - pHR = Dsd_Regular( pH ); - bSuppNew = Cudd_bddAnd( dd, bVarCur, pHR->S ); Cudd_Ref(bSuppNew); - if ( bLow == b0 ) - ///////////////////////////////////////////////////////////////// - // Low == 0, High != 1, F = x'&0+x&High = (x'+High')'--- NOR(x',High') - ///////////////////////////////////////////////////////////////// - if ( pHR->Type == DSD_NODE_OR && pH != pHR ) // DSD_NODE_OR and complement - { // add to the components - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pHR->nDecs+1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pHR->pDecs, pHR->nDecs ); - pThis = Dsd_Not(pThis); - } - else // all other cases - { // create a new 2-input NOR gate - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); - pH = Dsd_Not(pH); - dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 ); - pThis = Dsd_Not(pThis); - } - else // if ( bLow == b1 ) - ///////////////////////////////////////////////////////////////// - // Low == 1, High != 1, F = x'&1 + x&High = x' + High --- DSD_NODE_OR(x',High) - ///////////////////////////////////////////////////////////////// - if ( pHR->Type == DSD_NODE_OR && pH == pHR ) // OR and no complement - { // add to the components - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, pH->nDecs+1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), pH->pDecs, pH->nDecs ); - } - else // all other cases - { // create a new 2-input OR-gate - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, Dsd_Not(pVarCurDE), &pH, 1 ); - } - } - goto EXIT; - } - // else if ( bLow != const && bHigh != const ) - - // the case of equal cofactors (up to complementation) - if ( bLowR == bHigh ) - ///////////////////////////////////////////////////////////////// - // Low == G, High == G', F = x'&G + x&G' = (x(+)G) --- EXOR(x,Low) - ///////////////////////////////////////////////////////////////// - { - pL = dsdKernelDecompose_rec( pDsdMan, bLow ); - pLR = Dsd_Regular( pL ); - bSuppNew = Cudd_bddAnd( dd, bVarCur, pLR->S ); Cudd_Ref(bSuppNew); - if ( pLR->Type == DSD_NODE_EXOR ) // complemented or not - does not matter! - { // add to the components - pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, pLR->nDecs+1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, pVarCurDE, pLR->pDecs, pLR->nDecs ); - if ( pL != pLR ) - pThis = Dsd_Not( pThis ); - } - else // all other cases - { // create a new 2-input EXOR-gate - pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ ); - if ( pL != pLR ) // complemented - { - dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pLR, 1 ); - pThis = Dsd_Not( pThis ); - } - else // non-complemented - dsdKernelCopyListPlusOne( pThis, pVarCurDE, &pL, 1 ); - } - goto EXIT; - } - - ////////////////////////////////////////////////////////////////////// - // solve subproblems - ////////////////////////////////////////////////////////////////////// - pL = dsdKernelDecompose_rec( pDsdMan, bLow ); - pH = dsdKernelDecompose_rec( pDsdMan, bHigh ); - pLR = Dsd_Regular( pL ); - pHR = Dsd_Regular( pH ); - - assert( pLR->Type == DSD_NODE_BUF || pLR->Type == DSD_NODE_OR || pLR->Type == DSD_NODE_EXOR || pLR->Type == DSD_NODE_PRIME ); - assert( pHR->Type == DSD_NODE_BUF || pHR->Type == DSD_NODE_OR || pHR->Type == DSD_NODE_EXOR || pHR->Type == DSD_NODE_PRIME ); - -/* -if ( Depth == 1 ) -{ -// PRK(bLow,pDecTreeTotal->nInputs); -// PRK(bHigh,pDecTreeTotal->nInputs); -if ( s_Show ) -{ - PRD( pL ); - PRD( pH ); -} -} -*/ - // compute the new support - bTemp = Cudd_bddAnd( dd, pLR->S, pHR->S ); Cudd_Ref( bTemp ); - nSuppL = Extra_bddSuppSize( dd, pLR->S ); - nSuppH = Extra_bddSuppSize( dd, pHR->S ); - nSuppLH = Extra_bddSuppSize( dd, bTemp ); - bSuppNew = Cudd_bddAnd( dd, bTemp, bVarCur ); Cudd_Ref( bSuppNew ); - Cudd_RecursiveDeref( dd, bTemp ); - - - // several possibilities are possible - // (1) support of one component contains another - // (2) none of the supports is contained in another - fContained = dsdKernelCheckContainment( pDsdMan, pLR, pHR, &pLargeR, &pSmallR ); - - ////////////////////////////////////////////////////////////////////// - // CASE 3.b One of the cofactors in a constant (OR and EXOR) - ////////////////////////////////////////////////////////////////////// - // the support of the larger component should contain the support of the smaller - // it is possible to have PRIME function in this role - // for example: F = ITE( a+b, c(+)d, e+f ), F0 = ITE( b, c(+)d, e+f ), F1 = c(+)d - if ( fContained ) - { - Dsd_Node_t * pSmall, * pLarge; - int c, iCompLarge; // the number of the component is Large is equal to the whole of Small - int fLowIsLarge; - - DdNode * bFTemp; // the changed input function - Dsd_Node_t * pDETemp, * pDENew; - - Dsd_Node_t * pComp = NULL; - int nComp; - - if ( pSmallR == pLR ) - { // Low is Small => High is Large - pSmall = pL; - pLarge = pH; - fLowIsLarge = 0; - } - else - { // vice versa - pSmall = pH; - pLarge = pL; - fLowIsLarge = 1; - } - - // treat the situation when the larger is PRIME - if ( pLargeR->Type == DSD_NODE_PRIME ) //&& pLargeR->nDecs != pSmallR->nDecs ) - { - // QUESTION: Is it possible for pLargeR->nDecs > 3 - // and pSmall contained as one of input in pLarge? - // Yes, for example F = a'c + a & MUX(b,c',d) = a'c + abc' + ab'd is non-decomposable - // Consider the function H(a->xy) = F( xy, b, c, d ) - // H0 = H(x=0) = F(0,b,c,d) = c - // H1 = F(x=1) = F(y,b,c,d) - non-decomposable - // - // QUESTION: Is it possible that pLarge is PRIME(3) and pSmall is OR(2), - // which is not contained in PRIME as one input? - // Yes, for example F = abcd + b'c'd' + a'c'd' = PRIME(ab, c, d) - // F(a=0) = c'd' = NOT(OR(a,d)) F(a=1) = bcd + b'c'd' = PRIME(b,c,d) - // To find decomposition, we have to prove that F(a=1)|b=0 = F(a=0) - - // Is it possible that (pLargeR->nDecs == pSmallR->nDecs) and yet this case holds? - // Yes, consider the function such that F(a=0) = PRIME(a,b+c,d,e) and F(a=1) = OR(b,c,d,e) - // They have the same number of inputs and it is possible that they will be the cofactors - // as discribed in the previous example. - - // find the component, which when substituted for 0 or 1, produces the desired result - int g, fFoundComp; // {0,1} depending on whether setting cofactor to 0 or 1 worked out - - DdNode * bLarge, * bSmall; - if ( fLowIsLarge ) - { - bLarge = bLow; - bSmall = bHigh; - } - else - { - bLarge = bHigh; - bSmall = bLow; - } - - for ( g = 0; g < pLargeR->nDecs; g++ ) -// if ( g != c ) - { - pDETemp = pLargeR->pDecs[g]; // cannot be complemented - if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, pDETemp->G, b1 ) ) - { - fFoundComp = 1; - break; - } - - s_Loops1++; - - if ( Dsd_CheckRootFunctionIdentity( dd, bLarge, bSmall, Cudd_Not(pDETemp->G), b1 ) ) - { - fFoundComp = 0; - break; - } - - s_Loops1++; - } - - if ( g != pLargeR->nDecs ) - { // decomposition is found - if ( fFoundComp ) - if ( fLowIsLarge ) - bFTemp = Cudd_bddOr( dd, bVarCur, pLargeR->pDecs[g]->G ); - else - bFTemp = Cudd_bddOr( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G ); - else - if ( fLowIsLarge ) - bFTemp = Cudd_bddAnd( dd, Cudd_Not(bVarCur), pLargeR->pDecs[g]->G ); - else - bFTemp = Cudd_bddAnd( dd, bVarCur, pLargeR->pDecs[g]->G ); - Cudd_Ref( bFTemp ); - - pDENew = dsdKernelDecompose_rec( pDsdMan, bFTemp ); - pDENew = Dsd_Regular( pDENew ); - Cudd_RecursiveDeref( dd, bFTemp ); - - // get the new gate - pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLargeR->nDecs, s_nDecBlocks++ ); - dsdKernelCopyListPlusOneMinusOne( pThis, pDENew, pLargeR->pDecs, pLargeR->nDecs, g ); - goto EXIT; - } - } - - // try to find one component in the pLarger that is equal to the whole of pSmaller - for ( c = 0; c < pLargeR->nDecs; c++ ) - if ( pLargeR->pDecs[c] == pSmall || pLargeR->pDecs[c] == Dsd_Not(pSmall) ) - { - iCompLarge = c; - break; - } - - // assign the equal component - if ( c != pLargeR->nDecs ) // the decomposition is possible! - { - pComp = pLargeR->pDecs[iCompLarge]; - nComp = 1; - } - else // the decomposition is still possible - { // for example F = OR(ab,c,d), F(a=0) = OR(c,d), F(a=1) = OR(b,c,d) - // supp(F0) is contained in supp(F1), Polarity(F(a=0)) == Polarity(F(a=1)) - - // try to find a group of common components - if ( pLargeR->Type == pSmallR->Type && - (pLargeR->Type == DSD_NODE_EXOR || pSmallR->Type == DSD_NODE_OR&& ((pLarge==pLargeR) == (pSmall==pSmallR))) ) - { - Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; - int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLargeR, pSmallR, &pCommon, &pLastDiffL, &pLastDiffH ); - // if all the components of pSmall are contained in pLarge, - // then the decomposition exists - if ( nCommon == pSmallR->nDecs ) - { - pComp = pSmallR; - nComp = pSmallR->nDecs; - } - } - } - - if ( pComp ) // the decomposition is possible! - { -// Dsd_Node_t * pComp = pLargeR->pDecs[iCompLarge]; - Dsd_Node_t * pCompR = Dsd_Regular( pComp ); - int fComp1 = (int)( pLarge != pLargeR ); - int fComp2 = (int)( pComp != pCompR ); - int fComp3 = (int)( pSmall != pSmallR ); - - DdNode * bFuncComp; // the function of the given component - DdNode * bFuncNew; // the function of the input component - - if ( pLargeR->Type == DSD_NODE_OR ) // Figure 4 of Matsunaga's paper - { - // the decomposition exists only if the polarity assignment - // along the paths is the same - if ( (fComp1 ^ fComp2) == fComp3 ) - { // decomposition exists = consider 4 cases - // consideration of cases leads to the following conclusion - // fComp1 gives the polarity of the resulting DSD_NODE_OR gate - // fComp2 gives the polarity of the common component feeding into the DSD_NODE_OR gate - // - // | fComp1 pL/ |pS - // <> .........<=>....... <> | - // | / | - // [OR] [OR] | fComp3 - // / \ fComp2 / | \ | - // <> <> .......<=>... /..|..<> | - // / \ / | \| - // [OR] [C] S1 S2 C - // / \ - // <> \ - // / \ - // [OR] [x] - // / \ - // S1 S2 - // - - - // at this point we have the function F (bFTemp) and the common component C (bFuncComp) - // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0 - // we compute the following R = Exist( F - C, supp(C) ) - bFTemp = (fComp1)? Cudd_Not( bF ): bF; - bFuncComp = (fComp2)? Cudd_Not( pCompR->G ): pCompR->G; - bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bFuncComp), pCompR->S ); Cudd_Ref( bFuncNew ); - - // there is no need to copy the dec entry list first, because pComp is a component - // which will not be destroyed by the recursive call to decomposition - pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); - assert( Dsd_IsComplement(pDENew) ); // follows from the consideration of cases - Cudd_RecursiveDeref( dd, bFuncNew ); - - // get the new gate - if ( nComp == 1 ) - { - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, 2, s_nDecBlocks++ ); - pThis->pDecs[0] = pDENew; - pThis->pDecs[1] = pComp; // takes the complement - } - else - { // pComp is not complemented - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nComp+1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp ); - } - - if ( fComp1 ) - pThis = Dsd_Not( pThis ); - goto EXIT; - } - } - else if ( pLargeR->Type == DSD_NODE_EXOR ) // Figure 5 of Matsunaga's paper (with correction) - { // decomposition always exists = consider 4 cases - - // consideration of cases leads to the following conclusion - // fComp3 gives the COMPLEMENT of the polarity of the resulting EXOR gate - // (if fComp3 is 0, the EXOR gate is complemented, and vice versa) - // - // | fComp1 pL/ |pS - // <> .........<=>....... /....| fComp3 - // | / | - // [XOR] [XOR] | - // / \ fComp2==0 / | \ | - // / \ / | \ | - // / \ / | \| - // [OR] [C] S1 S2 C - // / \ - // <> \ - // / \ - // [XOR] [x] - // / \ - // S1 S2 - // - - assert( fComp2 == 0 ); - // find the functionality of the lower gates - bFTemp = (fComp3)? bF: Cudd_Not( bF ); - bFuncNew = Cudd_bddXor( dd, bFTemp, pComp->G ); Cudd_Ref( bFuncNew ); - - pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); - assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases - Cudd_RecursiveDeref( dd, bFuncNew ); - - // get the new gate - if ( nComp == 1 ) - { - pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, 2, s_nDecBlocks++ ); - pThis->pDecs[0] = pDENew; - pThis->pDecs[1] = pComp; - } - else - { // pComp is not complemented - pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nComp+1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, pDENew, pComp->pDecs, nComp ); - } - - if ( !fComp3 ) - pThis = Dsd_Not( pThis ); - goto EXIT; - } - } - } - - // this case was added to fix the trivial bug found November 4, 2002 in Japan - // by running the example provided by T. Sasao - if ( nSuppLH == nSuppL + nSuppH ) // the supports of the components are disjoint - { - // create a new component of the type ITE( a, pH, pL ) - pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, 3, s_nDecBlocks++ ); - if ( dd->perm[pLR->S->index] < dd->perm[pHR->S->index] ) // pLR is higher in the varible order - { - pThis->pDecs[1] = pLR; - pThis->pDecs[2] = pHR; - } - else // pHR is higher in the varible order - { - pThis->pDecs[1] = pHR; - pThis->pDecs[2] = pLR; - } - // add the first component - pThis->pDecs[0] = pVarCurDE; - goto EXIT; - } - - - ////////////////////////////////////////////////////////////////////// - // CASE 3.a Neither of the cofactors is a constant (OR, EXOR, PRIME) - ////////////////////////////////////////////////////////////////////// - // the component types are identical - // and if they are OR, they are either both complemented or both not complemented - // and if they are PRIME, their dec numbers should be the same - if ( pLR->Type == pHR->Type && - pLR->Type != DSD_NODE_BUF && - (pLR->Type != DSD_NODE_OR || ( pL == pLR && pH == pHR || pL != pLR && pH != pHR ) ) && - (pLR->Type != DSD_NODE_PRIME || pLR->nDecs == pHR->nDecs) ) - { - // array to store common comps in pL and pH - Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; - int nCommon = dsdKernelFindCommonComponents( pDsdMan, pLR, pHR, &pCommon, &pLastDiffL, &pLastDiffH ); - if ( nCommon ) - { - if ( pLR->Type == DSD_NODE_OR ) // Figure 2 of Matsunaga's paper - { // at this point we have the function F and the group of common components C - // to get the remainder, R, in the relationship F = R + C, supp(R) & supp(C) = 0 - // we compute the following R = Exist( F - C, supp(C) ) - - // compute the sum total of the common components and the union of their supports - DdNode * bCommF, * bCommS, * bFTemp, * bFuncNew; - Dsd_Node_t * pDENew; - - dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, &bCommS, 0 ); - Cudd_Ref( bCommF ); - Cudd_Ref( bCommS ); - bFTemp = ( pL != pLR )? Cudd_Not(bF): bF; - - bFuncNew = Cudd_bddAndAbstract( dd, bFTemp, Cudd_Not(bCommF), bCommS ); Cudd_Ref( bFuncNew ); - Cudd_RecursiveDeref( dd, bCommF ); - Cudd_RecursiveDeref( dd, bCommS ); - - // get the new gate - - // copy the components first, then call the decomposition - // because decomposition will distroy the list used for copying - pThis = Dsd_TreeNodeCreate( DSD_NODE_OR, nCommon + 1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon ); - - // call the decomposition recursively - pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); -// assert( !Dsd_IsComplement(pDENew) ); // follows from the consideration of cases - Cudd_RecursiveDeref( dd, bFuncNew ); - - // add the first component - pThis->pDecs[0] = pDENew; - - if ( pL != pLR ) - pThis = Dsd_Not( pThis ); - goto EXIT; - } - else - if ( pLR->Type == DSD_NODE_EXOR ) // Figure 3 of Matsunaga's paper - { - // compute the sum total of the common components and the union of their supports - DdNode * bCommF, * bFuncNew; - Dsd_Node_t * pDENew; - int fCompExor; - - dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, 1 ); - Cudd_Ref( bCommF ); - - bFuncNew = Cudd_bddXor( dd, bF, bCommF ); Cudd_Ref( bFuncNew ); - Cudd_RecursiveDeref( dd, bCommF ); - - // get the new gate - - // copy the components first, then call the decomposition - // because decomposition will distroy the list used for copying - pThis = Dsd_TreeNodeCreate( DSD_NODE_EXOR, nCommon + 1, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon ); - - // call the decomposition recursively - pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); - Cudd_RecursiveDeref( dd, bFuncNew ); - - // remember the fact that it was complemented - fCompExor = Dsd_IsComplement(pDENew); - pDENew = Dsd_Regular(pDENew); - - // add the first component - pThis->pDecs[0] = pDENew; - - - if ( fCompExor ) - pThis = Dsd_Not( pThis ); - goto EXIT; - } - else - if ( pLR->Type == DSD_NODE_PRIME && (nCommon == pLR->nDecs-1 || nCommon == pLR->nDecs) ) - { - // for example the function F(a,b,c,d) = ITE(b,c,a(+)d) produces - // two cofactors F(a=0) = PRIME(b,c,d) and F(a=1) = PRIME(b,c,d) - // with exactly the same list of common components - - Dsd_Node_t * pDENew; - DdNode * bFuncNew; - int fCompComp = 0; // this flag can be {0,1,2} - // if it is 0 there is no identity - // if it is 1/2, the cofactored functions are equal in the direct/complemented polarity - - if ( nCommon == pLR->nDecs ) - { // all the components are the same - // find the formal input, in which pLow and pHigh differ (if such input exists) - int m; - Dsd_Node_t * pTempL, * pTempH; - - s_Common++; - for ( m = 0; m < pLR->nDecs; m++ ) - { - pTempL = pLR->pDecs[m]; // cannot be complemented - pTempH = pHR->pDecs[m]; // cannot be complemented - - if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pTempL->G, Cudd_Not(pTempH->G) ) && - Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pTempL->G), pTempH->G ) ) - { - pLastDiffL = pTempL; - pLastDiffH = pTempH; - assert( pLastDiffL == pLastDiffH ); - fCompComp = 2; - break; - } - - s_Loops2++; - s_Loops2++; -/* - if ( s_Loops2 % 10000 == 0 ) - { - int i; - for ( i = 0; i < pLR->nDecs; i++ ) - printf( " %d(s=%d)", pLR->pDecs[i]->Type, - Extra_bddSuppSize(dd, pLR->pDecs[i]->S) ); - printf( "\n" ); - } -*/ - - } -// if ( pLR->nDecs == Extra_bddSuppSize(dd, pLR->S) ) -// s_Loops2Useless += pLR->nDecs * 2; - - if ( fCompComp ) - { // put the equal components into pCommon, so that they could be copied into the new dec entry - nCommon = 0; - for ( m = 0; m < pLR->nDecs; m++ ) - if ( pLR->pDecs[m] != pLastDiffL ) - pCommon[nCommon++] = pLR->pDecs[m]; - assert( nCommon = pLR->nDecs-1 ); - } - } - else - { // the differing components are known - check that they have compatible PRIME function - - s_CommonNo++; - - // find the numbers of different components - assert( pLastDiffL ); - assert( pLastDiffH ); - // also, they cannot be complemented, because the decomposition type is PRIME - - if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), Cudd_Not(pLastDiffH->G) ) && - Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, pLastDiffH->G ) ) - fCompComp = 1; - else if ( Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, pLastDiffL->G, Cudd_Not(pLastDiffH->G) ) && - Dsd_CheckRootFunctionIdentity( dd, bLow, bHigh, Cudd_Not(pLastDiffL->G), pLastDiffH->G ) ) - fCompComp = 2; - - s_Loops3 += 4; - } - - if ( fCompComp ) - { - if ( fCompComp == 1 ) // it is true that bLow(G=0) == bHigh(H=0) && bLow(G=1) == bHigh(H=1) - bFuncNew = Cudd_bddIte( dd, bVarCur, pLastDiffH->G, pLastDiffL->G ); - else // it is true that bLow(G=0) == bHigh(H=1) && bLow(G=1) == bHigh(H=0) - bFuncNew = Cudd_bddIte( dd, bVarCur, Cudd_Not(pLastDiffH->G), pLastDiffL->G ); - Cudd_Ref( bFuncNew ); - - // get the new gate - - // copy the components first, then call the decomposition - // because decomposition will distroy the list used for copying - pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, pLR->nDecs, s_nDecBlocks++ ); - dsdKernelCopyListPlusOne( pThis, NULL, pCommon, nCommon ); - - // create a new component - pDENew = dsdKernelDecompose_rec( pDsdMan, bFuncNew ); - Cudd_RecursiveDeref( dd, bFuncNew ); - // the BDD of the argument function in PRIME decomposition, should be regular - pDENew = Dsd_Regular(pDENew); - - // add the first component - pThis->pDecs[0] = pDENew; - goto EXIT; - } - } // end of PRIME type - } // end of existing common components - } // end of CASE 3.a - -// if ( Depth != 1) -// { - -//CASE4: - ////////////////////////////////////////////////////////////////////// - // CASE 4 - ////////////////////////////////////////////////////////////////////// - { - // estimate the number of entries in the list - int nEntriesMax = pDsdMan->nInputs - dd->perm[VarInt]; - - // create the new decomposition entry - int nEntries = 0; - - DdNode * SuppL, * SuppH, * SuppL_init, * SuppH_init; - Dsd_Node_t *pHigher, *pLower, * pTemp, * pDENew; - - - int levTopSuppL; - int levTopSuppH; - int levTop; - - pThis = Dsd_TreeNodeCreate( DSD_NODE_PRIME, nEntriesMax, s_nDecBlocks++ ); - pThis->pDecs[ nEntries++ ] = pVarCurDE; - // other entries will be added to this list one-by-one during analysis - - // count how many times does it happen that the decomposition entries are - s_Case4Calls++; - - // consider the simplest case: when the supports are equal - // and at least one of the components - // is the PRIME without decompositions, or - // when both of them are without decomposition - if ( (((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) || (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) && pLR->S == pHR->S) || - ((pLR->Type == DSD_NODE_PRIME && nSuppL == pLR->nDecs) && (pHR->Type == DSD_NODE_PRIME && nSuppH == pHR->nDecs)) ) - { - - s_Case4CallsSpecial++; - // walk through both supports and create the decomposition list composed of simple entries - SuppL = pLR->S; - SuppH = pHR->S; - do - { - // determine levels - levTopSuppL = cuddI(dd,SuppL->index); - levTopSuppH = cuddI(dd,SuppH->index); - - // skip the topmost variable in both supports - if ( levTopSuppL <= levTopSuppH ) - { - levTop = levTopSuppL; - SuppL = cuddT(SuppL); - } - else - levTop = levTopSuppH; - - if ( levTopSuppH <= levTopSuppL ) - SuppH = cuddT(SuppH); - - // set the new decomposition entry - pThis->pDecs[ nEntries++ ] = pDsdMan->pInputs[ dd->invperm[levTop] ]; - } - while ( SuppL != b1 || SuppH != b1 ); - } - else - { - - // compare two different decomposition lists - SuppL_init = pLR->S; - SuppH_init = pHR->S; - // start references (because these supports will change) - SuppL = pLR->S; Cudd_Ref( SuppL ); - SuppH = pHR->S; Cudd_Ref( SuppH ); - while ( SuppL != b1 || SuppH != b1 ) - { - // determine the top level in cofactors and - // whether they have the same top level - int TopLevL = cuddI(dd,SuppL->index); - int TopLevH = cuddI(dd,SuppH->index); - int TopLevel = TopLevH; - int fEqualLevel = 0; - - DdNode * bVarTop; - DdNode * bSuppSubract; - - - if ( TopLevL < TopLevH ) - { - pHigher = pLR; - pLower = pHR; - TopLevel = TopLevL; - } - else if ( TopLevL > TopLevH ) - { - pHigher = pHR; - pLower = pLR; - } - else - fEqualLevel = 1; - assert( TopLevel != CUDD_CONST_INDEX ); - - - // find the currently top variable in the decomposition lists - bVarTop = dd->vars[dd->invperm[TopLevel]]; - - if ( !fEqualLevel ) - { - // find the lower support - DdNode * bSuppLower = (TopLevL < TopLevH)? SuppH_init: SuppL_init; - - // find the first component in pHigher - // whose support does not overlap with supp(Lower) - // and remember the previous component - int fPolarity; - Dsd_Node_t * pPrev = NULL; // the pointer to the component proceeding pCur - Dsd_Node_t * pCur = pHigher; // the first component not contained in supp(Lower) - while ( Extra_bddSuppOverlapping( dd, pCur->S, bSuppLower ) ) - { // get the next component - pPrev = pCur; - pCur = dsdKernelFindContainingComponent( pDsdMan, pCur, bVarTop, &fPolarity ); - }; - - // look for the possibility to subtract more than one component - if ( pPrev == NULL || pPrev->Type == DSD_NODE_PRIME ) - { // if there is no previous component, or if the previous component is PRIME - // there is no way to subtract more than one component - - // add the new decomposition entry (it is already regular) - pThis->pDecs[ nEntries++ ] = pCur; - // assign the support to be subtracted from both components - bSuppSubract = pCur->S; - } - else // all other types - { - // go through the decomposition list of pPrev and find components - // whose support does not overlap with supp(Lower) - - static Dsd_Node_t * pNonOverlap[MAXINPUTS]; - int i, nNonOverlap = 0; - for ( i = 0; i < pPrev->nDecs; i++ ) - { - pTemp = Dsd_Regular( pPrev->pDecs[i] ); - if ( !Extra_bddSuppOverlapping( dd, pTemp->S, bSuppLower ) ) - pNonOverlap[ nNonOverlap++ ] = pPrev->pDecs[i]; - } - assert( nNonOverlap > 0 ); - - if ( nNonOverlap == 1 ) - { // one one component was found, which is the original one - assert( Dsd_Regular(pNonOverlap[0]) == pCur); - // add the new decomposition entry - pThis->pDecs[ nEntries++ ] = pCur; - // assign the support to be subtracted from both components - bSuppSubract = pCur->S; - } - else // more than one components was found - { - // find the OR (EXOR) of the non-overlapping components - DdNode * bCommF; - dsdKernelComputeSumOfComponents( pDsdMan, pNonOverlap, nNonOverlap, &bCommF, NULL, (int)(pPrev->Type==DSD_NODE_EXOR) ); - Cudd_Ref( bCommF ); - - // create a new gated - pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF ); - Cudd_RecursiveDeref(dd, bCommF); - // make it regular... it must be regular already - assert( !Dsd_IsComplement(pDENew) ); - - // add the new decomposition entry - pThis->pDecs[ nEntries++ ] = pDENew; - // assign the support to be subtracted from both components - bSuppSubract = pDENew->S; - } - } - - // subtract its support from the support of upper component - if ( TopLevL < TopLevH ) - { - SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ); Cudd_Ref( SuppL ); - Cudd_RecursiveDeref(dd, bTemp); - } - else - { - SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ); Cudd_Ref( SuppH ); - Cudd_RecursiveDeref(dd, bTemp); - } - } // end of if ( !fEqualLevel ) - else // if ( fEqualLevel ) -- they have the same top level var - { - static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks - static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks - int nMarkedLeft = 0; - - int fPolarity = 0; - Dsd_Node_t * pTempL = pLR; - - int fPolarityCurH = 0; - Dsd_Node_t * pPrevH = NULL, * pCurH = pHR; - - int fPolarityCurL = 0; - Dsd_Node_t * pPrevL = NULL, * pCurL = pLR; // = pMarkedLeft[0]; - int index = 1; - - // set the new mark - s_Mark++; - - // go over the dec list of pL, mark all components that contain the given variable - assert( Extra_bddSuppContainVar( dd, pLR->S, bVarTop ) ); - assert( Extra_bddSuppContainVar( dd, pHR->S, bVarTop ) ); - do { - pTempL->Mark = s_Mark; - pMarkedLeft[ nMarkedLeft ] = pTempL; - pMarkedPols[ nMarkedLeft ] = fPolarity; - nMarkedLeft++; - } while ( pTempL = dsdKernelFindContainingComponent( pDsdMan, pTempL, bVarTop, &fPolarity ) ); - - // go over the dec list of pH, and find the component that is marked and the previos one - // (such component always exists, because they have common variables) - while ( pCurH->Mark != s_Mark ) - { - pPrevH = pCurH; - pCurH = dsdKernelFindContainingComponent( pDsdMan, pCurH, bVarTop, &fPolarityCurH ); - assert( pCurH ); - } - - // go through the first list once again and find - // the component proceeding the one marked found in the second list - while ( pCurL != pCurH ) - { - pPrevL = pCurL; - pCurL = pMarkedLeft[index]; - fPolarityCurL = pMarkedPols[index]; - index++; - } - - // look for the possibility to subtract more than one component - if ( !pPrevL || !pPrevH || pPrevL->Type != pPrevH->Type || pPrevL->Type == DSD_NODE_PRIME || fPolarityCurL != fPolarityCurH ) - { // there is no way to extract more than one - pThis->pDecs[ nEntries++ ] = pCurH; - // assign the support to be subtracted from both components - bSuppSubract = pCurH->S; - } - else - { - // find the equal components in two decomposition lists - Dsd_Node_t ** pCommon, * pLastDiffL = NULL, * pLastDiffH = NULL; - int nCommon = dsdKernelFindCommonComponents( pDsdMan, pPrevL, pPrevH, &pCommon, &pLastDiffL, &pLastDiffH ); - - if ( nCommon == 0 || nCommon == 1 ) - { // one one component was found, which is the original one - // assert( Dsd_Regular(pCommon[0]) == pCurL); - // add the new decomposition entry - pThis->pDecs[ nEntries++ ] = pCurL; - // assign the support to be subtracted from both components - bSuppSubract = pCurL->S; - } - else // more than one components was found - { - // find the OR (EXOR) of the non-overlapping components - DdNode * bCommF; - dsdKernelComputeSumOfComponents( pDsdMan, pCommon, nCommon, &bCommF, NULL, (int)(pPrevL->Type==DSD_NODE_EXOR) ); - Cudd_Ref( bCommF ); - - pDENew = dsdKernelDecompose_rec( pDsdMan, bCommF ); - assert( !Dsd_IsComplement(pDENew) ); // cannot be complemented because of construction - Cudd_RecursiveDeref( dd, bCommF ); - - // add the new decomposition entry - pThis->pDecs[ nEntries++ ] = pDENew; - - // assign the support to be subtracted from both components - bSuppSubract = pDENew->S; - } - } - - SuppL = Cudd_bddExistAbstract( dd, bTemp = SuppL, bSuppSubract ), Cudd_Ref( SuppL ); - Cudd_RecursiveDeref(dd, bTemp); - - SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH ); - Cudd_RecursiveDeref(dd, bTemp); - - } // end of if ( fEqualLevel ) - - } // end of decomposition list comparison - Cudd_RecursiveDeref( dd, SuppL ); - Cudd_RecursiveDeref( dd, SuppH ); - - } - - // check that the estimation of the number of entries was okay - assert( nEntries <= nEntriesMax ); - -// if ( nEntries != Extra_bddSuppSize(dd, bSuppNew) ) -// s_Case5++; - - // update the number of entries in the new decomposition list - pThis->nDecs = nEntries; - } -//} -EXIT: - - { - // if the component created is complemented, it represents a function without complement - // therefore, as it is, without complement, it should recieve the complemented function - Dsd_Node_t * pThisR = Dsd_Regular( pThis ); - assert( pThisR->G == NULL ); - assert( pThisR->S == NULL ); - - if ( pThisR == pThis ) // set regular function - pThisR->G = bF; - else // set complemented function - pThisR->G = Cudd_Not(bF); - Cudd_Ref(bF); // reference the function in the component - - assert( bSuppNew ); - pThisR->S = bSuppNew; // takes the reference from the new support - if ( st_insert( pDsdMan->Table, (char*)bF, (char*)pThis ) ) - { - assert( 0 ); - } - s_CacheEntries++; - - -/* - if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 ) - { - // write the function, for which verification does not work - cout << endl << "Internal verification failed!"" ); - - // create the variable mask - static int s_pVarMask[MAXINPUTS]; - int nInputCounter = 0; - - Cudd_SupportArray( dd, bF, s_pVarMask ); - int k; - for ( k = 0; k < dd->size; k++ ) - if ( s_pVarMask[k] ) - nInputCounter++; - - cout << endl << "The problem function is "" ); - - DdNode * zNewFunc = Cudd_zddIsopCover( dd, bF, bF ); Cudd_Ref( zNewFunc ); - cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask ); - Cudd_RecursiveDerefZdd( dd, zNewFunc ); - } -*/ - - } - - Depth--; - return Dsd_NotCond( pThis, fCompF ); -} - - -//////////////////////////////////////////////////////////////////////// -/// OTHER FUNCTIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Finds the corresponding decomposition entry.] - - Description [This function returns the non-complemented pointer to the - DecEntry of that component which contains the given variable in its - support, or NULL if no such component exists] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pWhere, DdNode * Var, int * fPolarity ) - -{ - Dsd_Node_t * pTemp; - int i; - -// assert( !Dsd_IsComplement( pWhere ) ); -// assert( Extra_bddSuppContainVar( pDsdMan->dd, pWhere->S, Var ) ); - - if ( pWhere->nDecs == 1 ) - return NULL; - - for( i = 0; i < pWhere->nDecs; i++ ) - { - pTemp = Dsd_Regular( pWhere->pDecs[i] ); - if ( Extra_bddSuppContainVar( pDsdMan->dd, pTemp->S, Var ) ) - { - *fPolarity = (int)( pTemp != pWhere->pDecs[i] ); - return pTemp; - } - } - assert( 0 ); - return NULL; -} - -/**Function************************************************************* - - Synopsis [Find the common decomposition components.] - - Description [This function determines the common components. It counts - the number of common components in the decomposition lists of pL and pH - and returns their number and the lists of common components. It assumes - that pL and pH are regular pointers. It retuns also the pointers to the - last different components encountered in pL and pH.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH ) -{ - static Dsd_Node_t * Common[MAXINPUTS]; - int nCommon = 0; - - // pointers to the current decomposition entries - Dsd_Node_t * pLcur; - Dsd_Node_t * pHcur; - - // the pointers to their supports - DdNode * bSLcur; - DdNode * bSHcur; - - // the top variable in the supports - int TopVar; - - // the indices running through the components - int iCurL = 0; - int iCurH = 0; - while ( iCurL < pL->nDecs && iCurH < pH->nDecs ) - { // both did not run out - - pLcur = Dsd_Regular(pL->pDecs[iCurL]); - pHcur = Dsd_Regular(pH->pDecs[iCurH]); - - bSLcur = pLcur->S; - bSHcur = pHcur->S; - - // find out what component is higher in the BDD - if ( pDsdMan->dd->perm[bSLcur->index] < pDsdMan->dd->perm[bSHcur->index] ) - TopVar = bSLcur->index; - else - TopVar = bSHcur->index; - - if ( TopVar == bSLcur->index && TopVar == bSHcur->index ) - { - // the components may be equal - should match exactly! - if ( pL->pDecs[iCurL] == pH->pDecs[iCurH] ) - Common[nCommon++] = pL->pDecs[iCurL]; - else - { - *pLastDiffL = pL->pDecs[iCurL]; - *pLastDiffH = pH->pDecs[iCurH]; - } - - // skip both - iCurL++; - iCurH++; - } - else if ( TopVar == bSLcur->index ) - { // the components cannot be equal - // skip the top-most one - *pLastDiffL = pL->pDecs[iCurL++]; - } - else // if ( TopVar == bSHcur->index ) - { // the components cannot be equal - // skip the top-most one - *pLastDiffH = pH->pDecs[iCurH++]; - } - } - - // if one of the lists still has components, write the first one down - if ( iCurL < pL->nDecs ) - *pLastDiffL = pL->pDecs[iCurL]; - - if ( iCurH < pH->nDecs ) - *pLastDiffH = pH->pDecs[iCurH]; - - // return the pointer to the array - *pCommon = Common; - // return the number of common components - return nCommon; -} - -/**Function************************************************************* - - Synopsis [Computes the sum (OR or EXOR) of the functions of the components.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void dsdKernelComputeSumOfComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t ** pCommon, int nCommon, DdNode ** pCompF, DdNode ** pCompS, int fExor ) -{ - DdManager * dd = pDsdMan->dd; - DdNode * bF, * bS, * bFadd, * bTemp; - Dsd_Node_t * pDE, * pDER; - int i; - - // start the function - bF = b0; Cudd_Ref( bF ); - // start the support - if ( pCompS ) - bS = b1, Cudd_Ref( bS ); - - assert( nCommon > 0 ); - for ( i = 0; i < nCommon; i++ ) - { - pDE = pCommon[i]; - pDER = Dsd_Regular( pDE ); - bFadd = (pDE != pDER)? Cudd_Not(pDER->G): pDER->G; - // add to the function - if ( fExor ) - bF = Cudd_bddXor( dd, bTemp = bF, bFadd ); - else - bF = Cudd_bddOr( dd, bTemp = bF, bFadd ); - Cudd_Ref( bF ); - Cudd_RecursiveDeref( dd, bTemp ); - if ( pCompS ) - { - // add to the support - bS = Cudd_bddAnd( dd, bTemp = bS, pDER->S ); Cudd_Ref( bS ); - Cudd_RecursiveDeref( dd, bTemp ); - } - } - // return the function - Cudd_Deref( bF ); - *pCompF = bF; - - // return the support - if ( pCompS ) - Cudd_Deref( bS ), *pCompS = bS; -} - -/**Function************************************************************* - - Synopsis [Checks support containment of the decomposition components.] - - Description [This function returns 1 if support of one component is contained - in that of another. In this case, pLarge (pSmall) is assigned to point to the - larger (smaller) support. If the supports are identical return 0, and does not - assign the components.] -] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int dsdKernelCheckContainment( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t ** pLarge, Dsd_Node_t ** pSmall ) -{ - DdManager * dd = pDsdMan->dd; - DdNode * bSuppLarge, * bSuppSmall; - int RetValue; - - RetValue = Extra_bddSuppCheckContainment( dd, pL->S, pH->S, &bSuppLarge, &bSuppSmall ); - - if ( RetValue == 0 ) - return 0; - - if ( pH->S == bSuppLarge ) - { - *pLarge = pH; - *pSmall = pL; - } - else // if ( pL->S == bSuppLarge ) - { - *pLarge = pL; - *pSmall = pH; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Copies the list of components plus one.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void dsdKernelCopyListPlusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize ) -{ - int i; - assert( nListSize+1 == p->nDecs ); - p->pDecs[0] = First; - for( i = 0; i < nListSize; i++ ) - p->pDecs[i+1] = ppList[i]; -} - -/**Function************************************************************* - - Synopsis [Copies the list of components plus one, and skips one.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void dsdKernelCopyListPlusOneMinusOne( Dsd_Node_t * p, Dsd_Node_t * First, Dsd_Node_t ** ppList, int nListSize, int iSkipped ) -{ - int i, Counter; - assert( nListSize == p->nDecs ); - p->pDecs[0] = First; - for( i = 0, Counter = 1; i < nListSize; i++ ) - if ( i != iSkipped ) - p->pDecs[Counter++] = ppList[i]; -} - -/**Function************************************************************* - - Synopsis [Debugging procedure to compute the functionality of the decomposed structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE ) -{ - DdManager * dd = pDsdMan->dd; - Dsd_Node_t * pR = Dsd_Regular(pDE); - int fCompP = (int)( pDE != pR ); - int RetValue; - - DdNode * bRes; - if ( pR->Type == DSD_NODE_CONST1 ) - bRes = b1; - else if ( pR->Type == DSD_NODE_BUF ) - bRes = pR->G; - else if ( pR->Type == DSD_NODE_OR || pR->Type == DSD_NODE_EXOR ) - dsdKernelComputeSumOfComponents( pDsdMan, pR->pDecs, pR->nDecs, &bRes, NULL, (int)(pR->Type == DSD_NODE_EXOR) ); - else if ( pR->Type == DSD_NODE_PRIME ) - { - int i; - static DdNode * bGVars[MAXINPUTS]; - // transform the function of this block, so that it depended on inputs - // corresponding to the formal inputs - DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 ); Cudd_Ref( bNewFunc ); - - // compose this function with the inputs - // create the elementary permutation - for ( i = 0; i < dd->size; i++ ) - bGVars[i] = dd->vars[i]; - - // assign functions to be composed - for ( i = 0; i < pR->nDecs; i++ ) - bGVars[dd->invperm[i]] = pR->pDecs[i]->G; - - // perform the composition - bRes = Cudd_bddVectorCompose( dd, bNewFunc, bGVars ); Cudd_Ref( bRes ); - Cudd_RecursiveDeref( dd, bNewFunc ); - - ///////////////////////////////////////////////////////// - RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) ); - ///////////////////////////////////////////////////////// - Cudd_Deref( bRes ); - } - else - { - assert(0); - } - - Cudd_Ref( bRes ); - RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) ); - Cudd_RecursiveDeref( dd, bRes ); - return RetValue; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c deleted file mode 100644 index 2855d68d..00000000 --- a/src/bdd/dsd/dsdTree.c +++ /dev/null @@ -1,1068 +0,0 @@ -/**CFile**************************************************************** - - FileName [dsdTree.c] - - PackageName [DSD: Disjoint-support decomposition package.] - - Synopsis [Managing the decomposition tree.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 8.0. Started - September 22, 2003.] - - Revision [$Id: dsdTree.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "dsdInt.h" - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Dsd_TreeUnmark_rec( Dsd_Node_t * pNode ); -static void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur ); -static int Dsd_TreeCountNonTerminalNodes_rec( Dsd_Node_t * pNode ); -static int Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode ); -static int Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars ); -static void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes ); -static void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fCcmp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames ); -static void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter ); - -//////////////////////////////////////////////////////////////////////// -/// STATIC VARIABLES /// -//////////////////////////////////////////////////////////////////////// - -static int s_DepthMax; -static int s_GateSizeMax; - -static int s_CounterBlocks; -static int s_CounterPos; -static int s_CounterNeg; -static int s_CounterNo; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Create the DSD node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum ) -{ - // allocate memory for this node - Dsd_Node_t * p = (Dsd_Node_t *) malloc( sizeof(Dsd_Node_t) ); - memset( p, 0, sizeof(Dsd_Node_t) ); - p->Type = Type; // the type of this block - p->nDecs = nDecs; // the number of decompositions - if ( p->nDecs ) - { - p->pDecs = (Dsd_Node_t **) malloc( p->nDecs * sizeof(Dsd_Node_t *) ); - p->pDecs[0] = NULL; - } - return p; -} - -/**Function************************************************************* - - Synopsis [Frees the DSD node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode ) -{ - if ( pNode->G ) Cudd_RecursiveDeref( dd, pNode->G ); - if ( pNode->S ) Cudd_RecursiveDeref( dd, pNode->S ); - FREE( pNode->pDecs ); - FREE( pNode ); -} - -/**Function************************************************************* - - Synopsis [Unmarks the decomposition tree.] - - Description [This function assumes that originally pNode->nVisits are - set to zero!] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreeUnmark( Dsd_Manager_t * pDsdMan ) -{ - int i; - for ( i = 0; i < pDsdMan->nRoots; i++ ) - Dsd_TreeUnmark_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ); -} - - -/**Function************************************************************* - - Synopsis [Recursive unmarking.] - - Description [This function should be called with a non-complemented - pointer.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreeUnmark_rec( Dsd_Node_t * pNode ) -{ - int i; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->nVisits > 0 ); - - if ( --pNode->nVisits ) // if this is not the last visit, return - return; - - // upon the last visit, go through the list of successors and call recursively - if ( pNode->Type != DSD_NODE_BUF && pNode->Type != DSD_NODE_CONST1 ) - for ( i = 0; i < pNode->nDecs; i++ ) - Dsd_TreeUnmark_rec( Dsd_Regular(pNode->pDecs[i]) ); -} - -/**Function************************************************************* - - Synopsis [Getting information about the node.] - - Description [This function computes the max depth and the max gate size - of the tree rooted at the node.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreeNodeGetInfo( Dsd_Manager_t * pDsdMan, int * DepthMax, int * GateSizeMax ) -{ - int i; - s_DepthMax = 0; - s_GateSizeMax = 0; - - for ( i = 0; i < pDsdMan->nRoots; i++ ) - Dsd_TreeGetInfo_rec( Dsd_Regular( pDsdMan->pRoots[i] ), 0 ); - - if ( DepthMax ) - *DepthMax = s_DepthMax; - if ( GateSizeMax ) - *GateSizeMax = s_GateSizeMax; -} - -/**Function************************************************************* - - Synopsis [Getting information about the node.] - - Description [This function computes the max depth and the max gate size - of the tree rooted at the node.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax ) -{ - s_DepthMax = 0; - s_GateSizeMax = 0; - - Dsd_TreeGetInfo_rec( Dsd_Regular(pNode), 0 ); - - if ( DepthMax ) - *DepthMax = s_DepthMax; - if ( GateSizeMax ) - *GateSizeMax = s_GateSizeMax; -} - - -/**Function************************************************************* - - Synopsis [Performs the recursive step of Dsd_TreeNodeGetInfo().] - - Description [pNode is the node, for the tree rooted in which we are - determining info. RankCur is the current rank to assign to the node. - fSetRank is the flag saying whether the rank will be written in the - node. s_DepthMax is the maximum depths of the tree. s_GateSizeMax is - the maximum gate size.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur ) -{ - int i; - int GateSize; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->nVisits >= 0 ); - - // we don't want the two-input gates to count for non-decomposable blocks - if ( pNode->Type == DSD_NODE_OR || - pNode->Type == DSD_NODE_EXOR ) - GateSize = 2; - else - GateSize = pNode->nDecs; - - // update the max size of the node - if ( s_GateSizeMax < GateSize ) - s_GateSizeMax = GateSize; - - if ( pNode->nDecs < 2 ) - return; - - // update the max rank - if ( s_DepthMax < RankCur+1 ) - s_DepthMax = RankCur+1; - - // call recursively - for ( i = 0; i < pNode->nDecs; i++ ) - Dsd_TreeGetInfo_rec( Dsd_Regular(pNode->pDecs[i]), RankCur+1 ); -} - -/**Function************************************************************* - - Synopsis [Counts AIG nodes needed to implement this node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeGetAigCost_rec( Dsd_Node_t * pNode ) -{ - int i, Counter = 0; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->nVisits >= 0 ); - - if ( pNode->nDecs < 2 ) - return 0; - - // we don't want the two-input gates to count for non-decomposable blocks - if ( pNode->Type == DSD_NODE_OR ) - Counter += pNode->nDecs - 1; - else if ( pNode->Type == DSD_NODE_EXOR ) - Counter += 3*(pNode->nDecs - 1); - else if ( pNode->Type == DSD_NODE_PRIME && pNode->nDecs == 3 ) - Counter += 3; - - // call recursively - for ( i = 0; i < pNode->nDecs; i++ ) - Counter += Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode->pDecs[i]) ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Counts AIG nodes needed to implement this node.] - - Description [Assumes that the only primes of the DSD tree are MUXes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeGetAigCost( Dsd_Node_t * pNode ) -{ - return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) ); -} - -/**Function************************************************************* - - Synopsis [Counts non-terminal nodes of the DSD tree.] - - Description [Nonterminal nodes include all the nodes with the - support more than 1. These are OR, EXOR, and PRIME nodes. They - do not include the elementary variable nodes and the constant 1 - node.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * pDsdMan ) -{ - int Counter, i; - Counter = 0; - for ( i = 0; i < pDsdMan->nRoots; i++ ) - Counter += Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ); - Dsd_TreeUnmark( pDsdMan ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot ) -{ - int Counter = 0; - - // go through the list of successors and call recursively - Counter = Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular(pRoot) ); - - Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) ); - return Counter; -} - - -/**Function************************************************************* - - Synopsis [Counts non-terminal nodes for one root.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCountNonTerminalNodes_rec( Dsd_Node_t * pNode ) -{ - int i; - int Counter = 0; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->nVisits >= 0 ); - - if ( pNode->nVisits++ ) // if this is not the first visit, return zero - return 0; - - if ( pNode->nDecs <= 1 ) - return 0; - - // upon the first visit, go through the list of successors and call recursively - for ( i = 0; i < pNode->nDecs; i++ ) - Counter += Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular(pNode->pDecs[i]) ); - - return Counter + 1; -} - - -/**Function************************************************************* - - Synopsis [Counts prime nodes of the DSD tree.] - - Description [Prime nodes are nodes with the support more than 2, - that is not an OR or EXOR gate.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan ) -{ - int Counter, i; - Counter = 0; - for ( i = 0; i < pDsdMan->nRoots; i++ ) - Counter += Dsd_TreeCountPrimeNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) ); - Dsd_TreeUnmark( pDsdMan ); - return Counter; -} - -/**Function************************************************************* - - Synopsis [Counts prime nodes for one root.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot ) -{ - int Counter = 0; - - // go through the list of successors and call recursively - Counter = Dsd_TreeCountPrimeNodes_rec( Dsd_Regular(pRoot) ); - - Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) ); - return Counter; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode ) -{ - int i; - int Counter = 0; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - assert( pNode->nVisits >= 0 ); - - if ( pNode->nVisits++ ) // if this is not the first visit, return zero - return 0; - - if ( pNode->nDecs <= 1 ) - return 0; - - // upon the first visit, go through the list of successors and call recursively - for ( i = 0; i < pNode->nDecs; i++ ) - Counter += Dsd_TreeCountPrimeNodes_rec( Dsd_Regular(pNode->pDecs[i]) ); - - if ( pNode->Type == DSD_NODE_PRIME ) - Counter++; - - return Counter; -} - - -/**Function************************************************************* - - Synopsis [Collects the decomposable vars on the PI side.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * pDsdMan, int * pVars ) -{ - int nVars; - - // set the vars collected to 0 - nVars = 0; - Dsd_TreeCollectDecomposableVars_rec( pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[0]), pVars, &nVars ); - // return the number of collected vars - return nVars; -} - -/**Function************************************************************* - - Synopsis [Implements the recursive part of Dsd_TreeCollectDecomposableVars().] - - Description [Adds decomposable variables as they are found to pVars and increments - nVars. Returns 1 if a non-dec node with more than 4 inputs was encountered - in the processed subtree. Returns 0, otherwise. ] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars ) -{ - int fSkipThisNode, i; - Dsd_Node_t * pTemp; - int fVerbose = 0; - - assert( pNode ); - assert( !Dsd_IsComplement( pNode ) ); - - if ( pNode->nDecs <= 1 ) - return 0; - - // go through the list of successors and call recursively - fSkipThisNode = 0; - for ( i = 0; i < pNode->nDecs; i++ ) - if ( Dsd_TreeCollectDecomposableVars_rec(dd, Dsd_Regular(pNode->pDecs[i]), pVars, nVars) ) - fSkipThisNode = 1; - - if ( !fSkipThisNode && (pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR || pNode->nDecs <= 4) ) - { -if ( fVerbose ) -printf( "Node of type <%d> (OR=6,EXOR=8,RAND=1): ", pNode->Type ); - - for ( i = 0; i < pNode->nDecs; i++ ) - { - pTemp = Dsd_Regular(pNode->pDecs[i]); - if ( pTemp->Type == DSD_NODE_BUF ) - { - if ( pVars ) - pVars[ (*nVars)++ ] = pTemp->S->index; - else - (*nVars)++; - -if ( fVerbose ) -printf( "%d ", pTemp->S->index ); - } - } -if ( fVerbose ) -printf( "\n" ); - } - else - fSkipThisNode = 1; - - - return fSkipThisNode; -} - - -/**Function************************************************************* - - Synopsis [Creates the DFS ordered array of DSD nodes in the tree.] - - Description [The collected nodes do not include the terminal nodes - and the constant 1 node. The array of nodes is returned. The number - of entries in the array is returned in the variale pnNodes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes ) -{ - Dsd_Node_t ** ppNodes; - int nNodes, nNodesAlloc; - int i; - - nNodesAlloc = Dsd_TreeCountNonTerminalNodes(pDsdMan); - nNodes = 0; - ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc ); - for ( i = 0; i < pDsdMan->nRoots; i++ ) - Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pDsdMan->pRoots[i]), ppNodes, &nNodes ); - Dsd_TreeUnmark( pDsdMan ); - assert( nNodesAlloc == nNodes ); - *pnNodes = nNodes; - return ppNodes; -} - -/**Function************************************************************* - - Synopsis [Creates the DFS ordered array of DSD nodes in the tree.] - - Description [The collected nodes do not include the terminal nodes - and the constant 1 node. The array of nodes is returned. The number - of entries in the array is returned in the variale pnNodes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes ) -{ - Dsd_Node_t ** ppNodes; - int nNodes, nNodesAlloc; - nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode); - nNodes = 0; - ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc ); - Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes ); - Dsd_TreeUnmark_rec(Dsd_Regular(pNode)); - assert( nNodesAlloc == nNodes ); - *pnNodes = nNodes; - return ppNodes; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes ) -{ - int i; - assert( pNode ); - assert( !Dsd_IsComplement(pNode) ); - assert( pNode->nVisits >= 0 ); - - if ( pNode->nVisits++ ) // if this is not the first visit, return zero - return; - if ( pNode->nDecs <= 1 ) - return; - - // upon the first visit, go through the list of successors and call recursively - for ( i = 0; i < pNode->nDecs; i++ ) - Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode->pDecs[i]), ppNodes, pnNodes ); - - ppNodes[ (*pnNodes)++ ] = pNode; -} - -/**Function************************************************************* - - Synopsis [Prints the decompostion tree into file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * pDsdMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output ) -{ - Dsd_Node_t * pNode; - int SigCounter; - int i; - SigCounter = 1; - - if ( Output == -1 ) - { - for ( i = 0; i < pDsdMan->nRoots; i++ ) - { - pNode = Dsd_Regular( pDsdMan->pRoots[i] ); - Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], 0, &SigCounter, fShortNames ); - } - } - else - { - assert( Output >= 0 && Output < pDsdMan->nRoots ); - pNode = Dsd_Regular( pDsdMan->pRoots[Output] ); - Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], 0, &SigCounter, fShortNames ); - } -} - -/**Function************************************************************* - - Synopsis [Prints the decompostion tree into file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames ) -{ - char Buffer[100]; - Dsd_Node_t * pInput; - int * pInputNums; - int fCompNew, i; - - assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || - pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); - - Extra_PrintSymbols( pFile, ' ', nOffset, 0 ); - if ( !fComp ) - fprintf( pFile, "%s = ", pOutputName ); - else - fprintf( pFile, "NOT(%s) = ", pOutputName ); - pInputNums = ALLOC( int, pNode->nDecs ); - if ( pNode->Type == DSD_NODE_CONST1 ) - { - fprintf( pFile, " Constant 1.\n" ); - } - else if ( pNode->Type == DSD_NODE_BUF ) - { - if ( fShortNames ) - fprintf( pFile, "%d", 'a' + pNode->S->index ); - else - fprintf( pFile, "%s", pInputNames[pNode->S->index] ); - fprintf( pFile, "\n" ); - } - else if ( pNode->Type == DSD_NODE_PRIME ) - { - // print the line - fprintf( pFile, "PRIME(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - if ( i ) - fprintf( pFile, "," ); - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - if ( fShortNames ) - fprintf( pFile, "%d", pInput->S->index ); - else - fprintf( pFile, "%s", pInputNames[pInput->S->index] ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, "<%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, ")" ); - } - fprintf( pFile, " )\n" ); - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); - } - } - else if ( pNode->Type == DSD_NODE_OR ) - { - // print the line - fprintf( pFile, "OR(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - if ( i ) - fprintf( pFile, "," ); - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - if ( fShortNames ) - fprintf( pFile, "%c", 'a' + pInput->S->index ); - else - fprintf( pFile, "%s", pInputNames[pInput->S->index] ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, "<%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, ")" ); - } - fprintf( pFile, " )\n" ); - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); - } - } - else if ( pNode->Type == DSD_NODE_EXOR ) - { - // print the line - fprintf( pFile, "EXOR(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - if ( i ) - fprintf( pFile, "," ); - if ( fCompNew ) - fprintf( pFile, " NOT(" ); - else - fprintf( pFile, " " ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - if ( fShortNames ) - fprintf( pFile, "%c", 'a' + pInput->S->index ); - else - fprintf( pFile, "%s", pInputNames[pInput->S->index] ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, "<%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, ")" ); - } - fprintf( pFile, " )\n" ); - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames ); - } - } - free( pInputNums ); -} - -/**Function************************************************************* - - Synopsis [Prints the decompostion tree into file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode ) -{ - Dsd_Node_t * pNodeR; - int SigCounter = 1; - pNodeR = Dsd_Regular(pNode); - Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter ); -} - -/**Function************************************************************* - - Synopsis [Prints one node of the decomposition tree.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter ) -{ - char Buffer[100]; - Dsd_Node_t * pInput; - int * pInputNums; - int fCompNew, i; - - assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || - pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); - - Extra_PrintSymbols( pFile, ' ', nOffset, 0 ); - if ( !fComp ) - fprintf( pFile, "%s = ", pOutputName ); - else - fprintf( pFile, "NOT(%s) = ", pOutputName ); - pInputNums = ALLOC( int, pNode->nDecs ); - if ( pNode->Type == DSD_NODE_CONST1 ) - { - fprintf( pFile, " Constant 1.\n" ); - } - else if ( pNode->Type == DSD_NODE_BUF ) - { - fprintf( pFile, " " ); - fprintf( pFile, "%c", 'a' + pNode->S->index ); - fprintf( pFile, "\n" ); - } - else if ( pNode->Type == DSD_NODE_PRIME ) - { - // print the line - fprintf( pFile, "PRIME(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - assert( fCompNew == 0 ); - if ( i ) - fprintf( pFile, "," ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - fprintf( pFile, " %c", 'a' + pInput->S->index ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, " <%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, "\'" ); - } - fprintf( pFile, " )\n" ); -/* - fprintf( pFile, " ) " ); - { - DdNode * bLocal; - bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd ); Cudd_Ref( bLocal ); - Extra_bddPrint( dd, bLocal ); - Cudd_RecursiveDeref( dd, bLocal ); - } -*/ - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); - } - } - else if ( pNode->Type == DSD_NODE_OR ) - { - // print the line - fprintf( pFile, "OR(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - if ( i ) - fprintf( pFile, "," ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - fprintf( pFile, " %c", 'a' + pInput->S->index ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, " <%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, "\'" ); - } - fprintf( pFile, " )\n" ); - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); - } - } - else if ( pNode->Type == DSD_NODE_EXOR ) - { - // print the line - fprintf( pFile, "EXOR(" ); - for ( i = 0; i < pNode->nDecs; i++ ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - fCompNew = (int)( pInput != pNode->pDecs[i] ); - assert( fCompNew == 0 ); - if ( i ) - fprintf( pFile, "," ); - if ( pInput->Type == DSD_NODE_BUF ) - { - pInputNums[i] = 0; - fprintf( pFile, " %c", 'a' + pInput->S->index ); - } - else - { - pInputNums[i] = (*pSigCounter)++; - fprintf( pFile, " <%d>", pInputNums[i] ); - } - if ( fCompNew ) - fprintf( pFile, "\'" ); - } - fprintf( pFile, " )\n" ); - // call recursively for the following blocks - for ( i = 0; i < pNode->nDecs; i++ ) - if ( pInputNums[i] ) - { - pInput = Dsd_Regular( pNode->pDecs[i] ); - sprintf( Buffer, "<%d>", pInputNums[i] ); - Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter ); - } - } - free( pInputNums ); -} - - -/**Function************************************************************* - - Synopsis [Retuns the function of one node of the decomposition tree.] - - Description [This is the old procedure. It is now superceded by the - procedure Dsd_TreeGetPrimeFunction() found in "dsdLocal.c".] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Dsd_TreeGetPrimeFunctionOld( 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 == DSD_NODE_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 != DSD_NODE_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; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// diff --git a/src/bdd/dsd/module.make b/src/bdd/dsd/module.make deleted file mode 100644 index f5e6673d..00000000 --- a/src/bdd/dsd/module.make +++ /dev/null @@ -1,6 +0,0 @@ -SRC += src/bdd/dsd/dsdApi.c \ - src/bdd/dsd/dsdCheck.c \ - src/bdd/dsd/dsdLocal.c \ - src/bdd/dsd/dsdMan.c \ - src/bdd/dsd/dsdProc.c \ - src/bdd/dsd/dsdTree.c |