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
|
/**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.00 2005/08/28 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CSAT_APIS_H__
#define __CSAT_APIS_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct CSAT_ManagerStruct_t CSAT_Manager_t;
typedef struct CSAT_ManagerStruct_t * CSAT_Manager;
// GateType defines the gate type that can be added to circuit by
// CSAT_AddGate();
#ifndef _CSAT_GATE_TYPE_
#define _CSAT_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_BPPO, // bit level PSEUDO PRIMARY OUTPUT
CSAT_BPO // boolean PO
};
#endif
//CSAT_StatusT defines the return value by CSAT_Solve();
#ifndef _CSAT_STATUS_
#define _CSAT_STATUS_
enum CSAT_StatusT
{
UNDETERMINED = 0,
UNSATISFIABLE,
SATISFIABLE,
TIME_OUT,
FRAME_OUT,
NO_TARGET,
ABORTED,
SEQ_SATISFIABLE
};
#endif
// CSAT_OptionT defines the solver option about learning
// which is used by CSAT_SetSolveOption();
#ifndef _CSAT_OPTION_
#define _CSAT_OPTION_
enum CSAT_OptionT
{
BASE_LINE = 0,
IMPLICT_LEARNING, //default
EXPLICT_LEARNING
};
#endif
#ifndef _CSAT_Target_Result
#define _CSAT_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 DEFITIONS ///
////////////////////////////////////////////////////////////////////////
// create a new manager
extern CSAT_Manager CSAT_InitManager(void);
// set solver options for learning
extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option);
// 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 CSAT_AddGate(CSAT_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 CSAT_Check_Integrity(CSAT_Manager mng);
// set time limit for solving a target.
// runtime: time limit (in second).
extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime);
extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num);
extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num);
extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num);
extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file);
// 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 CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
// initialize the solver internal data structure.
extern void CSAT_SolveInit(CSAT_Manager mng);
extern void CSAT_AnalyzeTargets(CSAT_Manager mng);
// solve the targets added by CSAT_AddTarget()
extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
// get the solve status of a target
// TargetID: the target id returned by CSAT_AddTarget().
extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
extern void CSAT_Dump_Bench_File(CSAT_Manager mng);
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
|
