blob: 62ce7e99b28e64d7ffbb5e81f468d58e504483b5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
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 ///
////////////////////////////////////////////////////////////////////////
|
