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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
/**CFile****************************************************************
FileName [cec.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CEC_H__
#define __CEC_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// dynamic SAT parameters
typedef struct Cec_ParSat_t_ Cec_ParSat_t;
struct Cec_ParSat_t_
{
int nBTLimit; // conflict limit at a node
int nSatVarMax; // the max number of SAT variables
int nCallsRecycle; // calls to perform before recycling SAT solver
int fNonChrono; // use non-chronological backtracling (for circuit SAT only)
int fPolarFlip; // flops polarity of variables
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
int fLearnCls; // perform clause learning
int fVerbose; // verbose stats
};
// simulation parameters
typedef struct Cec_ParSim_t_ Cec_ParSim_t;
struct Cec_ParSim_t_
{
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int TimeLimit; // the runtime limit in seconds
int fDualOut; // miter with separate outputs
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
int fSeqSimulate; // performs sequential simulation
int fLatchCorr; // consider only latch outputs
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};
// semiformal parameters
typedef struct Cec_ParSmf_t_ Cec_ParSmf_t;
struct Cec_ParSmf_t_
{
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int nFrames; // the number of time frames
int nBTLimit; // conflict limit at a node
int TimeLimit; // the runtime limit in seconds
int fDualOut; // miter with separate outputs
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
int fVerbose; // verbose stats
};
// combinational SAT sweeping parameters
typedef struct Cec_ParFra_t_ Cec_ParFra_t;
struct Cec_ParFra_t_
{
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int nItersMax; // the maximum number of iterations of SAT sweeping
int nBTLimit; // conflict limit at a node
int TimeLimit; // the runtime limit in seconds
int nLevelMax; // restriction on the level nodes to be swept
int nDepthMax; // the depth in terms of steps of speculative reduction
int fRewriting; // enables AIG rewriting
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
int fDualOut; // miter with separate outputs
int fColorDiff; // miter with separate outputs
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};
// combinational equivalence checking parameters
typedef struct Cec_ParCec_t_ Cec_ParCec_t;
struct Cec_ParCec_t_
{
int nBTLimit; // conflict limit at a node
int TimeLimit; // the runtime limit in seconds
int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
int fRewriting; // enables AIG rewriting
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};
// sequential register correspodence parameters
typedef struct Cec_ParCor_t_ Cec_ParCor_t;
struct Cec_ParCor_t_
{
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int nFrames; // the number of time frames
int nPrefix; // the number of time frames in the prefix
int nBTLimit; // conflict limit at a node
int fLatchCorr; // consider only latch outputs
int fUseRings; // use rings
int fMakeChoices; // use equilvaences as choices
int fUseCSat; // use circuit-based solver
int fFirstStop; // stop on the first sat output
int fUseSmartCnf; // use smart CNF computation
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};
// sequential register correspodence parameters
typedef struct Cec_ParChc_t_ Cec_ParChc_t;
struct Cec_ParChc_t_
{
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int nBTLimit; // conflict limit at a node
int fUseRings; // use rings
int fUseCSat; // use circuit-based solver
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cecCec.c ==========================================================*/
extern int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars );
extern int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
/*=== cecChoice.c ==========================================================*/
extern Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
/*=== cecCorr.c ==========================================================*/
extern Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
/*=== cecCore.c ==========================================================*/
extern void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
extern void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p );
extern void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p );
extern void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p );
extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
extern void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p );
extern void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p );
extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
/*=== cecSeq.c ==========================================================*/
extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex );
extern int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
