1 /**CFile****************************************************************
2
3 FileName [cecMan.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Combinational equivalence checking.]
8
9 Synopsis [Manager procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: cecMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "cecInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Creates the manager.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Cec_ManSatCreate(Gia_Man_t * pAig,Cec_ParSat_t * pPars)45 Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
46 {
47 Cec_ManSat_t * p;
48 // create interpolation manager
49 p = ABC_ALLOC( Cec_ManSat_t, 1 );
50 memset( p, 0, sizeof(Cec_ManSat_t) );
51 p->pPars = pPars;
52 p->pAig = pAig;
53 // SAT solving
54 p->nSatVars = 1;
55 p->pSatVars = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
56 p->vUsedNodes = Vec_PtrAlloc( 1000 );
57 p->vFanins = Vec_PtrAlloc( 100 );
58 p->vCex = Vec_IntAlloc( 100 );
59 p->vVisits = Vec_IntAlloc( 100 );
60 return p;
61 }
62
63 /**Function*************************************************************
64
65 Synopsis [Prints statistics of the manager.]
66
67 Description []
68
69 SideEffects []
70
71 SeeAlso []
72
73 ***********************************************************************/
Cec_ManSatPrintStats(Cec_ManSat_t * p)74 void Cec_ManSatPrintStats( Cec_ManSat_t * p )
75 {
76 Abc_Print( 1, "CO = %8d ", Gia_ManCoNum(p->pAig) );
77 Abc_Print( 1, "AND = %8d ", Gia_ManAndNum(p->pAig) );
78 Abc_Print( 1, "Conf = %5d ", p->pPars->nBTLimit );
79 Abc_Print( 1, "MinVar = %5d ", p->pPars->nSatVarMax );
80 Abc_Print( 1, "MinCalls = %5d\n", p->pPars->nCallsRecycle );
81 Abc_Print( 1, "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
82 p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
83 Abc_PrintTimeP( 1, "Time", p->timeSatUnsat, p->timeTotal );
84 Abc_Print( 1, "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
85 p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
86 Abc_PrintTimeP( 1, "Time", p->timeSatSat, p->timeTotal );
87 Abc_Print( 1, "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
88 p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
89 Abc_PrintTimeP( 1, "Time", p->timeSatUndec, p->timeTotal );
90 Abc_PrintTime( 1, "Total time", p->timeTotal );
91 }
92
93 /**Function*************************************************************
94
95 Synopsis [Frees the manager.]
96
97 Description []
98
99 SideEffects []
100
101 SeeAlso []
102
103 ***********************************************************************/
Cec_ManSatStop(Cec_ManSat_t * p)104 void Cec_ManSatStop( Cec_ManSat_t * p )
105 {
106 if ( p->pSat )
107 sat_solver_delete( p->pSat );
108 Vec_IntFree( p->vCex );
109 Vec_IntFree( p->vVisits );
110 Vec_PtrFree( p->vUsedNodes );
111 Vec_PtrFree( p->vFanins );
112 ABC_FREE( p->pSatVars );
113 ABC_FREE( p );
114 }
115
116
117
118 /**Function*************************************************************
119
120 Synopsis [Creates AIG.]
121
122 Description []
123
124 SideEffects []
125
126 SeeAlso []
127
128 ***********************************************************************/
Cec_ManPatStart()129 Cec_ManPat_t * Cec_ManPatStart()
130 {
131 Cec_ManPat_t * p;
132 p = ABC_CALLOC( Cec_ManPat_t, 1 );
133 p->vStorage = Vec_StrAlloc( 1<<20 );
134 p->vPattern1 = Vec_IntAlloc( 1000 );
135 p->vPattern2 = Vec_IntAlloc( 1000 );
136 return p;
137 }
138
139 /**Function*************************************************************
140
141 Synopsis [Creates AIG.]
142
143 Description []
144
145 SideEffects []
146
147 SeeAlso []
148
149 ***********************************************************************/
Cec_ManPatPrintStats(Cec_ManPat_t * p)150 void Cec_ManPatPrintStats( Cec_ManPat_t * p )
151 {
152 Abc_Print( 1, "Latest: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f MB\n",
153 p->nPats, p->nPatLits, p->nPatLitsMin, 1.0 * p->nPatLitsMin/p->nPats,
154 1.0*(Vec_StrSize(p->vStorage)-p->iStart)/(1<<20) );
155 Abc_Print( 1, "Total: P = %8d. L = %10d. Lm = %10d. Ave = %6.1f. MEM =%6.2f MB\n",
156 p->nPatsAll, p->nPatLitsAll, p->nPatLitsMinAll, 1.0 * p->nPatLitsMinAll/p->nPatsAll,
157 1.0*Vec_StrSize(p->vStorage)/(1<<20) );
158 Abc_PrintTimeP( 1, "Finding ", p->timeFind, p->timeTotal );
159 Abc_PrintTimeP( 1, "Shrinking", p->timeShrink, p->timeTotal );
160 Abc_PrintTimeP( 1, "Verifying", p->timeVerify, p->timeTotal );
161 Abc_PrintTimeP( 1, "Sorting ", p->timeSort, p->timeTotal );
162 Abc_PrintTimeP( 1, "Packing ", p->timePack, p->timeTotal );
163 Abc_PrintTime( 1, "TOTAL ", p->timeTotal );
164 }
165
166 /**Function*************************************************************
167
168 Synopsis [Deletes AIG.]
169
170 Description []
171
172 SideEffects []
173
174 SeeAlso []
175
176 ***********************************************************************/
Cec_ManPatStop(Cec_ManPat_t * p)177 void Cec_ManPatStop( Cec_ManPat_t * p )
178 {
179 Vec_StrFree( p->vStorage );
180 Vec_IntFree( p->vPattern1 );
181 Vec_IntFree( p->vPattern2 );
182 ABC_FREE( p );
183 }
184
185
186
187 /**Function*************************************************************
188
189 Synopsis [Creates AIG.]
190
191 Description []
192
193 SideEffects []
194
195 SeeAlso []
196
197 ***********************************************************************/
Cec_ManSimStart(Gia_Man_t * pAig,Cec_ParSim_t * pPars)198 Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
199 {
200 Cec_ManSim_t * p;
201 p = ABC_ALLOC( Cec_ManSim_t, 1 );
202 memset( p, 0, sizeof(Cec_ManSim_t) );
203 p->pAig = pAig;
204 p->pPars = pPars;
205 p->nWords = pPars->nWords;
206 p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
207 p->vClassOld = Vec_IntAlloc( 1000 );
208 p->vClassNew = Vec_IntAlloc( 1000 );
209 p->vClassTemp = Vec_IntAlloc( 1000 );
210 p->vRefinedC = Vec_IntAlloc( 10000 );
211 p->vCiSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(p->pAig), pPars->nWords );
212 if ( pPars->fCheckMiter || Gia_ManRegNum(p->pAig) )
213 {
214 p->vCoSimInfo = Vec_PtrAllocSimInfo( Gia_ManCoNum(p->pAig), pPars->nWords );
215 Vec_PtrCleanSimInfo( p->vCoSimInfo, 0, pPars->nWords );
216 }
217 p->iOut = -1;
218 return p;
219 }
220
221 /**Function*************************************************************
222
223 Synopsis [Deletes AIG.]
224
225 Description []
226
227 SideEffects []
228
229 SeeAlso []
230
231 ***********************************************************************/
Cec_ManSimStop(Cec_ManSim_t * p)232 void Cec_ManSimStop( Cec_ManSim_t * p )
233 {
234 Vec_IntFree( p->vClassOld );
235 Vec_IntFree( p->vClassNew );
236 Vec_IntFree( p->vClassTemp );
237 Vec_IntFree( p->vRefinedC );
238 if ( p->vCiSimInfo )
239 Vec_PtrFree( p->vCiSimInfo );
240 if ( p->vCoSimInfo )
241 Vec_PtrFree( p->vCoSimInfo );
242 ABC_FREE( p->pScores );
243 ABC_FREE( p->pCexComb );
244 ABC_FREE( p->pCexes );
245 ABC_FREE( p->pMems );
246 ABC_FREE( p->pSimInfo );
247 ABC_FREE( p );
248 }
249
250
251 /**Function*************************************************************
252
253 Synopsis [Creates AIG.]
254
255 Description []
256
257 SideEffects []
258
259 SeeAlso []
260
261 ***********************************************************************/
Cec_ManFraStart(Gia_Man_t * pAig,Cec_ParFra_t * pPars)262 Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
263 {
264 Cec_ManFra_t * p;
265 p = ABC_ALLOC( Cec_ManFra_t, 1 );
266 memset( p, 0, sizeof(Cec_ManFra_t) );
267 p->pAig = pAig;
268 p->pPars = pPars;
269 p->vXorNodes = Vec_IntAlloc( 1000 );
270 return p;
271 }
272
273 /**Function*************************************************************
274
275 Synopsis [Deletes AIG.]
276
277 Description []
278
279 SideEffects []
280
281 SeeAlso []
282
283 ***********************************************************************/
Cec_ManFraStop(Cec_ManFra_t * p)284 void Cec_ManFraStop( Cec_ManFra_t * p )
285 {
286 Vec_IntFree( p->vXorNodes );
287 ABC_FREE( p );
288 }
289
290
291 ////////////////////////////////////////////////////////////////////////
292 /// END OF FILE ///
293 ////////////////////////////////////////////////////////////////////////
294
295
296 ABC_NAMESPACE_IMPL_END
297
298