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, 3773 insertions, 0 deletions
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h new file mode 100644 index 00000000..b73b81ab --- /dev/null +++ b/src/bdd/dsd/dsd.h @@ -0,0 +1,129 @@ +/**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 new file mode 100644 index 00000000..d1c90e23 --- /dev/null +++ b/src/bdd/dsd/dsdApi.c @@ -0,0 +1,97 @@ +/**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 new file mode 100644 index 00000000..58b824d2 --- /dev/null +++ b/src/bdd/dsd/dsdCheck.c @@ -0,0 +1,314 @@ +/**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 new file mode 100644 index 00000000..62ce7e99 --- /dev/null +++ b/src/bdd/dsd/dsdInt.h @@ -0,0 +1,91 @@ +/**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 new file mode 100644 index 00000000..6dd6e7d1 --- /dev/null +++ b/src/bdd/dsd/dsdLocal.c @@ -0,0 +1,337 @@ +/**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 new file mode 100644 index 00000000..6e43f0f4 --- /dev/null +++ b/src/bdd/dsd/dsdMan.c @@ -0,0 +1,114 @@ +/**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 new file mode 100644 index 00000000..543ad387 --- /dev/null +++ b/src/bdd/dsd/dsdProc.c @@ -0,0 +1,1617 @@ +/**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 new file mode 100644 index 00000000..2855d68d --- /dev/null +++ b/src/bdd/dsd/dsdTree.c @@ -0,0 +1,1068 @@ +/**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 new file mode 100644 index 00000000..f5e6673d --- /dev/null +++ b/src/bdd/dsd/module.make @@ -0,0 +1,6 @@ +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 |