1 /**CFile****************************************************************
2
3 FileName [abcVerify.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Combinational and sequential verification for two networks.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcVerify.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "base/main/main.h"
23 #include "base/cmd/cmd.h"
24 #include "proof/fraig/fraig.h"
25 #include "opt/sim/sim.h"
26 #include "aig/aig/aig.h"
27 #include "aig/saig/saig.h"
28 #include "aig/gia/gia.h"
29 #include "proof/ssw/ssw.h"
30
31 ABC_NAMESPACE_IMPL_START
32
33
34 ////////////////////////////////////////////////////////////////////////
35 /// DECLARATIONS ///
36 ////////////////////////////////////////////////////////////////////////
37
38 static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
39 extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
40
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 /**Function*************************************************************
46
47 Synopsis [Verifies combinational equivalence by brute-force SAT.]
48
49 Description []
50
51 SideEffects []
52
53 SeeAlso []
54
55 ***********************************************************************/
Abc_NtkCecSat(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nConfLimit,int nInsLimit)56 void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit )
57 {
58 extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
59 Abc_Ntk_t * pMiter;
60 Abc_Ntk_t * pCnf;
61 int RetValue;
62
63 // get the miter of the two networks
64 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 );
65 if ( pMiter == NULL )
66 {
67 printf( "Miter computation has failed.\n" );
68 return;
69 }
70 RetValue = Abc_NtkMiterIsConstant( pMiter );
71 if ( RetValue == 0 )
72 {
73 printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
74 // report the error
75 pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
76 Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
77 ABC_FREE( pMiter->pModel );
78 Abc_NtkDelete( pMiter );
79 return;
80 }
81 if ( RetValue == 1 )
82 {
83 Abc_NtkDelete( pMiter );
84 printf( "Networks are equivalent after structural hashing.\n" );
85 return;
86 }
87
88 // convert the miter into a CNF
89 pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 );
90 Abc_NtkDelete( pMiter );
91 if ( pCnf == NULL )
92 {
93 printf( "Renoding for CNF has failed.\n" );
94 return;
95 }
96
97 // solve the CNF using the SAT solver
98 RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, 0, NULL, NULL );
99 if ( RetValue == -1 )
100 printf( "Networks are undecided (SAT solver timed out).\n" );
101 else if ( RetValue == 0 )
102 printf( "Networks are NOT EQUIVALENT after SAT.\n" );
103 else
104 printf( "Networks are equivalent after SAT.\n" );
105 if ( pCnf->pModel )
106 Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel );
107 ABC_FREE( pCnf->pModel );
108 Abc_NtkDelete( pCnf );
109 }
110
111
112 /**Function*************************************************************
113
114 Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
115
116 Description []
117
118 SideEffects []
119
120 SeeAlso []
121
122 ***********************************************************************/
Abc_NtkCecFraig(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nSeconds,int fVerbose)123 void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
124 {
125 abctime clk = Abc_Clock();
126 Prove_Params_t Params, * pParams = &Params;
127 // Fraig_Params_t Params;
128 // Fraig_Man_t * pMan;
129 Abc_Ntk_t * pMiter, * pTemp;
130 Abc_Ntk_t * pExdc = NULL;
131 int RetValue;
132
133 if ( pNtk1->pExdc != NULL || pNtk2->pExdc != NULL )
134 {
135 if ( pNtk1->pExdc != NULL && pNtk2->pExdc != NULL )
136 {
137 printf( "Comparing EXDC of the two networks:\n" );
138 Abc_NtkCecFraig( pNtk1->pExdc, pNtk2->pExdc, nSeconds, fVerbose );
139 printf( "Comparing networks under EXDC of the first network.\n" );
140 pExdc = pNtk1->pExdc;
141 }
142 else if ( pNtk1->pExdc != NULL )
143 {
144 printf( "Second network has no EXDC. Comparing main networks under EXDC of the first network.\n" );
145 pExdc = pNtk1->pExdc;
146 }
147 else if ( pNtk2->pExdc != NULL )
148 {
149 printf( "First network has no EXDC. Comparing main networks under EXDC of the second network.\n" );
150 pExdc = pNtk2->pExdc;
151 }
152 else assert( 0 );
153 }
154
155 // get the miter of the two networks
156 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0, 0 );
157 if ( pMiter == NULL )
158 {
159 printf( "Miter computation has failed.\n" );
160 return;
161 }
162 // add EXDC to the miter
163 if ( pExdc )
164 {
165 assert( Abc_NtkPoNum(pMiter) == 1 );
166 assert( Abc_NtkPoNum(pExdc) == 1 );
167 pMiter = Abc_NtkMiter( pTemp = pMiter, pExdc, 1, 0, 1, 0 );
168 Abc_NtkDelete( pTemp );
169 }
170 // handle trivial case
171 RetValue = Abc_NtkMiterIsConstant( pMiter );
172 if ( RetValue == 0 )
173 {
174 printf( "Networks are NOT EQUIVALENT after structural hashing. " );
175 // report the error
176 pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
177 Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
178 ABC_FREE( pMiter->pModel );
179 Abc_NtkDelete( pMiter );
180 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
181 return;
182 }
183 if ( RetValue == 1 )
184 {
185 printf( "Networks are equivalent after structural hashing. " );
186 Abc_NtkDelete( pMiter );
187 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
188 return;
189 }
190 /*
191 // convert the miter into a FRAIG
192 Fraig_ParamsSetDefault( &Params );
193 Params.fVerbose = fVerbose;
194 Params.nSeconds = nSeconds;
195 // Params.fFuncRed = 0;
196 // Params.nPatsRand = 0;
197 // Params.nPatsDyna = 0;
198 pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 );
199 Fraig_ManProveMiter( pMan );
200
201 // analyze the result
202 RetValue = Fraig_ManCheckMiter( pMan );
203 // report the result
204 if ( RetValue == -1 )
205 printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
206 else if ( RetValue == 1 )
207 printf( "Networks are equivalent after fraiging.\n" );
208 else if ( RetValue == 0 )
209 {
210 printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
211 Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) );
212 }
213 else assert( 0 );
214 // delete the fraig manager
215 Fraig_ManFree( pMan );
216 // delete the miter
217 Abc_NtkDelete( pMiter );
218 */
219 // solve the CNF using the SAT solver
220 Prove_ParamsSetDefault( pParams );
221 pParams->nItersMax = 5;
222 // RetValue = Abc_NtkMiterProve( &pMiter, pParams );
223 // pParams->fVerbose = 1;
224 RetValue = Abc_NtkIvyProve( &pMiter, pParams );
225 if ( RetValue == -1 )
226 printf( "Networks are undecided (resource limits is reached). " );
227 else if ( RetValue == 0 )
228 {
229 int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel );
230 if ( pSimInfo[0] != 1 )
231 printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
232 else
233 printf( "Networks are NOT EQUIVALENT. " );
234 ABC_FREE( pSimInfo );
235 }
236 else
237 printf( "Networks are equivalent. " );
238 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
239 if ( pMiter->pModel )
240 Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
241 Abc_NtkDelete( pMiter );
242 }
243
244 /**Function*************************************************************
245
246 Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
247
248 Description []
249
250 SideEffects []
251
252 SeeAlso []
253
254 ***********************************************************************/
Abc_NtkCecFraigPart(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nSeconds,int nPartSize,int fVerbose)255 void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose )
256 {
257 Prove_Params_t Params, * pParams = &Params;
258 Abc_Ntk_t * pMiter, * pMiterPart;
259 Abc_Obj_t * pObj;
260 int i, RetValue, Status, nOutputs;
261
262 // solve the CNF using the SAT solver
263 Prove_ParamsSetDefault( pParams );
264 pParams->nItersMax = 5;
265 // pParams->fVerbose = 1;
266
267 assert( nPartSize > 0 );
268
269 // get the miter of the two networks
270 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize, 0, 0 );
271 if ( pMiter == NULL )
272 {
273 printf( "Miter computation has failed.\n" );
274 return;
275 }
276 RetValue = Abc_NtkMiterIsConstant( pMiter );
277 if ( RetValue == 0 )
278 {
279 printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
280 // report the error
281 pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
282 Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
283 ABC_FREE( pMiter->pModel );
284 Abc_NtkDelete( pMiter );
285 return;
286 }
287 if ( RetValue == 1 )
288 {
289 printf( "Networks are equivalent after structural hashing.\n" );
290 Abc_NtkDelete( pMiter );
291 return;
292 }
293
294 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
295
296 // solve the problem iteratively for each output of the miter
297 Status = 1;
298 nOutputs = 0;
299 Abc_NtkForEachPo( pMiter, pObj, i )
300 {
301 if ( Abc_ObjFanin0(pObj) == Abc_AigConst1(pMiter) )
302 {
303 if ( Abc_ObjFaninC0(pObj) ) // complemented -> const 0
304 RetValue = 1;
305 else
306 RetValue = 0;
307 pMiterPart = NULL;
308 }
309 else
310 {
311 // get the cone of this output
312 pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
313 if ( Abc_ObjFaninC0(pObj) )
314 Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
315 // solve the cone
316 // RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
317 RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
318 }
319
320 if ( RetValue == -1 )
321 {
322 printf( "Networks are undecided (resource limits is reached).\r" );
323 Status = -1;
324 }
325 else if ( RetValue == 0 )
326 {
327 int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
328 if ( pSimInfo[0] != 1 )
329 printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
330 else
331 printf( "Networks are NOT EQUIVALENT. \n" );
332 ABC_FREE( pSimInfo );
333 Status = 0;
334 break;
335 }
336 else
337 {
338 printf( "Finished part %5d (out of %5d)\r", i+1, Abc_NtkPoNum(pMiter) );
339 nOutputs += nPartSize;
340 }
341 // if ( pMiter->pModel )
342 // Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
343 if ( pMiterPart )
344 Abc_NtkDelete( pMiterPart );
345 }
346
347 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
348
349 if ( Status == 1 )
350 printf( "Networks are equivalent. \n" );
351 else if ( Status == -1 )
352 printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
353 Abc_NtkDelete( pMiter );
354 }
355
356 /**Function*************************************************************
357
358 Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
359
360 Description []
361
362 SideEffects []
363
364 SeeAlso []
365
366 ***********************************************************************/
Abc_NtkCecFraigPartAuto(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nSeconds,int fVerbose)367 void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
368 {
369 extern Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
370 extern void Abc_NtkConvertCos( Abc_Ntk_t * pNtk, Vec_Int_t * vOuts, Vec_Ptr_t * vOnePtr );
371
372 Vec_Ptr_t * vParts, * vOnePtr;
373 Vec_Int_t * vOne;
374 Prove_Params_t Params, * pParams = &Params;
375 Abc_Ntk_t * pMiter, * pMiterPart;
376 int i, RetValue, Status, nOutputs;
377
378 // solve the CNF using the SAT solver
379 Prove_ParamsSetDefault( pParams );
380 pParams->nItersMax = 5;
381 // pParams->fVerbose = 1;
382
383 // get the miter of the two networks
384 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1, 0, 0 );
385 if ( pMiter == NULL )
386 {
387 printf( "Miter computation has failed.\n" );
388 return;
389 }
390 RetValue = Abc_NtkMiterIsConstant( pMiter );
391 if ( RetValue == 0 )
392 {
393 printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
394 // report the error
395 pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
396 Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
397 ABC_FREE( pMiter->pModel );
398 Abc_NtkDelete( pMiter );
399 return;
400 }
401 if ( RetValue == 1 )
402 {
403 printf( "Networks are equivalent after structural hashing.\n" );
404 Abc_NtkDelete( pMiter );
405 return;
406 }
407
408 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
409
410 // partition the outputs
411 vParts = Abc_NtkPartitionSmart( pMiter, 300, 0 );
412
413 // fraig each partition
414 Status = 1;
415 nOutputs = 0;
416 vOnePtr = Vec_PtrAlloc( 1000 );
417 Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i )
418 {
419 // get this part of the miter
420 Abc_NtkConvertCos( pMiter, vOne, vOnePtr );
421 pMiterPart = Abc_NtkCreateConeArray( pMiter, vOnePtr, 0 );
422 Abc_NtkCombinePos( pMiterPart, 0, 0 );
423 // check the miter for being constant
424 RetValue = Abc_NtkMiterIsConstant( pMiterPart );
425 if ( RetValue == 0 )
426 {
427 printf( "Networks are NOT EQUIVALENT after partitioning.\n" );
428 Abc_NtkDelete( pMiterPart );
429 break;
430 }
431 if ( RetValue == 1 )
432 {
433 Abc_NtkDelete( pMiterPart );
434 continue;
435 }
436 printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
437 i+1, Vec_PtrSize(vParts), Abc_NtkPiNum(pMiterPart), Abc_NtkPoNum(pMiterPart),
438 Abc_NtkNodeNum(pMiterPart), Abc_AigLevel(pMiterPart) );
439 fflush( stdout );
440 // solve the problem
441 RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
442 if ( RetValue == -1 )
443 {
444 printf( "Networks are undecided (resource limits is reached).\r" );
445 Status = -1;
446 }
447 else if ( RetValue == 0 )
448 {
449 int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
450 if ( pSimInfo[0] != 1 )
451 printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
452 else
453 printf( "Networks are NOT EQUIVALENT. \n" );
454 ABC_FREE( pSimInfo );
455 Status = 0;
456 Abc_NtkDelete( pMiterPart );
457 break;
458 }
459 else
460 {
461 // printf( "Finished part %5d (out of %5d)\r", i+1, Vec_PtrSize(vParts) );
462 nOutputs += Vec_IntSize(vOne);
463 }
464 Abc_NtkDelete( pMiterPart );
465 }
466 printf( " \r" );
467 Vec_VecFree( (Vec_Vec_t *)vParts );
468 Vec_PtrFree( vOnePtr );
469
470 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
471
472 if ( Status == 1 )
473 printf( "Networks are equivalent. \n" );
474 else if ( Status == -1 )
475 printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
476 Abc_NtkDelete( pMiter );
477 }
478
479 /**Function*************************************************************
480
481 Synopsis [Verifies sequential equivalence by brute-force SAT.]
482
483 Description []
484
485 SideEffects []
486
487 SeeAlso []
488
489 ***********************************************************************/
Abc_NtkSecSat(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nConfLimit,int nInsLimit,int nFrames)490 void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames )
491 {
492 extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
493 Abc_Ntk_t * pMiter;
494 Abc_Ntk_t * pFrames;
495 Abc_Ntk_t * pCnf;
496 int RetValue;
497
498 // get the miter of the two networks
499 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
500 if ( pMiter == NULL )
501 {
502 printf( "Miter computation has failed.\n" );
503 return;
504 }
505 RetValue = Abc_NtkMiterIsConstant( pMiter );
506 if ( RetValue == 0 )
507 {
508 Abc_NtkDelete( pMiter );
509 printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
510 return;
511 }
512 if ( RetValue == 1 )
513 {
514 Abc_NtkDelete( pMiter );
515 printf( "Networks are equivalent after structural hashing.\n" );
516 return;
517 }
518
519 // create the timeframes
520 pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
521 Abc_NtkDelete( pMiter );
522 if ( pFrames == NULL )
523 {
524 printf( "Frames computation has failed.\n" );
525 return;
526 }
527 RetValue = Abc_NtkMiterIsConstant( pFrames );
528 if ( RetValue == 0 )
529 {
530 Abc_NtkDelete( pFrames );
531 printf( "Networks are NOT EQUIVALENT after framing.\n" );
532 return;
533 }
534 if ( RetValue == 1 )
535 {
536 Abc_NtkDelete( pFrames );
537 printf( "Networks are equivalent after framing.\n" );
538 return;
539 }
540
541 // convert the miter into a CNF
542 pCnf = Abc_NtkMulti( pFrames, 0, 100, 1, 0, 0, 0 );
543 Abc_NtkDelete( pFrames );
544 if ( pCnf == NULL )
545 {
546 printf( "Renoding for CNF has failed.\n" );
547 return;
548 }
549
550 // solve the CNF using the SAT solver
551 RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, 0, NULL, NULL );
552 if ( RetValue == -1 )
553 printf( "Networks are undecided (SAT solver timed out).\n" );
554 else if ( RetValue == 0 )
555 printf( "Networks are NOT EQUIVALENT after SAT.\n" );
556 else
557 printf( "Networks are equivalent after SAT.\n" );
558 Abc_NtkDelete( pCnf );
559 }
560
561 /**Function*************************************************************
562
563 Synopsis [Verifies combinational equivalence by fraiging followed by SAT]
564
565 Description []
566
567 SideEffects []
568
569 SeeAlso []
570
571 ***********************************************************************/
Abc_NtkSecFraig(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nSeconds,int nFrames,int fVerbose)572 int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose )
573 {
574 Fraig_Params_t Params;
575 Fraig_Man_t * pMan;
576 Abc_Ntk_t * pMiter;
577 Abc_Ntk_t * pFrames;
578 int RetValue;
579
580 // get the miter of the two networks
581 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
582 if ( pMiter == NULL )
583 {
584 printf( "Miter computation has failed.\n" );
585 return 0;
586 }
587 RetValue = Abc_NtkMiterIsConstant( pMiter );
588 if ( RetValue == 0 )
589 {
590 printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
591 // report the error
592 pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
593 Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
594 ABC_FREE( pMiter->pModel );
595 Abc_NtkDelete( pMiter );
596 return 0;
597 }
598 if ( RetValue == 1 )
599 {
600 Abc_NtkDelete( pMiter );
601 printf( "Networks are equivalent after structural hashing.\n" );
602 return 1;
603 }
604
605 // create the timeframes
606 pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
607 Abc_NtkDelete( pMiter );
608 if ( pFrames == NULL )
609 {
610 printf( "Frames computation has failed.\n" );
611 return 0;
612 }
613 RetValue = Abc_NtkMiterIsConstant( pFrames );
614 if ( RetValue == 0 )
615 {
616 printf( "Networks are NOT EQUIVALENT after framing.\n" );
617 // report the error
618 pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
619 // Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
620 ABC_FREE( pFrames->pModel );
621 Abc_NtkDelete( pFrames );
622 return 0;
623 }
624 if ( RetValue == 1 )
625 {
626 Abc_NtkDelete( pFrames );
627 printf( "Networks are equivalent after framing.\n" );
628 return 1;
629 }
630
631 // convert the miter into a FRAIG
632 Fraig_ParamsSetDefault( &Params );
633 Params.fVerbose = fVerbose;
634 Params.nSeconds = nSeconds;
635 // Params.fFuncRed = 0;
636 // Params.nPatsRand = 0;
637 // Params.nPatsDyna = 0;
638 pMan = (Fraig_Man_t *)Abc_NtkToFraig( pFrames, &Params, 0, 0 );
639 Fraig_ManProveMiter( pMan );
640
641 // analyze the result
642 RetValue = Fraig_ManCheckMiter( pMan );
643 // report the result
644 if ( RetValue == -1 )
645 printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
646 else if ( RetValue == 1 )
647 printf( "Networks are equivalent after fraiging.\n" );
648 else if ( RetValue == 0 )
649 {
650 printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
651 // Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
652 }
653 else assert( 0 );
654 // delete the fraig manager
655 Fraig_ManFree( pMan );
656 // delete the miter
657 Abc_NtkDelete( pFrames );
658 return RetValue == 1;
659 }
660
661 /**Function*************************************************************
662
663 Synopsis [Returns a dummy pattern full of zeros.]
664
665 Description []
666
667 SideEffects []
668
669 SeeAlso []
670
671 ***********************************************************************/
Abc_NtkVerifyGetCleanModel(Abc_Ntk_t * pNtk,int nFrames)672 int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
673 {
674 int * pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) * nFrames );
675 memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) * nFrames );
676 return pModel;
677 }
678
679 /**Function*************************************************************
680
681 Synopsis [Returns the PO values under the given input pattern.]
682
683 Description []
684
685 SideEffects []
686
687 SeeAlso []
688
689 ***********************************************************************/
Abc_NtkVerifySimulatePattern(Abc_Ntk_t * pNtk,int * pModel)690 int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
691 {
692 Abc_Obj_t * pNode;
693 int * pValues, Value0, Value1, i;
694 int fStrashed = 0;
695 if ( !Abc_NtkIsStrash(pNtk) )
696 {
697 pNtk = Abc_NtkStrash(pNtk, 0, 0, 0);
698 fStrashed = 1;
699 }
700 /*
701 printf( "Counter example: " );
702 Abc_NtkForEachCi( pNtk, pNode, i )
703 printf( " %d", pModel[i] );
704 printf( "\n" );
705 */
706 // increment the trav ID
707 Abc_NtkIncrementTravId( pNtk );
708 // set the CI values
709 Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)1;
710 Abc_NtkForEachCi( pNtk, pNode, i )
711 pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)pModel[i];
712 // simulate in the topological order
713 Abc_NtkForEachNode( pNtk, pNode, i )
714 {
715 Value0 = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ (int)Abc_ObjFaninC0(pNode);
716 Value1 = ((int)(ABC_PTRINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ (int)Abc_ObjFaninC1(pNode);
717 pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)(Value0 & Value1);
718 }
719 // fill the output values
720 pValues = ABC_ALLOC( int, Abc_NtkCoNum(pNtk) );
721 Abc_NtkForEachCo( pNtk, pNode, i )
722 pValues[i] = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ (int)Abc_ObjFaninC0(pNode);
723 if ( fStrashed )
724 Abc_NtkDelete( pNtk );
725 return pValues;
726 }
727
728
729 /**Function*************************************************************
730
731 Synopsis [Reports mismatch between the two networks.]
732
733 Description []
734
735 SideEffects []
736
737 SeeAlso []
738
739 ***********************************************************************/
Abc_NtkVerifyReportError(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int * pModel)740 void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel )
741 {
742 Vec_Ptr_t * vNodes;
743 Abc_Obj_t * pNode;
744 int * pValues1, * pValues2;
745 int nErrors, nPrinted, i, iNode = -1;
746
747 assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
748 assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
749 // get the CO values under this model
750 pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
751 pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
752 // count the mismatches
753 nErrors = 0;
754 for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
755 nErrors += (int)( pValues1[i] != pValues2[i] );
756 printf( "Verification failed for at least %d outputs: ", nErrors );
757 // print the first 3 outputs
758 nPrinted = 0;
759 for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
760 if ( pValues1[i] != pValues2[i] )
761 {
762 if ( iNode == -1 )
763 iNode = i;
764 printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
765 if ( ++nPrinted == 3 )
766 break;
767 }
768 if ( nPrinted != nErrors )
769 printf( " ..." );
770 printf( "\n" );
771 // report mismatch for the first output
772 if ( iNode >= 0 )
773 {
774 printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n",
775 Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] );
776 printf( "Input pattern: " );
777 // collect PIs in the cone
778 pNode = Abc_NtkCo(pNtk1,iNode);
779 vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
780 // set the PI numbers
781 Abc_NtkForEachCi( pNtk1, pNode, i )
782 pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)i;
783 // print the model
784 pNode = (Abc_Obj_t *)Vec_PtrEntry( vNodes, 0 );
785 if ( Abc_ObjIsCi(pNode) )
786 {
787 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
788 {
789 assert( Abc_ObjIsCi(pNode) );
790 printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)(ABC_PTRINT_T)pNode->pCopy] );
791 }
792 }
793 printf( "\n" );
794 Vec_PtrFree( vNodes );
795 }
796 ABC_FREE( pValues1 );
797 ABC_FREE( pValues2 );
798 }
799
800
801 /**Function*************************************************************
802
803 Synopsis [Computes the COs in the support of the PO in the given frame.]
804
805 Description []
806
807 SideEffects []
808
809 SeeAlso []
810
811 ***********************************************************************/
Abc_NtkGetSeqPoSupp(Abc_Ntk_t * pNtk,int iFrame,int iNumPo)812 void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
813 {
814 Abc_Ntk_t * pFrames;
815 Abc_Obj_t * pObj, * pNodePo;
816 Vec_Ptr_t * vSupp;
817 int i, k;
818 // get the timeframes of the network
819 pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0, 0 );
820 //Abc_NtkShowAig( pFrames );
821
822 // get the PO of the timeframes
823 pNodePo = Abc_NtkPo( pFrames, iFrame * Abc_NtkPoNum(pNtk) + iNumPo );
824 // set the support
825 vSupp = Abc_NtkNodeSupport( pFrames, &pNodePo, 1 );
826 // mark the support of the frames
827 Abc_NtkForEachCi( pFrames, pObj, i )
828 pObj->pCopy = NULL;
829 Vec_PtrForEachEntry( Abc_Obj_t *, vSupp, pObj, i )
830 pObj->pCopy = (Abc_Obj_t *)1;
831 // mark the support of the network if the support of the timeframes is marked
832 Abc_NtkForEachCi( pNtk, pObj, i )
833 pObj->pCopy = NULL;
834 Abc_NtkForEachLatch( pNtk, pObj, i )
835 if ( Abc_NtkBox(pFrames, i)->pCopy )
836 pObj->pCopy = (Abc_Obj_t *)1;
837 Abc_NtkForEachPi( pNtk, pObj, i )
838 for ( k = 0; k <= iFrame; k++ )
839 if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
840 pObj->pCopy = (Abc_Obj_t *)1;
841 // free stuff
842 Vec_PtrFree( vSupp );
843 Abc_NtkDelete( pFrames );
844 }
845
846 /**Function*************************************************************
847
848 Synopsis [Reports mismatch between the two sequential networks.]
849
850 Description []
851
852 SideEffects []
853
854 SeeAlso []
855
856 ***********************************************************************/
Abc_NtkVerifyReportErrorSeq(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int * pModel,int nFrames)857 void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames )
858 {
859 Vec_Ptr_t * vInfo1, * vInfo2;
860 Abc_Obj_t * pObj, * pObjError, * pObj1, * pObj2;
861 int ValueError1 = -1, ValueError2 = -1;
862 unsigned * pPats1, * pPats2;
863 int i, o, k, nErrors, iFrameError = -1, iNodePo = -1, nPrinted;
864 int fRemove1 = 0, fRemove2 = 0;
865
866 if ( !Abc_NtkIsStrash(pNtk1) )
867 fRemove1 = 1, pNtk1 = Abc_NtkStrash( pNtk1, 0, 0, 0 );
868 if ( !Abc_NtkIsStrash(pNtk2) )
869 fRemove2 = 1, pNtk2 = Abc_NtkStrash( pNtk2, 0, 0, 0 );
870
871 // simulate sequential circuits
872 vInfo1 = Sim_SimulateSeqModel( pNtk1, nFrames, pModel );
873 vInfo2 = Sim_SimulateSeqModel( pNtk2, nFrames, pModel );
874
875 // look for a discrepancy in the PO values
876 nErrors = 0;
877 pObjError = NULL;
878 for ( i = 0; i < nFrames; i++ )
879 {
880 if ( pObjError )
881 break;
882 Abc_NtkForEachPo( pNtk1, pObj1, o )
883 {
884 pObj2 = Abc_NtkPo( pNtk2, o );
885 pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
886 pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
887 if ( pPats1[i] == pPats2[i] )
888 continue;
889 nErrors++;
890 if ( pObjError == NULL )
891 {
892 pObjError = pObj1;
893 iFrameError = i;
894 iNodePo = o;
895 ValueError1 = (pPats1[i] > 0);
896 ValueError2 = (pPats2[i] > 0);
897 }
898 }
899 }
900
901 if ( pObjError == NULL )
902 {
903 printf( "No output mismatches detected.\n" );
904 Sim_UtilInfoFree( vInfo1 );
905 Sim_UtilInfoFree( vInfo2 );
906 if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
907 if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
908 return;
909 }
910
911 printf( "Verification failed for at least %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
912 // print the first 3 outputs
913 nPrinted = 0;
914 Abc_NtkForEachPo( pNtk1, pObj1, o )
915 {
916 pObj2 = Abc_NtkPo( pNtk2, o );
917 pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
918 pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
919 if ( pPats1[iFrameError] == pPats2[iFrameError] )
920 continue;
921 printf( " %s", Abc_ObjName(pObj1) );
922 if ( ++nPrinted == 3 )
923 break;
924 }
925 if ( nPrinted != nErrors )
926 printf( " ..." );
927 printf( "\n" );
928
929 // mark CIs of the networks in the cone of influence of this output
930 Abc_NtkGetSeqPoSupp( pNtk1, iFrameError, iNodePo );
931 Abc_NtkGetSeqPoSupp( pNtk2, iFrameError, iNodePo );
932
933 // report mismatch for the first output
934 printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n",
935 Abc_ObjName(pObjError), ValueError1, ValueError2 );
936
937 printf( "The cone of influence of output %s in Network1:\n", Abc_ObjName(pObjError) );
938 printf( "PIs: " );
939 Abc_NtkForEachPi( pNtk1, pObj, i )
940 if ( pObj->pCopy )
941 printf( "%s ", Abc_ObjName(pObj) );
942 printf( "\n" );
943 printf( "Latches: " );
944 Abc_NtkForEachLatch( pNtk1, pObj, i )
945 if ( pObj->pCopy )
946 printf( "%s ", Abc_ObjName(pObj) );
947 printf( "\n" );
948
949 printf( "The cone of influence of output %s in Network2:\n", Abc_ObjName(pObjError) );
950 printf( "PIs: " );
951 Abc_NtkForEachPi( pNtk2, pObj, i )
952 if ( pObj->pCopy )
953 printf( "%s ", Abc_ObjName(pObj) );
954 printf( "\n" );
955 printf( "Latches: " );
956 Abc_NtkForEachLatch( pNtk2, pObj, i )
957 if ( pObj->pCopy )
958 printf( "%s ", Abc_ObjName(pObj) );
959 printf( "\n" );
960
961 // print the patterns
962 for ( i = 0; i <= iFrameError; i++ )
963 {
964 printf( "Frame %d: ", i+1 );
965
966 printf( "PI(1):" );
967 Abc_NtkForEachPi( pNtk1, pObj, k )
968 if ( pObj->pCopy )
969 printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
970 printf( " " );
971 printf( "L(1):" );
972 Abc_NtkForEachLatch( pNtk1, pObj, k )
973 if ( pObj->pCopy )
974 printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
975 printf( " " );
976 printf( "%s(1):", Abc_ObjName(pObjError) );
977 printf( "%d", Sim_SimInfoGet(vInfo1, pObjError)[i] > 0 );
978
979 printf( " " );
980
981 printf( "PI(2):" );
982 Abc_NtkForEachPi( pNtk2, pObj, k )
983 if ( pObj->pCopy )
984 printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
985 printf( " " );
986 printf( "L(2):" );
987 Abc_NtkForEachLatch( pNtk2, pObj, k )
988 if ( pObj->pCopy )
989 printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
990 printf( " " );
991 printf( "%s(2):", Abc_ObjName(pObjError) );
992 printf( "%d", Sim_SimInfoGet(vInfo2, pObjError)[i] > 0 );
993
994 printf( "\n" );
995 }
996 Abc_NtkForEachCi( pNtk1, pObj, i )
997 pObj->pCopy = NULL;
998 Abc_NtkForEachCi( pNtk2, pObj, i )
999 pObj->pCopy = NULL;
1000
1001 Sim_UtilInfoFree( vInfo1 );
1002 Sim_UtilInfoFree( vInfo2 );
1003 if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
1004 if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
1005 }
1006
1007 /**Function*************************************************************
1008
1009 Synopsis [Simulates buggy miter emailed by Mike.]
1010
1011 Description []
1012
1013 SideEffects []
1014
1015 SeeAlso []
1016
1017 ***********************************************************************/
Abc_NtkSimulteBuggyMiter(Abc_Ntk_t * pNtk)1018 void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
1019 {
1020 Abc_Obj_t * pObj;
1021 int i;
1022 int * pModel1, * pModel2, * pResult1, * pResult2;
1023 char * vPiValues1 = "01001011100000000011010110101000000";
1024 char * vPiValues2 = "11001101011101011111110100100010001";
1025
1026 assert( strlen(vPiValues1) == (unsigned)Abc_NtkPiNum(pNtk) );
1027 assert( 1 == Abc_NtkPoNum(pNtk) );
1028
1029 pModel1 = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
1030 Abc_NtkForEachPi( pNtk, pObj, i )
1031 pModel1[i] = vPiValues1[i] - '0';
1032 Abc_NtkForEachLatch( pNtk, pObj, i )
1033 pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)(ABC_PTRINT_T)pObj->pData) - 1;
1034
1035 pResult1 = Abc_NtkVerifySimulatePattern( pNtk, pModel1 );
1036 printf( "Value = %d\n", pResult1[0] );
1037
1038 pModel2 = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) );
1039 Abc_NtkForEachPi( pNtk, pObj, i )
1040 pModel2[i] = vPiValues2[i] - '0';
1041 Abc_NtkForEachLatch( pNtk, pObj, i )
1042 pModel2[Abc_NtkPiNum(pNtk)+i] = pResult1[Abc_NtkPoNum(pNtk)+i];
1043
1044 pResult2 = Abc_NtkVerifySimulatePattern( pNtk, pModel2 );
1045 printf( "Value = %d\n", pResult2[0] );
1046
1047 ABC_FREE( pModel1 );
1048 ABC_FREE( pModel2 );
1049 ABC_FREE( pResult1 );
1050 ABC_FREE( pResult2 );
1051 }
1052
1053
1054 /**Function*************************************************************
1055
1056 Synopsis [Returns the PO values under the given input pattern.]
1057
1058 Description []
1059
1060 SideEffects []
1061
1062 SeeAlso []
1063
1064 ***********************************************************************/
Abc_NtkIsTrueCex(Abc_Ntk_t * pNtk,Abc_Cex_t * pCex)1065 int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
1066 {
1067 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
1068 Aig_Man_t * pMan;
1069 int status = 0, fStrashed = 0;
1070 if ( !Abc_NtkIsStrash(pNtk) )
1071 {
1072 pNtk = Abc_NtkStrash(pNtk, 0, 0, 0);
1073 fStrashed = 1;
1074 }
1075 pMan = Abc_NtkToDar( pNtk, 0, 1 );
1076 if ( pMan )
1077 {
1078 status = Saig_ManVerifyCex( pMan, pCex );
1079 Aig_ManStop( pMan );
1080 }
1081 if ( fStrashed )
1082 Abc_NtkDelete( pNtk );
1083 return status;
1084 }
1085
1086 /**Function*************************************************************
1087
1088 Synopsis [Returns 1 if the number of PIs matches.]
1089
1090 Description []
1091
1092 SideEffects []
1093
1094 SeeAlso []
1095
1096 ***********************************************************************/
Abc_NtkIsValidCex(Abc_Ntk_t * pNtk,Abc_Cex_t * pCex)1097 int Abc_NtkIsValidCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
1098 {
1099 return Abc_NtkPiNum(pNtk) == pCex->nPis;
1100 }
1101
1102
1103 ////////////////////////////////////////////////////////////////////////
1104 /// END OF FILE ///
1105 ////////////////////////////////////////////////////////////////////////
1106
1107
1108 ABC_NAMESPACE_IMPL_END
1109
1110