1 /**CFile****************************************************************
2
3 FileName [cecCore.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Combinational equivalence checking.]
8
9 Synopsis [Core 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: cecCore.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 [This procedure sets default parameters.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Cec_ManSatSetDefaultParams(Cec_ParSat_t * p)45 void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
46 {
47 memset( p, 0, sizeof(Cec_ParSat_t) );
48 p->nBTLimit = 100; // conflict limit at a node
49 p->nSatVarMax = 2000; // the max number of SAT variables
50 p->nCallsRecycle = 200; // calls to perform before recycling SAT solver
51 p->fNonChrono = 1; // use non-chronological backtracling (for circuit SAT only)
52 p->fPolarFlip = 1; // flops polarity of variables
53 p->fCheckMiter = 0; // the circuit is the miter
54 // p->fFirstStop = 0; // stop on the first sat output
55 p->fLearnCls = 0; // perform clause learning
56 p->fVerbose = 0; // verbose stats
57 }
58
59 /**Function************ *************************************************
60
61 Synopsis [This procedure sets default parameters.]
62
63 Description []
64
65 SideEffects []
66
67 SeeAlso []
68
69 ***********************************************************************/
Cec_ManSimSetDefaultParams(Cec_ParSim_t * p)70 void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
71 {
72 memset( p, 0, sizeof(Cec_ParSim_t) );
73 p->nWords = 31; // the number of simulation words
74 p->nFrames = 100; // the number of simulation frames
75 p->nRounds = 20; // the max number of simulation rounds
76 p->nNonRefines = 3; // the max number of rounds without refinement
77 p->TimeLimit = 0; // the runtime limit in seconds
78 p->fCheckMiter = 0; // the circuit is the miter
79 // p->fFirstStop = 0; // stop on the first sat output
80 p->fDualOut = 0; // miter with separate outputs
81 p->fConstCorr = 0; // consider only constants
82 p->fSeqSimulate = 0; // performs sequential simulation
83 p->fVeryVerbose = 0; // verbose stats
84 p->fVerbose = 0; // verbose stats
85 }
86
87 /**Function************ *************************************************
88
89 Synopsis [This procedure sets default parameters.]
90
91 Description []
92
93 SideEffects []
94
95 SeeAlso []
96
97 ***********************************************************************/
Cec_ManSmfSetDefaultParams(Cec_ParSmf_t * p)98 void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
99 {
100 memset( p, 0, sizeof(Cec_ParSmf_t) );
101 p->nWords = 31; // the number of simulation words
102 p->nRounds = 200; // the number of simulation rounds
103 p->nFrames = 200; // the max number of time frames
104 p->nNonRefines = 3; // the max number of rounds without refinement
105 p->nMinOutputs = 0; // the min outputs to accumulate
106 p->nBTLimit = 100; // conflict limit at a node
107 p->TimeLimit = 0; // the runtime limit in seconds
108 p->fDualOut = 0; // miter with separate outputs
109 p->fCheckMiter = 0; // the circuit is the miter
110 // p->fFirstStop = 0; // stop on the first sat output
111 p->fVerbose = 0; // verbose stats
112 }
113
114 /**Function************ *************************************************
115
116 Synopsis [This procedure sets default parameters.]
117
118 Description []
119
120 SideEffects []
121
122 SeeAlso []
123
124 ***********************************************************************/
Cec_ManFraSetDefaultParams(Cec_ParFra_t * p)125 void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
126 {
127 memset( p, 0, sizeof(Cec_ParFra_t) );
128 p->nWords = 15; // the number of simulation words
129 p->nRounds = 15; // the number of simulation rounds
130 p->TimeLimit = 0; // the runtime limit in seconds
131 p->nItersMax = 10; // the maximum number of iterations of SAT sweeping
132 p->nBTLimit = 100; // conflict limit at a node
133 p->nLevelMax = 0; // restriction on the level of nodes to be swept
134 p->nDepthMax = 1; // the depth in terms of steps of speculative reduction
135 p->fRewriting = 0; // enables AIG rewriting
136 p->fCheckMiter = 0; // the circuit is the miter
137 // p->fFirstStop = 0; // stop on the first sat output
138 p->fDualOut = 0; // miter with separate outputs
139 p->fColorDiff = 0; // miter with separate outputs
140 p->fSatSweeping = 0; // enable SAT sweeping
141 p->fUseCones = 0; // use cones
142 p->fVeryVerbose = 0; // verbose stats
143 p->fVerbose = 0; // verbose stats
144 p->iOutFail = -1; // the failed output
145 }
146
147 /**Function*************************************************************
148
149 Synopsis [This procedure sets default parameters.]
150
151 Description []
152
153 SideEffects []
154
155 SeeAlso []
156
157 ***********************************************************************/
Cec_ManCecSetDefaultParams(Cec_ParCec_t * p)158 void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
159 {
160 memset( p, 0, sizeof(Cec_ParCec_t) );
161 p->nBTLimit = 1000; // conflict limit at a node
162 p->TimeLimit = 0; // the runtime limit in seconds
163 // p->fFirstStop = 0; // stop on the first sat output
164 p->fUseSmartCnf = 0; // use smart CNF computation
165 p->fRewriting = 0; // enables AIG rewriting
166 p->fVeryVerbose = 0; // verbose stats
167 p->fVerbose = 0; // verbose stats
168 p->iOutFail = -1; // the number of failed output
169 }
170
171 /**Function*************************************************************
172
173 Synopsis [This procedure sets default parameters.]
174
175 Description []
176
177 SideEffects []
178
179 SeeAlso []
180
181 ***********************************************************************/
Cec_ManCorSetDefaultParams(Cec_ParCor_t * p)182 void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
183 {
184 memset( p, 0, sizeof(Cec_ParCor_t) );
185 p->nWords = 15; // the number of simulation words
186 p->nRounds = 15; // the number of simulation rounds
187 p->nFrames = 1; // the number of time frames
188 p->nBTLimit = 100; // conflict limit at a node
189 p->nLevelMax = -1; // (scorr only) the max number of levels
190 p->nStepsMax = -1; // (scorr only) the max number of induction steps
191 p->fLatchCorr = 0; // consider only latch outputs
192 p->fConstCorr = 0; // consider only constants
193 p->fUseRings = 1; // combine classes into rings
194 p->fUseCSat = 1; // use circuit-based solver
195 // p->fFirstStop = 0; // stop on the first sat output
196 p->fUseSmartCnf = 0; // use smart CNF computation
197 p->fVeryVerbose = 0; // verbose stats
198 p->fVerbose = 0; // verbose stats
199 }
200
201 /**Function*************************************************************
202
203 Synopsis [This procedure sets default parameters.]
204
205 Description []
206
207 SideEffects []
208
209 SeeAlso []
210
211 ***********************************************************************/
Cec_ManChcSetDefaultParams(Cec_ParChc_t * p)212 void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
213 {
214 memset( p, 0, sizeof(Cec_ParChc_t) );
215 p->nWords = 15; // the number of simulation words
216 p->nRounds = 15; // the number of simulation rounds
217 p->nBTLimit = 1000; // conflict limit at a node
218 p->fUseRings = 1; // use rings
219 p->fUseCSat = 0; // use circuit-based solver
220 p->fVeryVerbose = 0; // verbose stats
221 p->fVerbose = 0; // verbose stats
222 }
223
224 /**Function*************************************************************
225
226 Synopsis [Core procedure for SAT sweeping.]
227
228 Description []
229
230 SideEffects []
231
232 SeeAlso []
233
234 ***********************************************************************/
Cec_ManSatSolving(Gia_Man_t * pAig,Cec_ParSat_t * pPars)235 Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
236 {
237 Gia_Man_t * pNew;
238 Cec_ManPat_t * pPat;
239 pPat = Cec_ManPatStart();
240 Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL );
241 // pNew = Gia_ManDupDfsSkip( pAig );
242 pNew = Gia_ManDup( pAig );
243 Cec_ManPatStop( pPat );
244 pNew->vSeqModelVec = pAig->vSeqModelVec;
245 pAig->vSeqModelVec = NULL;
246 return pNew;
247 }
248
249 /**Function*************************************************************
250
251 Synopsis [Core procedure for simulation.]
252
253 Description [Returns 1 if refinement has happened.]
254
255 SideEffects []
256
257 SeeAlso []
258
259 ***********************************************************************/
Cec_ManSimulationOne(Gia_Man_t * pAig,Cec_ParSim_t * pPars)260 int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
261 {
262 Cec_ManSim_t * pSim;
263 int RetValue = 0;
264 abctime clkTotal = Abc_Clock();
265 pSim = Cec_ManSimStart( pAig, pPars );
266 if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim, -1 ))) ||
267 (RetValue == 0 && (RetValue = Cec_ManSimClassesRefine( pSim ))) )
268 Abc_Print( 1, "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n",
269 pSim->nOuts, pPars->nWords, pPars->nFrames );
270 if ( pPars->fVerbose )
271 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
272 Cec_ManSimStop( pSim );
273 return RetValue;
274 }
275
276 /**Function*************************************************************
277
278 Synopsis [Core procedure for simulation.]
279
280 Description []
281
282 SideEffects []
283
284 SeeAlso []
285
286 ***********************************************************************/
Cec_ManSimulation(Gia_Man_t * pAig,Cec_ParSim_t * pPars)287 void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
288 {
289 int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0;
290 Gia_ManRandom( 1 );
291 if ( pPars->fSeqSimulate )
292 Abc_Print( 1, "Performing rounds of random simulation of %d frames with %d words.\n",
293 pPars->nRounds, pPars->nFrames, pPars->nWords );
294 nLitsOld = Gia_ManEquivCountLits( pAig );
295 for ( r = 0; r < pPars->nRounds; r++ )
296 {
297 if ( Cec_ManSimulationOne( pAig, pPars ) )
298 {
299 fStop = 1;
300 break;
301 }
302 // decide when to stop
303 nLitsNew = Gia_ManEquivCountLits( pAig );
304 if ( nLitsOld == 0 || nLitsOld > nLitsNew )
305 {
306 nLitsOld = nLitsNew;
307 nCountNoRef = 0;
308 }
309 else if ( ++nCountNoRef == pPars->nNonRefines )
310 {
311 r++;
312 break;
313 }
314 assert( nLitsOld == nLitsNew );
315 }
316 // if ( pPars->fVerbose )
317 if ( r == pPars->nRounds || fStop )
318 Abc_Print( 1, "Random simulation is stopped after %d rounds.\n", r );
319 else
320 Abc_Print( 1, "Random simulation saturated after %d rounds.\n", r );
321 if ( pPars->fCheckMiter )
322 {
323 int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
324 if ( nNonConsts )
325 Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
326 }
327 }
328
329 /**Function*************************************************************
330
331 Synopsis [Core procedure for SAT sweeping.]
332
333 Description []
334
335 SideEffects []
336
337 SeeAlso []
338
339 ***********************************************************************/
Cec_ManSatSweeping(Gia_Man_t * pAig,Cec_ParFra_t * pPars,int fSilent)340 Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent )
341 {
342 int fOutputResult = 0;
343 Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
344 Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
345 Gia_Man_t * pIni, * pSrm, * pTemp;
346 Cec_ManFra_t * p;
347 Cec_ManSim_t * pSim;
348 Cec_ManPat_t * pPat;
349 int i, fTimeOut = 0, nMatches = 0;
350 abctime clk, clk2, clkTotal = Abc_Clock();
351
352 // duplicate AIG and transfer equivalence classes
353 Gia_ManRandom( 1 );
354 pIni = Gia_ManDup(pAig);
355 pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
356 pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
357 if ( pPars->fUseOrigIds )
358 {
359 Gia_ManOrigIdsInit( pIni );
360 Vec_IntFreeP( &pAig->vIdsEquiv );
361 pAig->vIdsEquiv = Vec_IntAlloc( 1000 );
362 }
363
364 // prepare the managers
365 // SAT sweeping
366 p = Cec_ManFraStart( pIni, pPars );
367 if ( pPars->fDualOut )
368 pPars->fColorDiff = 1;
369 // simulation
370 Cec_ManSimSetDefaultParams( pParsSim );
371 pParsSim->nWords = pPars->nWords;
372 pParsSim->nFrames = pPars->nRounds;
373 pParsSim->fCheckMiter = pPars->fCheckMiter;
374 pParsSim->fDualOut = pPars->fDualOut;
375 pParsSim->fVerbose = pPars->fVerbose;
376 pSim = Cec_ManSimStart( p->pAig, pParsSim );
377 // SAT solving
378 Cec_ManSatSetDefaultParams( pParsSat );
379 pParsSat->nBTLimit = pPars->nBTLimit;
380 pParsSat->fVerbose = pPars->fVeryVerbose;
381 // simulation patterns
382 pPat = Cec_ManPatStart();
383 pPat->fVerbose = pPars->fVeryVerbose;
384
385 // start equivalence classes
386 clk = Abc_Clock();
387 if ( p->pAig->pReprs == NULL )
388 {
389 if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
390 {
391 Gia_ManStop( p->pAig );
392 p->pAig = NULL;
393 goto finalize;
394 }
395 }
396 p->timeSim += Abc_Clock() - clk;
397 // perform solving
398 for ( i = 1; i <= pPars->nItersMax; i++ )
399 {
400 clk2 = Abc_Clock();
401 nMatches = 0;
402 if ( pPars->fDualOut )
403 {
404 nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose );
405 // p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig );
406 // Gia_ManEquivTransform( p->pAig, 1 );
407 }
408 pSrm = Cec_ManFraSpecReduction( p );
409
410 // Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0, 0 );
411
412 if ( pPars->fVeryVerbose )
413 Gia_ManPrintStats( pSrm, NULL );
414 if ( Gia_ManCoNum(pSrm) == 0 )
415 {
416 Gia_ManStop( pSrm );
417 if ( p->pPars->fVerbose )
418 Abc_Print( 1, "Considered all available candidate equivalences.\n" );
419 if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 )
420 {
421 if ( pPars->fColorDiff )
422 {
423 if ( p->pPars->fVerbose )
424 Abc_Print( 1, "Switching into reduced mode.\n" );
425 pPars->fColorDiff = 0;
426 }
427 else
428 {
429 if ( p->pPars->fVerbose )
430 Abc_Print( 1, "Switching into normal mode.\n" );
431 pPars->fDualOut = 0;
432 }
433 continue;
434 }
435 break;
436 }
437 clk = Abc_Clock();
438 if ( pPars->fRunCSat )
439 Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
440 else
441 Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv );
442 p->timeSat += Abc_Clock() - clk;
443 if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
444 {
445 Gia_ManStop( pSrm );
446 Gia_ManStop( p->pAig );
447 p->pAig = NULL;
448 goto finalize;
449 }
450 Gia_ManStop( pSrm );
451
452 // update the manager
453 pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
454 if ( p->pAig == NULL )
455 {
456 p->pAig = pTemp;
457 break;
458 }
459 Gia_ManStop( pTemp );
460 if ( p->pPars->fVerbose )
461 {
462 Abc_Print( 1, "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ",
463 i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) );
464 Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
465 }
466 if ( Gia_ManAndNum(p->pAig) == 0 )
467 {
468 if ( p->pPars->fVerbose )
469 Abc_Print( 1, "Network after reduction is empty.\n" );
470 break;
471 }
472 // check resource limits
473 if ( p->pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
474 {
475 fTimeOut = 1;
476 break;
477 }
478 // if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved )
479 if ( p->nAllFailed > p->nAllProved + p->nAllDisproved )
480 {
481 if ( pParsSat->nBTLimit >= 10001 )
482 break;
483 if ( pPars->fSatSweeping )
484 {
485 if ( p->pPars->fVerbose )
486 Abc_Print( 1, "Exceeded the limit on the number of conflicts (%d).\n", pParsSat->nBTLimit );
487 break;
488 }
489 pParsSat->nBTLimit *= 10;
490 if ( p->pPars->fVerbose )
491 {
492 if ( p->pPars->fVerbose )
493 Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
494 if ( fOutputResult )
495 {
496 Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0, 0 );
497 Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
498 }
499 }
500 }
501 if ( pPars->fDualOut && pPars->fColorDiff && (Gia_ManAndNum(p->pAig) < 100000 || p->nAllProved + p->nAllDisproved < 10) )
502 {
503 if ( p->pPars->fVerbose )
504 Abc_Print( 1, "Switching into reduced mode.\n" );
505 pPars->fColorDiff = 0;
506 }
507 // if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
508 else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) )
509 {
510 if ( p->pPars->fVerbose )
511 Abc_Print( 1, "Switching into normal mode.\n" );
512 pPars->fColorDiff = 0;
513 pPars->fDualOut = 0;
514 }
515 }
516 finalize:
517 if ( p->pPars->fVerbose && p->pAig )
518 {
519 Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
520 Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig),
521 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
522 Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig),
523 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
524 Abc_PrintTimeP( 1, "Sim ", p->timeSim, Abc_Clock() - (int)clkTotal );
525 Abc_PrintTimeP( 1, "Sat ", p->timeSat-pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
526 Abc_PrintTimeP( 1, "Pat ", p->timePat+pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
527 Abc_PrintTime( 1, "Time", (int)(Abc_Clock() - clkTotal) );
528 }
529
530 pTemp = p->pAig; p->pAig = NULL;
531 if ( pTemp == NULL && pSim->iOut >= 0 )
532 {
533 if ( !fSilent )
534 Abc_Print( 1, "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
535 pPars->iOutFail = pSim->iOut;
536 }
537 else if ( pSim->pCexes && !fSilent )
538 Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts );
539 if ( fTimeOut && !fSilent )
540 Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
541
542 pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL;
543 Cec_ManSimStop( pSim );
544 Cec_ManPatStop( pPat );
545 Cec_ManFraStop( p );
546 return pTemp;
547 }
548
549
550 ////////////////////////////////////////////////////////////////////////
551 /// END OF FILE ///
552 ////////////////////////////////////////////////////////////////////////
553
554
555 ABC_NAMESPACE_IMPL_END
556
557