ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dch.h
Go to the documentation of this file.
1
20
21#ifndef ABC__aig__dch__dch_h
22#define ABC__aig__dch__dch_h
23
24
28
32
33
34
36
37
41
42// choicing parameters
43typedef struct Dch_Pars_t_ Dch_Pars_t;
45{
46 int nWords; // the number of simulation words
47 int nBTLimit; // conflict limit at a node
48 int nSatVarMax; // the max number of SAT variables
49 int fSynthesis; // set to 1 to perform synthesis
50 int fPolarFlip; // uses polarity adjustment
51 int fSimulateTfo; // uses simulation of TFO classes
52 int fPower; // uses power-aware rewriting
53 int fUseGia; // uses GIA package
54 int fUseCSat; // uses circuit-based solver
55 int fUseNew; // uses new implementation
56 int fUseNew2; // uses new implementation
57 int fLightSynth; // uses lighter version of synthesis
58 int fSkipRedSupp; // skip choices with redundant support vars
59 int fVerbose; // verbose stats
60 abctime timeSynth; // synthesis runtime
61 int nNodesAhead; // the lookahead in terms of nodes
62 int nCallsRecycle; // calls to perform before recycling SAT solver
63};
64
68
72
73/*=== dchAig.c ==========================================================*/
74extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
75/*=== dchCore.c ==========================================================*/
76extern void Dch_ManSetDefaultParams( Dch_Pars_t * p );
77extern int Dch_ManReadVerbose( Dch_Pars_t * p );
78extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
79extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
80/*=== dchScript.c ==========================================================*/
81extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
82
83
85
86
87
88#endif
89
93
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
Definition dch.h:43
Aig_Man_t * Dar_ManChoiceNew(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition darScript.c:849
void Dch_ManSetDefaultParams(Dch_Pars_t *p)
DECLARATIONS ///.
Definition dchCore.c:45
Aig_Man_t * Dch_ComputeChoices(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition dchCore.c:89
void Dch_ComputeEquivalences(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition dchCore.c:136
Aig_Man_t * Dch_DeriveTotalAig(Vec_Ptr_t *vAigs)
MACRO DEFINITIONS ///.
Definition dchAig.c:65
int Dch_ManReadVerbose(Dch_Pars_t *p)
Definition dchCore.c:73
Cube * p
Definition exorList.c:222
int fSynthesis
Definition dch.h:49
int fUseGia
Definition dch.h:53
int fSkipRedSupp
Definition dch.h:58
int fUseNew
Definition dch.h:55
int fSimulateTfo
Definition dch.h:51
int fLightSynth
Definition dch.h:57
int nBTLimit
Definition dch.h:47
abctime timeSynth
Definition dch.h:60
int fUseCSat
Definition dch.h:54
int fPolarFlip
Definition dch.h:50
int fPower
Definition dch.h:52
int nCallsRecycle
Definition dch.h:62
int fVerbose
Definition dch.h:59
int nSatVarMax
Definition dch.h:48
int fUseNew2
Definition dch.h:56
int nWords
Definition dch.h:46
int nNodesAhead
Definition dch.h:61
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42