ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dsdInt.h
Go to the documentation of this file.
1
18
19#ifndef ABC__bdd__dsd__dsdInt_h
20#define ABC__bdd__dsd__dsdInt_h
21
22
23#include "bdd/extrab/extraBdd.h"
24#include "dsd.h"
25
27
28
32
33typedef unsigned char byte;
34
38
39// DSD manager
41{
42 DdManager * dd; // the BDD manager
43 st__table * Table; // the mapping of BDDs into their DEs
44 int nInputs; // the number of primary inputs
45 int nRoots; // the number of primary outputs
46 int nRootsAlloc;// the number of primary outputs
47 Dsd_Node_t ** pInputs; // the primary input nodes
48 Dsd_Node_t ** pRoots; // the primary output nodes
49 Dsd_Node_t * pConst1; // the constant node
50 int fVerbose; // the verbosity level
51};
52
53// DSD node
55{
56 Dsd_Type_t Type; // decomposition type
57 DdNode * G; // function of the node
58 DdNode * S; // support of this function
59 Dsd_Node_t ** pDecs; // pointer to structures for formal inputs
60 word Mark; // the mark used by CASE 4 of disjoint decomposition
61 short nDecs; // the number of formal inputs
62 short nVisits; // the counter of visits
63};
64
68
69#define MAXINPUTS 1000
70
74
78
79/*=== dsdCheck.c =======================================================*/
80extern void Dsd_CheckCacheAllocate( int nEntries );
81extern void Dsd_CheckCacheDeallocate();
82extern void Dsd_CheckCacheClear();
83extern int Dsd_CheckRootFunctionIdentity( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 );
84/*=== dsdTree.c =======================================================*/
85extern Dsd_Node_t * Dsd_TreeNodeCreate( int Type, int nDecs, int BlockNum );
86extern void Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode );
87extern void Dsd_TreeUnmark( Dsd_Manager_t * dMan );
88extern DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap );
89
90
91
93
94#endif
95
99
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
void Dsd_CheckCacheDeallocate()
Definition dsdCheck.c:97
int Dsd_CheckRootFunctionIdentity(DdManager *dd, DdNode *bF1, DdNode *bF2, DdNode *bC1, DdNode *bC2)
Definition dsdCheck.c:133
Dsd_Node_t * Dsd_TreeNodeCreate(int Type, int nDecs, int BlockNum)
FUNCTION DEFINITIONS ///.
Definition dsdTree.c:61
void Dsd_TreeNodeDelete(DdManager *dd, Dsd_Node_t *pNode)
Definition dsdTree.c:87
void Dsd_CheckCacheAllocate(int nEntries)
PARAMETERS ///.
Definition dsdCheck.c:63
void Dsd_CheckCacheClear()
Definition dsdCheck.c:114
void Dsd_TreeUnmark(Dsd_Manager_t *dMan)
Definition dsdTree.c:107
DdNode * Dsd_TreeGetPrimeFunctionOld(DdManager *dd, Dsd_Node_t *pNode, int fRemap)
Definition dsdTree.c:1309
enum Dsd_Type_t_ Dsd_Type_t
Definition dsd.h:61
struct Dsd_Manager_t_ Dsd_Manager_t
TYPEDEF DEFINITIONS ///.
Definition dsd.h:59
struct Dsd_Node_t_ Dsd_Node_t
Definition dsd.h:60
unsigned char byte
Definition exor.h:121
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
STRUCTURE DEFINITIONS ///.
Definition dsdInt.h:41
DdManager * dd
Definition dsdInt.h:42
Dsd_Node_t ** pInputs
Definition dsdInt.h:47
int nRootsAlloc
Definition dsdInt.h:46
Dsd_Node_t * pConst1
Definition dsdInt.h:49
st__table * Table
Definition dsdInt.h:43
Dsd_Node_t ** pRoots
Definition dsdInt.h:48
DdNode * G
Definition dsdInt.h:57
Dsd_Type_t Type
Definition dsdInt.h:56
short nVisits
Definition dsdInt.h:62
DdNode * S
Definition dsdInt.h:58
Dsd_Node_t ** pDecs
Definition dsdInt.h:59
short nDecs
Definition dsdInt.h:61
word Mark
Definition dsdInt.h:60
Definition st.h:52