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
|
/**CFile****************************************************************
FileName [sswInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __SSW_INT_H__
#define __SSW_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "saig.h"
#include "satSolver.h"
#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Ssw_Man_t_ Ssw_Man_t; // signal correspondence manager
typedef struct Ssw_Cla_t_ Ssw_Cla_t; // equivalence classe manager
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
struct Ssw_Man_t_
{
// parameters
Ssw_Pars_t * pPars; // parameters
int nFrames; // for quick lookup
// AIGs used in the package
Aig_Man_t * pAig; // user-given AIG
Aig_Man_t * pFrames; // final AIG
Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
int fRefined; // is set to 1 when refinement happens
int nRefUse;
int nRefSkip;
// SAT solving
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
int * pSatVars; // mapping of each node into its SAT var
int nSatVarsTotal; // the total number of SAT vars created
Vec_Ptr_t * vFanins; // fanins of the CNF node
Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
// SAT solving (latch corr only)
int nCallsSince; // the number of calls since last recycling
int nRecycles; // the number of time SAT solver was recycled
Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables
Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
// constraints
int nConstrTotal; // the number of total constraints
int nConstrReduced; // the number of reduced constraints
int nStrangers; // the number of strange situations
// SAT calls statistics
int nSatCalls; // the number of SAT calls
int nSatProof; // the number of proofs
int nSatFailsReal; // the number of timeouts
int nSatFailsTotal; // the number of timeouts
int nSatCallsUnsat; // the number of unsat SAT calls
int nSatCallsSat; // the number of sat SAT calls
// node/register/lit statistics
int nLitsBeg;
int nLitsEnd;
int nNodesBeg;
int nNodesEnd;
int nRegsBeg;
int nRegsEnd;
// runtime stats
int timeBmc; // bounded model checking
int timeReduce; // speculative reduction
int timeMarkCones; // marking the cones not to be refined
int timeSimSat; // simulation of the counter-examples
int timeSat; // solving SAT
int timeSatSat; // sat
int timeSatUnsat; // unsat
int timeSatUndec; // undecided
int timeOther; // other runtime
int timeTotal; // total runtime
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; }
static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; }
static inline int Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
{
return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
}
static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
{
assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) );
Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}
static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFraig[p->nFrames*pObj->Id + i]; }
static inline void Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; }
static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sswAig.c ===================================================*/
extern Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p );
/*=== sswClass.c =================================================*/
extern Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig );
extern void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
extern void Ssw_ClassesStop( Ssw_Cla_t * p );
extern Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p );
extern void Ssw_ClassesClearRefined( Ssw_Cla_t * p );
extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p );
extern int Ssw_ClassesClassNum( Ssw_Cla_t * p );
extern int Ssw_ClassesLitNum( Ssw_Cla_t * p );
extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
extern void Ssw_ClassesCheck( Ssw_Cla_t * p );
extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose );
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj );
extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
/*=== sswCnf.c ===================================================*/
extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
/*=== sswCore.c ===================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
/*=== sswLcorr.c ==========================================================*/
extern int Ssw_ManSweepLatch( Ssw_Man_t * p );
/*=== sswMan.c ===================================================*/
extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
extern void Ssw_ManCleanup( Ssw_Man_t * p );
extern void Ssw_ManStop( Ssw_Man_t * p );
extern void Ssw_ManStartSolver( Ssw_Man_t * p );
/*=== sswSat.c ===================================================*/
extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== sswSim.c ===================================================*/
extern Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
extern void Ssw_SmlStop( Ssw_Sml_t * p );
extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
extern unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj );
extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
/*=== sswSimSat.c ===================================================*/
extern int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
