src/bdd/dsd/dsd.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Defines

#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)))
#define Dsd_NodeForEachChild(Node, Index, Child)

Typedefs

typedef struct Dsd_Manager_t_ Dsd_Manager_t
typedef struct Dsd_Node_t_ Dsd_Node_t
typedef enum Dsd_Type_t_ Dsd_Type_t

Enumerations

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
}

Functions

Dsd_Type_t Dsd_NodeReadType (Dsd_Node_t *p)
DdNode * Dsd_NodeReadFunc (Dsd_Node_t *p)
DdNode * Dsd_NodeReadSupp (Dsd_Node_t *p)
Dsd_Node_t ** Dsd_NodeReadDecs (Dsd_Node_t *p)
Dsd_Node_t * Dsd_NodeReadDec (Dsd_Node_t *p, int i)
int Dsd_NodeReadDecsNum (Dsd_Node_t *p)
int Dsd_NodeReadMark (Dsd_Node_t *p)
void Dsd_NodeSetMark (Dsd_Node_t *p, int Mark)
DdManager * Dsd_ManagerReadDd (Dsd_Manager_t *pMan)
Dsd_Node_t * Dsd_ManagerReadRoot (Dsd_Manager_t *pMan, int i)
Dsd_Node_t * Dsd_ManagerReadInput (Dsd_Manager_t *pMan, int i)
Dsd_Node_t * Dsd_ManagerReadConst1 (Dsd_Manager_t *pMan)
Dsd_Manager_t * Dsd_ManagerStart (DdManager *dd, int nSuppMax, int fVerbose)
void Dsd_ManagerStop (Dsd_Manager_t *dMan)
void Dsd_Decompose (Dsd_Manager_t *dMan, DdNode **pbFuncs, int nFuncs)
Dsd_Node_t * Dsd_DecomposeOne (Dsd_Manager_t *pDsdMan, DdNode *bFunc)
void Dsd_TreeNodeGetInfo (Dsd_Manager_t *dMan, int *DepthMax, int *GateSizeMax)
void Dsd_TreeNodeGetInfoOne (Dsd_Node_t *pNode, int *DepthMax, int *GateSizeMax)
int Dsd_TreeGetAigCost (Dsd_Node_t *pNode)
int Dsd_TreeCountNonTerminalNodes (Dsd_Manager_t *dMan)
int Dsd_TreeCountNonTerminalNodesOne (Dsd_Node_t *pRoot)
int Dsd_TreeCountPrimeNodes (Dsd_Manager_t *pDsdMan)
int Dsd_TreeCountPrimeNodesOne (Dsd_Node_t *pRoot)
int Dsd_TreeCollectDecomposableVars (Dsd_Manager_t *dMan, int *pVars)
Dsd_Node_t ** Dsd_TreeCollectNodesDfs (Dsd_Manager_t *dMan, int *pnNodes)
Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne (Dsd_Manager_t *pDsdMan, Dsd_Node_t *pNode, int *pnNodes)
void Dsd_TreePrint (FILE *pFile, Dsd_Manager_t *dMan, char *pInputNames[], char *pOutputNames[], int fShortNames, int Output)
void Dsd_NodePrint (FILE *pFile, Dsd_Node_t *pNode)
DdNode * Dsd_TreeGetPrimeFunction (DdManager *dd, Dsd_Node_t *pNode)

Define Documentation

#define Dsd_IsComplement ( p   )     (((int)((unsigned long) (p) & 01)))

MACRO DEFINITIONS ///

Definition at line 66 of file dsd.h.

#define Dsd_NodeForEachChild ( Node,
Index,
Child   ) 
Value:
for ( Index = 0;                                      \
          Index < Dsd_NodeReadDecsNum(Node) &&            \
             ((Child = Dsd_NodeReadDec(Node,Index))>=0);  \
          Index++ )

ITERATORS ///

Definition at line 76 of file dsd.h.

#define Dsd_Not ( p   )     ((Dsd_Node_t *)((unsigned long)(p) ^ 01))

Definition at line 68 of file dsd.h.

#define Dsd_NotCond ( p,
c   )     ((Dsd_Node_t *)((unsigned long)(p) ^ (c)))

Definition at line 69 of file dsd.h.

#define Dsd_Regular ( p   )     ((Dsd_Node_t *)((unsigned long)(p) & ~01))

Definition at line 67 of file dsd.h.

Typedef Documentation

typedef struct Dsd_Manager_t_ Dsd_Manager_t

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

] TYPEDEF DEFINITIONS ///

Definition at line 39 of file dsd.h.

typedef struct Dsd_Node_t_ Dsd_Node_t

Definition at line 40 of file dsd.h.

typedef enum Dsd_Type_t_ Dsd_Type_t

Definition at line 41 of file dsd.h.

Enumeration Type Documentation

enum Dsd_Type_t_

STRUCTURE DEFINITIONS /// PARAMETERS ///

Enumerator:
DSD_NODE_NONE 
DSD_NODE_CONST1 
DSD_NODE_BUF 
DSD_NODE_OR 
DSD_NODE_EXOR 
DSD_NODE_PRIME 

Definition at line 52 of file dsd.h.

00052                  { 
00053         DSD_NODE_NONE   = 0,
00054         DSD_NODE_CONST1 = 1,
00055         DSD_NODE_BUF    = 2,
00056         DSD_NODE_OR     = 3,
00057         DSD_NODE_EXOR   = 4,
00058         DSD_NODE_PRIME  = 5,
00059 };

Function Documentation

void Dsd_Decompose ( Dsd_Manager_t *  pDsdMan,
DdNode **  pbFuncs,
int  nFuncs 
)

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 []

Definition at line 120 of file dsdProc.c.

00121 {
00122         DdManager * dd = pDsdMan->dd;
00123         int i;
00124         long clk;
00125         Dsd_Node_t * pTemp;
00126         int SumMaxGateSize = 0;
00127         int nDecOutputs = 0;
00128         int nCBFOutputs = 0;
00129 /*
00130 s_Loops1 = 0;
00131 s_Loops2 = 0;
00132 s_Loops3 = 0;
00133 s_Case4Calls = 0;
00134 s_Case4CallsSpecial = 0;
00135 s_Case5 = 0;
00136 s_Loops2Useless = 0;
00137 */
00138         // resize the number of roots in the manager
00139         if ( pDsdMan->nRootsAlloc < nFuncs )
00140         {
00141                 if ( pDsdMan->nRootsAlloc > 0 )
00142                         free( pDsdMan->pRoots );
00143                 pDsdMan->nRootsAlloc = nFuncs;
00144                 pDsdMan->pRoots = (Dsd_Node_t **) malloc( pDsdMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
00145         }
00146 
00147         if ( pDsdMan->fVerbose )
00148                 printf( "\nDecomposability statistics for individual outputs:\n" );
00149 
00150         // set the counter of decomposition nodes
00151         s_nDecBlocks = 0;
00152 
00153         // perform decomposition for all outputs
00154         clk = clock();
00155         pDsdMan->nRoots = 0;
00156         s_nCascades = 0;
00157         for ( i = 0; i < nFuncs; i++ )
00158         {
00159                 int nLiteralsPrev;
00160                 int nDecBlocksPrev;
00161                 int nExorGatesPrev;
00162                 int nReusedBlocksPres;
00163                 int nCascades;
00164                 int MaxBlock;
00165                 int nPrimeBlocks;
00166                 long clk;
00167 
00168                 clk = clock();
00169                 nLiteralsPrev     = s_nLiterals;
00170                 nDecBlocksPrev    = s_nDecBlocks;
00171                 nExorGatesPrev    = s_nExorGates;
00172                 nReusedBlocksPres = s_nReusedBlocks;
00173                 nPrimeBlocks      = s_nPrimeBlocks;
00174 
00175                 pDsdMan->pRoots[ pDsdMan->nRoots++ ] = dsdKernelDecompose_rec( pDsdMan, pbFuncs[i] );
00176 
00177                 Dsd_TreeNodeGetInfoOne( pDsdMan->pRoots[i], &nCascades, &MaxBlock );
00178                 s_nCascades = ddMax( s_nCascades, nCascades );
00179                 pTemp = Dsd_Regular(pDsdMan->pRoots[i]);
00180                 if ( pTemp->Type != DSD_NODE_PRIME || pTemp->nDecs != Extra_bddSuppSize(dd,pTemp->S) )
00181                         nDecOutputs++;
00182                 if ( MaxBlock < 3 )
00183                         nCBFOutputs++;
00184                 SumMaxGateSize += MaxBlock;
00185 
00186                 if ( pDsdMan->fVerbose )
00187                 {
00188                         printf("#%02d: ", i );                              
00189                         printf("Ins=%2d. ", Cudd_SupportSize(dd,pbFuncs[i]) );                  
00190                         printf("Gts=%3d. ", Dsd_TreeCountNonTerminalNodesOne( pDsdMan->pRoots[i] ) ); 
00191                         printf("Pri=%3d. ", Dsd_TreeCountPrimeNodesOne( pDsdMan->pRoots[i] ) ); 
00192                         printf("Max=%3d. ", MaxBlock ); 
00193                         printf("Reuse=%2d. ", s_nReusedBlocks-nReusedBlocksPres ); 
00194                         printf("Csc=%2d. ", nCascades ); 
00195                         printf("T= %.2f s. ", (float)(clock()-clk)/(float)(CLOCKS_PER_SEC) ) ;
00196                         printf("Bdd=%2d. ", Cudd_DagSize(pbFuncs[i]) ); 
00197                         printf("\n");
00198                         fflush( stdout );
00199                 }
00200         }
00201         assert( pDsdMan->nRoots == nFuncs );
00202 
00203         if ( pDsdMan->fVerbose )
00204         {
00205                 printf( "\n" );
00206                 printf( "The cumulative decomposability statistics:\n" );
00207                 printf( "  Total outputs                             = %5d\n", nFuncs );
00208                 printf( "  Decomposable outputs                      = %5d\n", nDecOutputs );
00209                 printf( "  Completely decomposable outputs           = %5d\n", nCBFOutputs );
00210                 printf( "  The sum of max gate sizes                 = %5d\n", SumMaxGateSize );
00211                 printf( "  Shared BDD size                           = %5d\n", Cudd_SharingSize( pbFuncs, nFuncs ) );
00212                 printf( "  Decomposition entries                     = %5d\n", st_count( pDsdMan->Table ) );
00213                 printf( "  Pure decomposition time                   =  %.2f sec\n", (float)(clock() - clk)/(float)(CLOCKS_PER_SEC) );
00214         }
00215 /*
00216     printf( "s_Loops1 = %d.\n", s_Loops1 );
00217     printf( "s_Loops2 = %d.\n", s_Loops2 );
00218     printf( "s_Loops3 = %d.\n", s_Loops3 );
00219     printf( "s_Case4Calls = %d.\n", s_Case4Calls );
00220     printf( "s_Case4CallsSpecial = %d.\n", s_Case4CallsSpecial );
00221     printf( "s_Case5 = %d.\n", s_Case5 );
00222     printf( "s_Loops2Useless = %d.\n", s_Loops2Useless );
00223 */
00224 }

Dsd_Node_t* Dsd_DecomposeOne ( Dsd_Manager_t *  pDsdMan,
DdNode *  bFunc 
)

Function*************************************************************

Synopsis [Performs decomposition for one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file dsdProc.c.

00238 {
00239     return dsdKernelDecompose_rec( pDsdMan, bFunc );
00240 }

Dsd_Node_t* Dsd_ManagerReadConst1 ( Dsd_Manager_t *  pMan  ) 

Definition at line 92 of file dsdApi.c.

00092 { return pMan->pConst1;    }

DdManager* Dsd_ManagerReadDd ( Dsd_Manager_t *  pMan  ) 

Definition at line 93 of file dsdApi.c.

00093 { return pMan->dd;         }

Dsd_Node_t* Dsd_ManagerReadInput ( Dsd_Manager_t *  pMan,
int  i 
)

Definition at line 91 of file dsdApi.c.

00091 { return pMan->pInputs[i]; }

Dsd_Node_t* Dsd_ManagerReadRoot ( Dsd_Manager_t *  pMan,
int  i 
)

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 []

Definition at line 90 of file dsdApi.c.

00090 { return pMan->pRoots[i];  }

Dsd_Manager_t* Dsd_ManagerStart ( DdManager *  dd,
int  nSuppMax,
int  fVerbose 
)

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

] 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 []

Definition at line 44 of file dsdMan.c.

00045 {
00046         Dsd_Manager_t * dMan;
00047         Dsd_Node_t * pNode;
00048         int i;
00049 
00050         assert( nSuppMax <= dd->size );
00051 
00052         dMan = ALLOC( Dsd_Manager_t, 1 );
00053         memset( dMan, 0, sizeof(Dsd_Manager_t) );
00054         dMan->dd          = dd;
00055         dMan->nInputs     = nSuppMax;
00056         dMan->fVerbose    = fVerbose;
00057         dMan->nRoots      = 0;
00058         dMan->nRootsAlloc = 50;
00059         dMan->pRoots      = (Dsd_Node_t **) malloc( dMan->nRootsAlloc * sizeof(Dsd_Node_t *) );
00060         dMan->pInputs     = (Dsd_Node_t **) malloc( dMan->nInputs     * sizeof(Dsd_Node_t *) );
00061 
00062         // create the primary inputs and insert them into the table
00063         dMan->Table       = st_init_table(st_ptrcmp, st_ptrhash);
00064         for ( i = 0; i < dMan->nInputs; i++ )
00065         {
00066                 pNode = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, 0 );
00067                 pNode->G = dd->vars[i];  Cudd_Ref( pNode->G );
00068                 pNode->S = dd->vars[i];  Cudd_Ref( pNode->S );
00069                 st_insert( dMan->Table, (char*)dd->vars[i], (char*)pNode );
00070                 dMan->pInputs[i] = pNode;
00071         }
00072         pNode = Dsd_TreeNodeCreate( DSD_NODE_CONST1, 0, 0 );
00073         pNode->G = b1;  Cudd_Ref( pNode->G );
00074         pNode->S = b1;  Cudd_Ref( pNode->S );
00075         st_insert( dMan->Table, (char*)b1, (char*)pNode );
00076     dMan->pConst1 = pNode;
00077 
00078         Dsd_CheckCacheAllocate( 5000 );
00079         return dMan;
00080 }

void Dsd_ManagerStop ( Dsd_Manager_t *  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 []

Definition at line 97 of file dsdMan.c.

00098 {
00099         st_generator * gen;
00100         Dsd_Node_t * pNode;
00101         DdNode * bFunc;
00102         // delete the nodes
00103         st_foreach_item( dMan->Table, gen, (char**)&bFunc, (char**)&pNode )
00104                 Dsd_TreeNodeDelete( dMan->dd, Dsd_Regular(pNode) );
00105         st_free_table(dMan->Table);
00106         free( dMan->pInputs );
00107         free( dMan->pRoots );
00108         free( dMan );
00109         Dsd_CheckCacheDeallocate();
00110 }

void Dsd_NodePrint ( FILE *  pFile,
Dsd_Node_t *  pNode 
)

Function*************************************************************

Synopsis [Prints the decompostion tree into file.]

Description []

SideEffects []

SeeAlso []

Definition at line 837 of file dsdTree.c.

00838 {
00839     Dsd_Node_t * pNodeR;
00840         int SigCounter = 1;
00841         pNodeR = Dsd_Regular(pNode);
00842         Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter );
00843 }

Dsd_Node_t* Dsd_NodeReadDec ( Dsd_Node_t *  p,
int  i 
)

Definition at line 54 of file dsdApi.c.

00054 { return p->pDecs[i]; }

Dsd_Node_t** Dsd_NodeReadDecs ( Dsd_Node_t *  p  ) 

Definition at line 53 of file dsdApi.c.

00053 { return p->pDecs;    }

int Dsd_NodeReadDecsNum ( Dsd_Node_t *  p  ) 

Definition at line 55 of file dsdApi.c.

00055 { return p->nDecs;    }

DdNode* Dsd_NodeReadFunc ( Dsd_Node_t *  p  ) 

Definition at line 51 of file dsdApi.c.

00051 { return p->G;        }

int Dsd_NodeReadMark ( Dsd_Node_t *  p  ) 

Definition at line 56 of file dsdApi.c.

00056 { return p->Mark;     }

DdNode* Dsd_NodeReadSupp ( Dsd_Node_t *  p  ) 

Definition at line 52 of file dsdApi.c.

00052 { return p->S;        }

Dsd_Type_t Dsd_NodeReadType ( Dsd_Node_t *  p  ) 

FUNCTION DEFINITIONS ///

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

] 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 []

Definition at line 50 of file dsdApi.c.

00050 { return p->Type;     }

void Dsd_NodeSetMark ( Dsd_Node_t *  p,
int  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 []

Definition at line 74 of file dsdApi.c.

00074 { p->Mark = Mark;     }

int Dsd_TreeCollectDecomposableVars ( Dsd_Manager_t *  pDsdMan,
int *  pVars 
)

Function*************************************************************

Synopsis [Collects the decomposable vars on the PI side.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file dsdTree.c.

00471 {
00472         int nVars;
00473 
00474         // set the vars collected to 0
00475         nVars = 0;
00476         Dsd_TreeCollectDecomposableVars_rec( pDsdMan->dd, Dsd_Regular(pDsdMan->pRoots[0]), pVars, &nVars );
00477         // return the number of collected vars
00478         return nVars;
00479 }

Dsd_Node_t** Dsd_TreeCollectNodesDfs ( Dsd_Manager_t *  pDsdMan,
int *  pnNodes 
)

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 []

Definition at line 555 of file dsdTree.c.

00556 {
00557         Dsd_Node_t ** ppNodes;
00558         int nNodes, nNodesAlloc;
00559         int i;
00560 
00561     nNodesAlloc = Dsd_TreeCountNonTerminalNodes(pDsdMan);
00562         nNodes  = 0;
00563         ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
00564         for ( i = 0; i < pDsdMan->nRoots; i++ )
00565                 Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pDsdMan->pRoots[i]), ppNodes, &nNodes );
00566         Dsd_TreeUnmark( pDsdMan );
00567     assert( nNodesAlloc == nNodes );
00568         *pnNodes = nNodes;
00569         return ppNodes;
00570 }

Dsd_Node_t** Dsd_TreeCollectNodesDfsOne ( Dsd_Manager_t *  pDsdMan,
Dsd_Node_t *  pNode,
int *  pnNodes 
)

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 []

Definition at line 585 of file dsdTree.c.

00586 {
00587         Dsd_Node_t ** ppNodes;
00588         int nNodes, nNodesAlloc;
00589     nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode);
00590         nNodes  = 0;
00591         ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
00592     Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes );
00593         Dsd_TreeUnmark_rec(Dsd_Regular(pNode));
00594     assert( nNodesAlloc == nNodes );
00595         *pnNodes = nNodes;
00596         return ppNodes;
00597 }

int Dsd_TreeCountNonTerminalNodes ( Dsd_Manager_t *  pDsdMan  ) 

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 []

Definition at line 310 of file dsdTree.c.

00311 {
00312         int Counter, i;
00313     Counter = 0;
00314         for ( i = 0; i < pDsdMan->nRoots; i++ )
00315                 Counter += Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
00316         Dsd_TreeUnmark( pDsdMan );
00317     return Counter;
00318 }

int Dsd_TreeCountNonTerminalNodesOne ( Dsd_Node_t *  pRoot  ) 

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file dsdTree.c.

00332 {
00333         int Counter = 0;
00334 
00335         // go through the list of successors and call recursively 
00336         Counter = Dsd_TreeCountNonTerminalNodes_rec( Dsd_Regular(pRoot) );
00337 
00338         Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) );
00339         return Counter;
00340 }

int Dsd_TreeCountPrimeNodes ( Dsd_Manager_t *  pDsdMan  ) 

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 []

Definition at line 389 of file dsdTree.c.

00390 {
00391         int Counter, i;
00392     Counter = 0;
00393         for ( i = 0; i < pDsdMan->nRoots; i++ )
00394                 Counter += Dsd_TreeCountPrimeNodes_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
00395         Dsd_TreeUnmark( pDsdMan );
00396     return Counter;
00397 }

int Dsd_TreeCountPrimeNodesOne ( Dsd_Node_t *  pRoot  ) 

Function*************************************************************

Synopsis [Counts prime nodes for one root.]

Description []

SideEffects []

SeeAlso []

Definition at line 410 of file dsdTree.c.

00411 {
00412         int Counter = 0;
00413 
00414         // go through the list of successors and call recursively 
00415         Counter = Dsd_TreeCountPrimeNodes_rec( Dsd_Regular(pRoot) );
00416 
00417         Dsd_TreeUnmark_rec( Dsd_Regular(pRoot) );
00418         return Counter;
00419 }

int Dsd_TreeGetAigCost ( Dsd_Node_t *  pNode  ) 

Function*************************************************************

Synopsis [Counts AIG nodes needed to implement this node.]

Description [Assumes that the only primes of the DSD tree are MUXes.]

SideEffects []

SeeAlso []

Definition at line 291 of file dsdTree.c.

00292 {
00293     return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) );
00294 }

DdNode* Dsd_TreeGetPrimeFunction ( DdManager *  dd,
Dsd_Node_t *  pNode 
)

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 []

Definition at line 51 of file dsdLocal.c.

00052 {
00053     int * pForm2Var;   // the mapping of each formal input into its first var
00054     int * pVar2Form;   // the mapping of each var into its formal inputs
00055     int i, iVar, iLev, * pPermute;
00056     DdNode ** pbCube0, ** pbCube1;
00057     DdNode * bFunc, * bRes, * bTemp;
00058     st_table * pCache;
00059     
00060     pPermute  = ALLOC( int, dd->size );
00061     pVar2Form = ALLOC( int, dd->size );
00062     pForm2Var = ALLOC( int, dd->size );
00063 
00064     pbCube0 = ALLOC( DdNode *, dd->size );
00065     pbCube1 = ALLOC( DdNode *, dd->size );
00066 
00067     // remap the global function in such a way that
00068     // the support variables of each formal input are adjacent
00069     iLev = 0;
00070         for ( i = 0; i < pNode->nDecs; i++ )
00071     {
00072         pForm2Var[i] = dd->invperm[i];
00073         for ( bTemp = pNode->pDecs[i]->S; bTemp != b1; bTemp = cuddT(bTemp) )
00074         {
00075             iVar = dd->invperm[iLev];
00076             pPermute[bTemp->index] = iVar;
00077             pVar2Form[iVar] = i;
00078             iLev++;
00079         }
00080 
00081         // collect the cubes representing each assignment
00082         pbCube0[i] = Extra_bddGetOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) );
00083         Cudd_Ref( pbCube0[i] );
00084         pbCube1[i] = Extra_bddGetOneCube( dd, pNode->pDecs[i]->G );
00085         Cudd_Ref( pbCube1[i] );
00086     }
00087 
00088     // remap the function
00089     bFunc = Cudd_bddPermute( dd, pNode->G, pPermute ); Cudd_Ref( bFunc );
00090     // remap the cube
00091         for ( i = 0; i < pNode->nDecs; i++ )
00092     {
00093         pbCube0[i] = Cudd_bddPermute( dd, bTemp = pbCube0[i], pPermute ); Cudd_Ref( pbCube0[i] );
00094         Cudd_RecursiveDeref( dd, bTemp );
00095         pbCube1[i] = Cudd_bddPermute( dd, bTemp = pbCube1[i], pPermute ); Cudd_Ref( pbCube1[i] );
00096         Cudd_RecursiveDeref( dd, bTemp );
00097     }
00098 
00099     // remap the function
00100     pCache = st_init_table(st_ptrcmp,st_ptrhash);
00101     bRes = Extra_dsdRemap( dd, bFunc, pCache, pVar2Form, pForm2Var, pbCube0, pbCube1 );  Cudd_Ref( bRes );
00102     st_free_table( pCache );
00103 
00104     Cudd_RecursiveDeref( dd, bFunc );
00105         for ( i = 0; i < pNode->nDecs; i++ )
00106     {
00107         Cudd_RecursiveDeref( dd, pbCube0[i] );
00108         Cudd_RecursiveDeref( dd, pbCube1[i] );
00109     }
00110 /*
00112     // permute the function once again
00113     // in such a way that i-th var stood for i-th formal input
00114         for ( i = 0; i < dd->size; i++ )
00115         pPermute[i] = -1;
00116         for ( i = 0; i < pNode->nDecs; i++ )
00117         pPermute[dd->invperm[i]] = i;
00118     bRes = Cudd_bddPermute( dd, bTemp = bRes, pPermute ); Cudd_Ref( bRes );
00119     Cudd_RecursiveDeref( dd, bTemp );
00121 */
00122     FREE(pPermute);
00123     FREE(pVar2Form);
00124     FREE(pForm2Var);
00125     FREE(pbCube0);
00126     FREE(pbCube1);
00127 
00128     Cudd_Deref( bRes );
00129     return bRes;
00130 }

void Dsd_TreeNodeGetInfo ( Dsd_Manager_t *  pDsdMan,
int *  DepthMax,
int *  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 []

Definition at line 156 of file dsdTree.c.

00157 {
00158         int i;
00159         s_DepthMax    = 0;
00160         s_GateSizeMax = 0;
00161 
00162         for ( i = 0; i < pDsdMan->nRoots; i++ )
00163         Dsd_TreeGetInfo_rec( Dsd_Regular( pDsdMan->pRoots[i] ), 0 );
00164 
00165         if ( DepthMax ) 
00166                 *DepthMax     = s_DepthMax;
00167         if ( GateSizeMax ) 
00168                 *GateSizeMax  = s_GateSizeMax;
00169 }

void Dsd_TreeNodeGetInfoOne ( Dsd_Node_t *  pNode,
int *  DepthMax,
int *  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 []

Definition at line 183 of file dsdTree.c.

00184 {
00185         s_DepthMax    = 0;
00186         s_GateSizeMax = 0;
00187 
00188         Dsd_TreeGetInfo_rec( Dsd_Regular(pNode), 0 );
00189 
00190         if ( DepthMax ) 
00191                 *DepthMax     = s_DepthMax;
00192         if ( GateSizeMax ) 
00193                 *GateSizeMax  = s_GateSizeMax;
00194 }

void Dsd_TreePrint ( FILE *  pFile,
Dsd_Manager_t *  pDsdMan,
char *  pInputNames[],
char *  pOutputNames[],
int  fShortNames,
int  Output 
)

Function*************************************************************

Synopsis [Prints the decompostion tree into file.]

Description []

SideEffects []

SeeAlso []

Definition at line 641 of file dsdTree.c.

00642 {
00643         Dsd_Node_t * pNode;
00644         int SigCounter;
00645         int i;
00646         SigCounter = 1;
00647 
00648         if ( Output == -1 )
00649         {
00650                 for ( i = 0; i < pDsdMan->nRoots; i++ )
00651                 {
00652                         pNode = Dsd_Regular( pDsdMan->pRoots[i] );
00653                         Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[i]), pInputNames, pOutputNames[i], 0, &SigCounter, fShortNames );
00654                 }
00655         }
00656         else
00657         {
00658                 assert( Output >= 0 && Output < pDsdMan->nRoots );
00659                 pNode = Dsd_Regular( pDsdMan->pRoots[Output] );
00660                 Dsd_TreePrint_rec( pFile, pNode, (pNode != pDsdMan->pRoots[Output]), pInputNames, pOutputNames[Output], 0, &SigCounter, fShortNames );
00661         }
00662 }

Generated on Tue Jan 5 12:18:58 2010 for abc70930 by  doxygen 1.6.1