blob: a97bd958475ebe4e6260a9d54b5e1c268fbddc89 (
plain)
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
|
/**CFile****************************************************************
FileName [cec.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinatinoal 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 fPolarFlip; // flops polarity of variables
int fCheckMiter; // the circuit is the miter
int fFirstStop; // stop on the first sat output
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 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
};
////////////////////////////////////////////////////////////////////////
/// 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 );
/*=== 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 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 ///
////////////////////////////////////////////////////////////////////////
|
