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