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
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
|
/**CFile****************************************************************
FileName [csat_apis.h]
PackageName [Interface to CSAT.]
Synopsis [APIs, enums, and data structures expected from the use of CSAT.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - August 28, 2005]
Revision [$Id: csat_apis.h,v 1.5 2005/12/30 10:54:40 rmukherj Exp $]
***********************************************************************/
#ifndef ABC__sat__csat__csat_apis_h
#define ABC__sat__csat__csat_apis_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct ABC_ManagerStruct_t ABC_Manager_t;
typedef struct ABC_ManagerStruct_t * ABC_Manager;
// GateType defines the gate type that can be added to circuit by
// ABC_AddGate();
#ifndef _ABC_GATE_TYPE_
#define _ABC_GATE_TYPE_
enum GateType
{
CSAT_CONST = 0, // constant gate
CSAT_BPI, // boolean PI
CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT
CSAT_BAND, // bit level AND
CSAT_BNAND, // bit level NAND
CSAT_BOR, // bit level OR
CSAT_BNOR, // bit level NOR
CSAT_BXOR, // bit level XOR
CSAT_BXNOR, // bit level XNOR
CSAT_BINV, // bit level INVERTER
CSAT_BBUF, // bit level BUFFER
CSAT_BMUX, // bit level MUX --not supported
CSAT_BDFF, // bit level D-type FF
CSAT_BSDFF, // bit level scan FF --not supported
CSAT_BTRIH, // bit level TRISTATE gate with active high control --not supported
CSAT_BTRIL, // bit level TRISTATE gate with active low control --not supported
CSAT_BBUS, // bit level BUS --not supported
CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT
CSAT_BPO, // boolean PO
CSAT_BCNF, // boolean constraint
CSAT_BDC, // boolean don't care gate (2 input)
};
#endif
//CSAT_StatusT defines the return value by ABC_Solve();
#ifndef _ABC_STATUS_
#define _ABC_STATUS_
enum CSAT_StatusT
{
UNDETERMINED = 0,
UNSATISFIABLE,
SATISFIABLE,
TIME_OUT,
FRAME_OUT,
NO_TARGET,
ABORTED,
SEQ_SATISFIABLE
};
#endif
// to identify who called the CSAT solver
#ifndef _ABC_CALLER_
#define _ABC_CALLER_
enum CSAT_CallerT
{
BLS = 0,
SATORI,
NONE
};
#endif
// CSAT_OptionT defines the solver option about learning
// which is used by ABC_SetSolveOption();
#ifndef _ABC_OPTION_
#define _ABC_OPTION_
enum CSAT_OptionT
{
BASE_LINE = 0,
IMPLICT_LEARNING, //default
EXPLICT_LEARNING
};
#endif
#ifndef _ABC_Target_Result
#define _ABC_Target_Result
typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
struct _CSAT_Target_ResultT
{
enum CSAT_StatusT status; // solve status of the target
int num_dec; // num of decisions to solve the target
int num_imp; // num of implications to solve the target
int num_cftg; // num of conflict gates learned
int num_cfts; // num of conflict signals in conflict gates
double time; // time(in second) used to solve the target
int no_sig; // if "status" is SATISFIABLE, "no_sig" is the number of
// primary inputs, if the "status" is TIME_OUT, "no_sig" is the
// number of constant signals found.
char** names; // if the "status" is SATISFIABLE, "names" is the name array of
// primary inputs, "values" is the value array of primary
// inputs that satisfy the target.
// if the "status" is TIME_OUT, "names" is the name array of
// constant signals found (signals at the root of decision
// tree), "values" is the value array of constant signals found.
int* values;
};
#endif
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// create a new manager
extern ABC_Manager ABC_InitManager(void);
// release a manager
extern void ABC_ReleaseManager(ABC_Manager mng);
// set solver options for learning
extern void ABC_SetSolveOption(ABC_Manager mng, enum CSAT_OptionT option);
// enable checking by brute-force SAT solver (MiniSat-1.14)
extern void ABC_UseOnlyCoreSatSolver(ABC_Manager mng);
// add a gate to the circuit
// the meaning of the parameters are:
// type: the type of the gate to be added
// name: the name of the gate to be added, name should be unique in a circuit.
// nofi: number of fanins of the gate to be added;
// fanins: the name array of fanins of the gate to be added
extern int ABC_AddGate(ABC_Manager mng,
enum GateType type,
char* name,
int nofi,
char** fanins,
int dc_attr);
// check if there are gates that are not used by any primary ouput.
// if no such gates exist, return 1 else return 0;
extern int ABC_Check_Integrity(ABC_Manager mng);
// THIS PROCEDURE SHOULD BE CALLED AFTER THE NETWORK IS CONSTRUCTED!!!
extern void ABC_Network_Finalize( ABC_Manager mng );
// set time limit for solving a target.
// runtime: time limit (in second).
extern void ABC_SetTimeLimit(ABC_Manager mng, int runtime);
extern void ABC_SetLearnLimit(ABC_Manager mng, int num);
extern void ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num);
extern void ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num);
extern void ABC_EnableDump(ABC_Manager mng, char* dump_file);
extern void ABC_SetTotalBacktrackLimit( ABC_Manager mng, ABC_UINT64_T num );
extern void ABC_SetTotalInspectLimit( ABC_Manager mng, ABC_UINT64_T num );
extern ABC_UINT64_T ABC_GetTotalBacktracksMade( ABC_Manager mng );
extern ABC_UINT64_T ABC_GetTotalInspectsMade( ABC_Manager mng );
// the meaning of the parameters are:
// nog: number of gates that are in the targets
// names: name array of gates
// values: value array of the corresponding gates given in "names" to be
// solved. the relation of them is AND.
extern int ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values);
// initialize the solver internal data structure.
extern void ABC_SolveInit(ABC_Manager mng);
extern void ABC_AnalyzeTargets(ABC_Manager mng);
// solve the targets added by ABC_AddTarget()
extern enum CSAT_StatusT ABC_Solve(ABC_Manager mng);
// get the solve status of a target
// TargetID: the target id returned by ABC_AddTarget().
extern CSAT_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID);
extern void ABC_Dump_Bench_File(ABC_Manager mng);
// ADDED PROCEDURES:
extern void ABC_TargetResFree( CSAT_Target_ResultT * p );
extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller);
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
