1 /**CFile****************************************************************
2
3 FileName [fraSec.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [Performs SEC based on seq sweeping.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22 #include "aig/ioa/ioa.h"
23 #include "proof/int/int.h"
24 #include "proof/ssw/ssw.h"
25 #include "aig/saig/saig.h"
26 #include "bdd/bbr/bbr.h"
27 #include "proof/pdr/pdr.h"
28
29 ABC_NAMESPACE_IMPL_START
30
31
32 ////////////////////////////////////////////////////////////////////////
33 /// DECLARATIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39
40 /**Function*************************************************************
41
42 Synopsis []
43
44 Description []
45
46 SideEffects []
47
48 SeeAlso []
49
50 ***********************************************************************/
Fra_SecSetDefaultParams(Fra_Sec_t * p)51 void Fra_SecSetDefaultParams( Fra_Sec_t * p )
52 {
53 memset( p, 0, sizeof(Fra_Sec_t) );
54 p->fTryComb = 1; // try CEC call as a preprocessing step
55 p->fTryBmc = 1; // try BMC call as a preprocessing step
56 p->nFramesMax = 4; // the max number of frames used for induction
57 p->nBTLimit = 1000; // conflict limit at a node during induction
58 p->nBTLimitGlobal = 5000000; // global conflict limit during induction
59 p->nBTLimitInter = 10000; // conflict limit during interpolation
60 p->nBddVarsMax = 150; // the limit on the number of registers in BDD reachability
61 p->nBddMax = 50000; // the limit on the number of BDD nodes
62 p->nBddIterMax = 1000000; // the limit on the number of BDD iterations
63 p->fPhaseAbstract = 0; // enables phase abstraction
64 p->fRetimeFirst = 1; // enables most-forward retiming at the beginning
65 p->fRetimeRegs = 1; // enables min-register retiming at the beginning
66 p->fFraiging = 1; // enables fraiging at the beginning
67 p->fInduction = 1; // enables the use of induction (signal correspondence)
68 p->fInterpolation = 1; // enables interpolation
69 p->fInterSeparate = 0; // enables interpolation for each outputs separately
70 p->fReachability = 1; // enables BDD based reachability
71 p->fReorderImage = 1; // enables variable reordering during image computation
72 p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove
73 p->fUseNewProver = 0; // enables new prover
74 p->fUsePdr = 1; // enables PDR
75 p->nPdrTimeout = 60; // enabled PDR timeout
76 p->fSilent = 0; // disables all output
77 p->fVerbose = 0; // enables verbose reporting of statistics
78 p->fVeryVerbose = 0; // enables very verbose reporting
79 p->TimeLimit = 0; // enables the timeout
80 // internal parameters
81 p->fReportSolution = 0; // enables specialized format for reporting solution
82 }
83
84 /**Function*************************************************************
85
86 Synopsis []
87
88 Description []
89
90 SideEffects []
91
92 SeeAlso []
93
94 ***********************************************************************/
Fra_FraigSec(Aig_Man_t * p,Fra_Sec_t * pParSec,Aig_Man_t ** ppResult)95 int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
96 {
97 Ssw_Pars_t Pars2, * pPars2 = &Pars2;
98 Fra_Ssw_t Pars, * pPars = &Pars;
99 Fra_Sml_t * pSml;
100 Aig_Man_t * pNew, * pTemp;
101 int nFrames, RetValue, nIter;
102 abctime clk, clkTotal = Abc_Clock();
103 int TimeOut = 0;
104 int fLatchCorr = 0;
105 float TimeLeft = 0.0;
106 pParSec->nSMnumber = -1;
107
108 // try the miter before solving
109 pNew = Aig_ManDupSimple( p );
110 RetValue = Fra_FraigMiterStatus( pNew );
111 if ( RetValue >= 0 )
112 goto finish;
113
114 // prepare parameters
115 memset( pPars, 0, sizeof(Fra_Ssw_t) );
116 pPars->fLatchCorr = fLatchCorr;
117 pPars->fVerbose = pParSec->fVeryVerbose;
118 if ( pParSec->fVerbose )
119 {
120 printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
121 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
122 }
123 //Aig_ManDumpBlif( pNew, "after.blif", NULL, NULL );
124
125 // perform sequential cleanup
126 clk = Abc_Clock();
127 if ( pNew->nRegs )
128 pNew = Aig_ManReduceLaches( pNew, 0 );
129 if ( pNew->nRegs )
130 pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
131 if ( pParSec->fVerbose )
132 {
133 printf( "Sequential cleanup: Latches = %5d. Nodes = %6d. ",
134 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
135 ABC_PRT( "Time", Abc_Clock() - clk );
136 }
137 RetValue = Fra_FraigMiterStatus( pNew );
138 if ( RetValue >= 0 )
139 goto finish;
140
141 // perform phase abstraction
142 clk = Abc_Clock();
143 if ( pParSec->fPhaseAbstract )
144 {
145 extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
146 pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew);
147 pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew);
148 pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
149 Aig_ManStop( pTemp );
150 if ( pParSec->fVerbose )
151 {
152 printf( "Phase abstraction: Latches = %5d. Nodes = %6d. ",
153 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
154 ABC_PRT( "Time", Abc_Clock() - clk );
155 }
156 }
157
158 // perform forward retiming
159 if ( pParSec->fRetimeFirst && pNew->nRegs )
160 {
161 clk = Abc_Clock();
162 // pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
163 pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 );
164 Aig_ManStop( pTemp );
165 if ( pParSec->fVerbose )
166 {
167 printf( "Forward retiming: Latches = %5d. Nodes = %6d. ",
168 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
169 ABC_PRT( "Time", Abc_Clock() - clk );
170 }
171 }
172
173 // run latch correspondence
174 clk = Abc_Clock();
175 if ( pNew->nRegs )
176 {
177 pNew = Aig_ManDupOrdered( pTemp = pNew );
178 // pNew = Aig_ManDupDfs( pTemp = pNew );
179 Aig_ManStop( pTemp );
180 /*
181 if ( RetValue == -1 && pParSec->TimeLimit )
182 {
183 TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
184 TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
185 if ( TimeLeft == 0.0 )
186 {
187 if ( !pParSec->fSilent )
188 printf( "Runtime limit exceeded.\n" );
189 RetValue = -1;
190 TimeOut = 1;
191 goto finish;
192 }
193 }
194 */
195
196 // pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
197 //Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL );
198 Ssw_ManSetDefaultParamsLcorr( pPars2 );
199 pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 );
200 nIter = pPars2->nIters;
201
202 // prepare parameters for scorr
203 Ssw_ManSetDefaultParams( pPars2 );
204
205 if ( pTemp->pSeqModel )
206 {
207 if ( !Saig_ManVerifyCex( pTemp, pTemp->pSeqModel ) )
208 printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
209 if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
210 printf( "The counter-example is invalid because of phase abstraction.\n" );
211 else
212 {
213 ABC_FREE( p->pSeqModel );
214 p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
215 ABC_FREE( pTemp->pSeqModel );
216 }
217 }
218 if ( pNew == NULL )
219 {
220 if ( p->pSeqModel )
221 {
222 RetValue = 0;
223 if ( !pParSec->fSilent )
224 {
225 printf( "Networks are NOT EQUIVALENT after simulation. " );
226 ABC_PRT( "Time", Abc_Clock() - clkTotal );
227 }
228 if ( pParSec->fReportSolution && !pParSec->fRecursive )
229 {
230 printf( "SOLUTION: FAIL " );
231 ABC_PRT( "Time", Abc_Clock() - clkTotal );
232 }
233 Aig_ManStop( pTemp );
234 return RetValue;
235 }
236 pNew = pTemp;
237 RetValue = -1;
238 TimeOut = 1;
239 goto finish;
240 }
241 Aig_ManStop( pTemp );
242
243 if ( pParSec->fVerbose )
244 {
245 printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
246 nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
247 ABC_PRT( "Time", Abc_Clock() - clk );
248 }
249 }
250 /*
251 if ( RetValue == -1 && pParSec->TimeLimit )
252 {
253 TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
254 TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
255 if ( TimeLeft == 0.0 )
256 {
257 if ( !pParSec->fSilent )
258 printf( "Runtime limit exceeded.\n" );
259 RetValue = -1;
260 TimeOut = 1;
261 goto finish;
262 }
263 }
264 */
265 // perform fraiging
266 if ( pParSec->fFraiging )
267 {
268 clk = Abc_Clock();
269 pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
270 Aig_ManStop( pTemp );
271 if ( pParSec->fVerbose )
272 {
273 printf( "Fraiging: Latches = %5d. Nodes = %6d. ",
274 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
275 ABC_PRT( "Time", Abc_Clock() - clk );
276 }
277 }
278
279 if ( pNew->nRegs == 0 )
280 RetValue = Fra_FraigCec( &pNew, 100000, 0 );
281
282 RetValue = Fra_FraigMiterStatus( pNew );
283 if ( RetValue >= 0 )
284 goto finish;
285 /*
286 if ( RetValue == -1 && pParSec->TimeLimit )
287 {
288 TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
289 TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
290 if ( TimeLeft == 0.0 )
291 {
292 if ( !pParSec->fSilent )
293 printf( "Runtime limit exceeded.\n" );
294 RetValue = -1;
295 TimeOut = 1;
296 goto finish;
297 }
298 }
299 */
300 // perform min-area retiming
301 if ( pParSec->fRetimeRegs && pNew->nRegs )
302 {
303 // extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
304 clk = Abc_Clock();
305 pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew);
306 pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew);
307 // pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
308 pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
309 Aig_ManStop( pTemp );
310 pNew = Aig_ManDupOrdered( pTemp = pNew );
311 Aig_ManStop( pTemp );
312 if ( pParSec->fVerbose )
313 {
314 printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
315 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
316 ABC_PRT( "Time", Abc_Clock() - clk );
317 }
318 }
319
320 // perform seq sweeping while increasing the number of frames
321 RetValue = Fra_FraigMiterStatus( pNew );
322 if ( RetValue == -1 && pParSec->fInduction )
323 for ( nFrames = 1; nFrames <= pParSec->nFramesMax; nFrames *= 2 )
324 {
325 /*
326 if ( RetValue == -1 && pParSec->TimeLimit )
327 {
328 TimeLeft = (float)pParSec->TimeLimit - ((float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
329 TimeLeft = Abc_MaxInt( TimeLeft, 0.0 );
330 if ( TimeLeft == 0.0 )
331 {
332 if ( !pParSec->fSilent )
333 printf( "Runtime limit exceeded.\n" );
334 RetValue = -1;
335 TimeOut = 1;
336 goto finish;
337 }
338 }
339 */
340
341 clk = Abc_Clock();
342 pPars->nFramesK = nFrames;
343 pPars->TimeLimit = TimeLeft;
344 pPars->fSilent = pParSec->fSilent;
345 // pNew = Fra_FraigInduction( pTemp = pNew, pPars );
346
347 pPars2->nFramesK = nFrames;
348 pPars2->nBTLimit = pParSec->nBTLimit;
349 pPars2->nBTLimitGlobal = pParSec->nBTLimitGlobal;
350 // pPars2->nBTLimit = 1000 * nFrames;
351
352 if ( RetValue == -1 && pPars2->nConflicts > pPars2->nBTLimitGlobal )
353 {
354 if ( !pParSec->fSilent )
355 printf( "Global conflict limit (%d) exceeded.\n", pPars2->nBTLimitGlobal );
356 RetValue = -1;
357 TimeOut = 1;
358 goto finish;
359 }
360
361 Aig_ManSetRegNum( pNew, pNew->nRegs );
362 // pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
363 if ( Aig_ManRegNum(pNew) > 0 )
364 pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 );
365 else
366 pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
367
368 if ( pNew == NULL )
369 {
370 pNew = pTemp;
371 RetValue = -1;
372 TimeOut = 1;
373 goto finish;
374 }
375
376 // printf( "Total conflicts = %d.\n", pPars2->nConflicts );
377
378 Aig_ManStop( pTemp );
379 RetValue = Fra_FraigMiterStatus( pNew );
380 if ( pParSec->fVerbose )
381 {
382 printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
383 nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
384 ABC_PRT( "Time", Abc_Clock() - clk );
385 }
386 if ( RetValue != -1 )
387 break;
388
389 // perform retiming
390 // if ( pParSec->fRetimeFirst && pNew->nRegs )
391 if ( pNew->nRegs )
392 {
393 // extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
394 clk = Abc_Clock();
395 pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew);
396 pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew);
397 // pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
398 pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
399 Aig_ManStop( pTemp );
400 pNew = Aig_ManDupOrdered( pTemp = pNew );
401 Aig_ManStop( pTemp );
402 if ( pParSec->fVerbose )
403 {
404 printf( "Min-reg retiming: Latches = %5d. Nodes = %6d. ",
405 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
406 ABC_PRT( "Time", Abc_Clock() - clk );
407 }
408 }
409
410 if ( pNew->nRegs )
411 pNew = Aig_ManConstReduce( pNew, 0, -1, -1, 0, 0 );
412
413 // perform rewriting
414 clk = Abc_Clock();
415 pNew = Aig_ManDupOrdered( pTemp = pNew );
416 Aig_ManStop( pTemp );
417 // pNew = Dar_ManRewriteDefault( pTemp = pNew );
418 pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0, 0 );
419 Aig_ManStop( pTemp );
420 if ( pParSec->fVerbose )
421 {
422 printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
423 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
424 ABC_PRT( "Time", Abc_Clock() - clk );
425 }
426
427 // perform sequential simulation
428 if ( pNew->nRegs )
429 {
430 clk = Abc_Clock();
431 pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000), 1 );
432 if ( pParSec->fVerbose )
433 {
434 printf( "Seq simulation : Latches = %5d. Nodes = %6d. ",
435 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
436 ABC_PRT( "Time", Abc_Clock() - clk );
437 }
438 if ( pSml->fNonConstOut )
439 {
440 pNew->pSeqModel = Fra_SmlGetCounterExample( pSml );
441 // transfer to the original manager
442 if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
443 printf( "The counter-example is invalid because of phase abstraction.\n" );
444 else
445 {
446 ABC_FREE( p->pSeqModel );
447 p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
448 ABC_FREE( pNew->pSeqModel );
449 }
450
451 Fra_SmlStop( pSml );
452 Aig_ManStop( pNew );
453 RetValue = 0;
454 if ( !pParSec->fSilent )
455 {
456 printf( "Networks are NOT EQUIVALENT after simulation. " );
457 ABC_PRT( "Time", Abc_Clock() - clkTotal );
458 }
459 if ( pParSec->fReportSolution && !pParSec->fRecursive )
460 {
461 printf( "SOLUTION: FAIL " );
462 ABC_PRT( "Time", Abc_Clock() - clkTotal );
463 }
464 return RetValue;
465 }
466 Fra_SmlStop( pSml );
467 }
468 }
469
470 // get the miter status
471 RetValue = Fra_FraigMiterStatus( pNew );
472
473 // try interplation
474 clk = Abc_Clock();
475 Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
476 if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
477 {
478 Inter_ManParams_t Pars, * pPars = &Pars;
479 int Depth;
480 ABC_FREE( pNew->pSeqModel );
481 Inter_ManSetDefaultParams( pPars );
482 // pPars->nBTLimit = 100;
483 pPars->nBTLimit = pParSec->nBTLimitInter;
484 pPars->fVerbose = pParSec->fVeryVerbose;
485 if ( Saig_ManPoNum(pNew) == 1 )
486 {
487 RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
488 }
489 else if ( pParSec->fInterSeparate )
490 {
491 Abc_Cex_t * pCex = NULL;
492 Aig_Man_t * pTemp, * pAux;
493 Aig_Obj_t * pObjPo;
494 int i, Counter = 0;
495 Saig_ManForEachPo( pNew, pObjPo, i )
496 {
497 if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) )
498 continue;
499 if ( pPars->fVerbose )
500 printf( "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pNew) );
501 pTemp = Aig_ManDupOneOutput( pNew, i, 1 );
502 pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
503 Aig_ManStop( pAux );
504 if ( Saig_ManRegNum(pTemp) > 0 )
505 {
506 RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
507 if ( pTemp->pSeqModel )
508 {
509 pCex = p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) );
510 pCex->iPo = i;
511 Aig_ManStop( pTemp );
512 break;
513 }
514 // if solved, remove the output
515 if ( RetValue == 1 )
516 {
517 Aig_ObjPatchFanin0( pNew, pObjPo, Aig_ManConst0(pNew) );
518 // printf( "Output %3d : Solved ", i );
519 }
520 else
521 {
522 Counter++;
523 // printf( "Output %3d : Undec ", i );
524 }
525 }
526 else
527 Counter++;
528 // Aig_ManPrintStats( pTemp );
529 Aig_ManStop( pTemp );
530 printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
531 }
532 Aig_ManCleanup( pNew );
533 if ( pCex == NULL )
534 {
535 printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pNew) );
536 if ( Counter )
537 RetValue = -1;
538 }
539 pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 );
540 Aig_ManStop( pTemp );
541 pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0, -1, -1, 0, 0 );
542 Aig_ManStop( pTemp );
543 }
544 else
545 {
546 Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
547 RetValue = Inter_ManPerformInterpolation( pNewOrpos, pPars, &Depth );
548 if ( pNewOrpos->pSeqModel )
549 {
550 Abc_Cex_t * pCex;
551 pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
552 pCex->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
553 }
554 Aig_ManStop( pNewOrpos );
555 }
556
557 if ( pParSec->fVerbose )
558 {
559 if ( RetValue == 1 )
560 printf( "Property proved using interpolation. " );
561 else if ( RetValue == 0 )
562 printf( "Property DISPROVED in frame %d using interpolation. ", Depth );
563 else if ( RetValue == -1 )
564 printf( "Property UNDECIDED after interpolation. " );
565 else
566 assert( 0 );
567 ABC_PRT( "Time", Abc_Clock() - clk );
568 }
569 }
570
571 // try reachability analysis
572 if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
573 {
574 Saig_ParBbr_t Pars, * pPars = &Pars;
575 Bbr_ManSetDefaultParams( pPars );
576 pPars->TimeLimit = 0;
577 pPars->nBddMax = pParSec->nBddMax;
578 pPars->nIterMax = pParSec->nBddIterMax;
579 pPars->fPartition = 1;
580 pPars->fReorder = 1;
581 pPars->fReorderImage = 1;
582 pPars->fVerbose = 0;
583 pPars->fSilent = pParSec->fSilent;
584 pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew);
585 pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew);
586 RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
587 }
588
589 // try PDR
590 if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
591 {
592 Pdr_Par_t Pars, * pPars = &Pars;
593 Pdr_ManSetDefaultParams( pPars );
594 pPars->nTimeOut = pParSec->nPdrTimeout;
595 pPars->fVerbose = pParSec->fVerbose;
596 if ( pParSec->fVerbose )
597 printf( "Running property directed reachability...\n" );
598 RetValue = Pdr_ManSolve( pNew, pPars );
599 if ( pNew->pSeqModel )
600 pNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
601 }
602
603 finish:
604 // report the miter
605 if ( RetValue == 1 )
606 {
607 if ( !pParSec->fSilent )
608 {
609 printf( "Networks are equivalent. " );
610 ABC_PRT( "Time", Abc_Clock() - clkTotal );
611 }
612 if ( pParSec->fReportSolution && !pParSec->fRecursive )
613 {
614 printf( "SOLUTION: PASS " );
615 ABC_PRT( "Time", Abc_Clock() - clkTotal );
616 }
617 }
618 else if ( RetValue == 0 )
619 {
620 if ( pNew->pSeqModel == NULL )
621 {
622 int i;
623 // if the CEX is not derives, it is because tricial CEX should be assumed
624 pNew->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pNew), pNew->nTruePis, 1 );
625 // if the CEX does not work, we need to change PIs to 1 because
626 // the only way it can happen is when a PO is equal to a PI...
627 if ( Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ) == -1 )
628 for ( i = 0; i < pNew->nTruePis; i++ )
629 Abc_InfoSetBit( pNew->pSeqModel->pData, i );
630 }
631 if ( !pParSec->fSilent )
632 {
633 printf( "Networks are NOT EQUIVALENT. " );
634 ABC_PRT( "Time", Abc_Clock() - clkTotal );
635 }
636 if ( pParSec->fReportSolution && !pParSec->fRecursive )
637 {
638 printf( "SOLUTION: FAIL " );
639 ABC_PRT( "Time", Abc_Clock() - clkTotal );
640 }
641 }
642 else
643 {
644 ///////////////////////////////////
645 // save intermediate result
646 extern void Abc_FrameSetSave1( void * pAig );
647 Abc_FrameSetSave1( Aig_ManDupSimple(pNew) );
648 ///////////////////////////////////
649 if ( !pParSec->fSilent )
650 {
651 printf( "Networks are UNDECIDED. " );
652 ABC_PRT( "Time", Abc_Clock() - clkTotal );
653 }
654 if ( pParSec->fReportSolution && !pParSec->fRecursive )
655 {
656 printf( "SOLUTION: UNDECIDED " );
657 ABC_PRT( "Time", Abc_Clock() - clkTotal );
658 }
659 if ( !TimeOut && !pParSec->fSilent )
660 {
661 static int Counter = 1;
662 char pFileName[1000];
663 pParSec->nSMnumber = Counter;
664 sprintf( pFileName, "sm%02d.aig", Counter++ );
665 Ioa_WriteAiger( pNew, pFileName, 0, 0 );
666 printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
667 }
668 }
669 if ( pNew->pSeqModel )
670 {
671 if ( Saig_ManPiNum(p) != Saig_ManPiNum(pNew) )
672 printf( "The counter-example is invalid because of phase abstraction.\n" );
673 else
674 {
675 ABC_FREE( p->pSeqModel );
676 p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) );
677 ABC_FREE( pNew->pSeqModel );
678 }
679 }
680 if ( ppResult != NULL )
681 *ppResult = Aig_ManDupSimpleDfs( pNew );
682 if ( pNew )
683 Aig_ManStop( pNew );
684 return RetValue;
685 }
686
687 ////////////////////////////////////////////////////////////////////////
688 /// END OF FILE ///
689 ////////////////////////////////////////////////////////////////////////
690
691
692 ABC_NAMESPACE_IMPL_END
693
694