summaryrefslogtreecommitdiffstats
path: root/src/bdd/dsd
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/dsd')
-rw-r--r--src/bdd/dsd/dsd.h129
-rw-r--r--src/bdd/dsd/dsdApi.c97
-rw-r--r--src/bdd/dsd/dsdCheck.c314
-rw-r--r--src/bdd/dsd/dsdInt.h91
-rw-r--r--src/bdd/dsd/dsdLocal.c337
-rw-r--r--src/bdd/dsd/dsdMan.c114
-rw-r--r--src/bdd/dsd/dsdProc.c1617
-rw-r--r--src/bdd/dsd/dsdTree.c1068
-rw-r--r--src/bdd/dsd/module.make6
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