source: vis_dev/vis-2.3/src/eqv/eqvCmd.c @ 30

Last change on this file since 30 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 41.6 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [eqvCmd.c]
4
5  PackageName [eqv]
6
7  Synopsis    [Implements the eqv commands.]
8
9  Description [This file initializes the eqv package and provides the
10  interface between the command line and the top level routine which does the
11  equivalence checking.]
12
13  Author      [Shaz Qadeer]
14
15  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
16  All rights reserved.
17
18  Permission is hereby granted, without written agreement and without license
19  or royalty fees, to use, copy, modify, and distribute this software and its
20  documentation for any purpose, provided that the above copyright notice and
21  the following two paragraphs appear in all copies of this software.
22
23  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
24  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
25  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
26  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27
28  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
29  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
30  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
31  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
32  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33
34******************************************************************************/
35
36#include "eqvInt.h"
37
38static char rcsid[] UNUSED = "$Id: eqvCmd.c,v 1.20 2009/04/11 18:26:04 fabio Exp $";
39
40/*---------------------------------------------------------------------------*/
41/* Variable declarations                                                     */
42/*---------------------------------------------------------------------------*/
43static jmp_buf timeOutEnv;
44
45
46/**AutomaticStart*************************************************************/
47
48/*---------------------------------------------------------------------------*/
49/* Static function prototypes                                                */
50/*---------------------------------------------------------------------------*/
51
52static int CommandCombEquivalence(Hrc_Manager_t **hmgr, int argc, char **argv);
53static int CommandSeqEquivalence(Hrc_Manager_t **hmgr, int argc, char **argv);
54static void TimeOutHandle(void);
55
56/**AutomaticEnd***************************************************************/
57
58
59/*---------------------------------------------------------------------------*/
60/* Definition of exported functions                                          */
61/*---------------------------------------------------------------------------*/
62
63/**Function********************************************************************
64
65  Synopsis    [This function initializes the eqv package.]
66
67  SideEffects []
68
69  SeeAlso     [Eqv_End()]
70
71******************************************************************************/
72void
73Eqv_Init(void)
74{
75  Cmd_CommandAdd("comb_verify", CommandCombEquivalence, 0);
76  Cmd_CommandAdd("seq_verify", CommandSeqEquivalence, 0);
77}
78
79/**Function********************************************************************
80
81  Synopsis    [This function ends the eqv package.]
82
83  SideEffects []
84
85  SeeAlso     [Eqv_Init()]
86
87******************************************************************************/
88void
89Eqv_End(void)
90{
91}
92
93/*---------------------------------------------------------------------------*/
94/* Definition of internal functions                                          */
95/*---------------------------------------------------------------------------*/
96
97/*---------------------------------------------------------------------------*/
98/* Definition of static functions                                            */
99/*---------------------------------------------------------------------------*/
100
101/**Function********************************************************************
102
103  Synopsis [This function sits between the command line and the top level
104  function which checks combinational equivalence.]
105
106  Description [The function parses the command line and generates the
107  arguments to the top level routine.]
108
109  SideEffects [If the variables of the network present at the current node of
110  the existing hierarchy have not been ordered, they get ordered.]
111
112  SeeAlso [Eqv_NetworkVerifyCombinationalEquivalence]
113
114  CommandName [comb_verify]
115
116  CommandSynopsis [verify the combinational equivalence of two flattened networks]
117
118  CommandArguments [ \[-b\] \[-f <filename>\] \[-h\] \[-o <ordering
119  method>\] \[-t <timeOut>\] \[-1 <partition method>\] \[-2
120  <partition method>\] \[-i\] <filename1> \[<filename2>\] ]
121
122  CommandDescription [This command verifies the combinational equivalence of
123  two flattened networks.  In particular, any set of functions (the roots),
124  defined over any set of intermediate variables (the leaves), can be checked
125  for equivalence between the two networks.  Roots and leaves are subsets of
126  the nodes of a network, with the restriction that the leaves should form a
127  complete support for the roots. The correspondence between the roots and the
128  leaves in the two networks is specified in a file given by the option -f
129  <filename>. The default option
130  assumes that the roots are the combinational outputs and the leaves are the
131  combinational inputs.<p>
132
133  When there is a pseudo input in the set of leaves, the range of values it
134  can take should be the same as that of the multi-valued variable
135  corresponding to it, for comb_verify to function correctly.
136  This restriction will be removed in future.<p>
137
138  There are two ways to do combinational verification.  In the first mode, two
139  BLIF-MV files are given as arguments to the command, e.g.<p>
140
141  <pre>
142  vis> comb_verify foo.mv bar.mv
143  </pre>
144
145  Verification is done for the flattened networks at the root nodes of the two
146  BLIF-MV hierarchies.  In any error messages printed, "network1" refers to
147  the first file, and "network2" refers to the second. Both of these networks
148  are freed at the end of the command. This mode is totally independent from
149  any existing hierarchy previously read in.
150
151  In the second mode, it is assumed that a hierarchy has already been read
152  in. Then, comb_verify can be called with a single BLIF-MV file, and this
153  will do the comparison between the network present at the current node
154  ("network1") and the network corresponding to the root node of the hierarchy
155  in the BLIF-MV file("network2"). A typical sequence of commands is:<p>
156
157  <pre>
158  vis> read_blifmv foo.mv
159  vis> init_verify
160  vis> comb_verify bar.mv
161  </pre>
162
163  If a hierarchy has been read in but a flattened network does not exist at
164  the current node (flatten_hierarchy has not been invoked), the command does
165  nothing. If a network exists at the
166  current node, but the variables haven't been ordered, then the variables are
167  ordered and a partition created. This partition is freed at the end. A
168  side-effect is that the variables are ordered. If a partition exists, then
169  it is used if the vertices corresponding to the roots specified are present
170  in it, otherwise a new partition is created with the current ordering. The
171  partition created for the new network read in is always freed at the end.<p>
172
173  Command options:<p>
174
175  <dl>
176
177  <dt> -b
178  <dd> Specifies that the files are BLIF files and not BLIF-MV files.
179  <p>
180
181  <dt> -f &lt;filename&gt;
182  <dd> Provides the correspondence between the leaves and roots of
183  network1 and network2. If this option is not used, it is assumed
184  that the correspondence is by name, except that two latch inputs
185  match if either they have the same name or the corresponding latch
186  outputs have the same name.  Leaves are the combinational inputs,
187  and roots are the combinational outputs.  <p>
188
189  <dt> -h
190  <dd> Print the command usage.
191  <p>
192
193  <dt> -t &lt;timeOut&gt;
194  <dd> Time in seconds allowed to perform equivalence checking.  The default
195  is infinity.<p>
196
197  <dt> -o &lt;ordering method&gt;
198  <dd> Specifies the ordering method to be used for assigning a common
199  ordering to the leaves of network1 and network2. If this option is not used,
200  ordering is done using a default method.  Currently, only the default method
201  is available. <p>
202
203  <dt> -1 &lt;partition method&gt;
204
205  <dd> Specifies the partitioning method to be used for network1. Supported
206  methods are "total", "partial", and "inout" (see the command
207  <code>build_partition_mdds</code> for more information). If this option is
208  not specified, then the default method "inout" is used.  <p>
209
210  <dt> -2 &lt;partition method&gt;
211  <dd> Specifies the partitioning method to be used for network2. Supported
212  methods are "total", "partial", and "inout" (see the command
213  <code>build_partition_mdds</code> for more information). If this option is
214  not specified, then default method "inout" is used.  <p>
215
216  <dt> -i
217  <dd> Print Bdd statistics.
218
219  </dl>
220  ]
221
222******************************************************************************/
223
224static int
225CommandCombEquivalence(
226  Hrc_Manager_t **hmgr,
227  int argc,
228  char **argv)
229{
230  static int                   timeOutPeriod;
231  static Hrc_Manager_t        *hmgr1;
232  static Hrc_Manager_t        *hmgr2;
233  static Ntk_Network_t        *network1;
234  static Ntk_Network_t        *network2;
235  int                          c;
236  int                          check;
237  FILE                        *fp;
238  FILE                        *inputFile = NIL(FILE);
239  char                        *fileName1;
240  char                        *fileName2;
241  char                        *name1;
242  char                        *name2;
243  st_generator                *gen;
244  static Part_PartitionMethod  partMethod1;
245  static Part_PartitionMethod  partMethod2;
246  static OFT                   AssignCommonOrder;
247  static st_table             *inputMap;
248  static st_table             *outputMap;
249  st_table                    *rootsTable = NIL(st_table);
250  st_table                    *leavesTable = NIL(st_table);
251  boolean                      fileFlag = FALSE;
252  boolean                      equivalent;
253  boolean                      printBddInfo = FALSE;
254  static boolean               execMode; /* FALSE: verify against current network,
255                                            TRUE:  verify the two given networks */
256  boolean isBlif = FALSE;
257
258  /*
259   * These are the default values.  These variables must be declared static
260   * to avoid lint warnings.  Since they are static, we must reinitialize
261   * them outside of the variable declarations.
262   */
263  timeOutPeriod     = 0;
264  hmgr1             = NIL(Hrc_Manager_t);
265  hmgr2             = NIL(Hrc_Manager_t);
266  partMethod1       = Part_Default_c;
267  partMethod2       = Part_Default_c;
268  AssignCommonOrder = DefaultCommonOrder;
269  inputMap          = NIL(st_table);
270  outputMap         = NIL(st_table);
271
272  error_init();
273  util_getopt_reset();
274  while((c = util_getopt(argc, argv, "bf:o:1:2:ht:i")) != EOF) {
275    switch(c) {
276      case 'b':
277        isBlif = TRUE;
278        break;
279      case 'f':
280        if((inputFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 1)) ==
281           NIL(FILE)) {
282          (void) fprintf(vis_stderr, "** eqv error: File %s not found.\n", util_optarg);
283          goto usage;
284        }
285        fileFlag = 1;
286        break;
287      case 'o':
288        /* The following line causes a seg fault, because
289           FindOrderingMethod() always returns NULL, and currently
290           only DefaultCommonOrder is used.
291        AssignCommonOrder = FindOrderingMethod();
292        */
293        /* The programmer supplies and modifies this function if any new
294           ordering method is introduced. FindOrderingMethod() should return
295           the type OFT. */
296        break;
297      case 't':
298        timeOutPeriod = atoi(util_optarg);
299        break;
300      case '1':
301        if(!strcmp(util_optarg, "total")) {
302          partMethod1 =  Part_Total_c;
303        }
304        else
305          if(!strcmp(util_optarg, "partial")) {
306          partMethod1 =  Part_Partial_c;
307          }
308        else
309          if(!strcmp(util_optarg, "inout")) {
310            partMethod1 = Part_InOut_c;
311          }
312          else {
313            (void) fprintf(vis_stderr, "** eqv error: Unknown partition method 1\n");
314            goto usage;
315          }
316        break;
317      case '2':
318        if(!strcmp(util_optarg, "total")) {
319          partMethod2 =  Part_Total_c;
320        }
321        else
322          if(!strcmp(util_optarg, "partial")) {
323          partMethod2 =  Part_Partial_c;
324          }
325        else
326          if(!strcmp(util_optarg, "inout")) {
327            partMethod2 = Part_InOut_c;
328          }
329          else {
330            (void) fprintf(vis_stderr, "** eqv error: Unknown partition method 2\n");
331            goto usage;
332          }
333        break;
334      case 'i':
335        printBddInfo = TRUE;
336        break;
337      case 'h':
338        goto usage;
339      default :
340        goto usage;
341    }
342  }
343  if(argc == 1) {
344    goto usage;
345  }
346
347  if(argc == util_optind+1) {
348    execMode = FALSE;
349  }
350  else
351    if(argc == util_optind+2) {
352      execMode = TRUE;
353    }
354    else {
355      error_append("** eqv error: Improper number of arguments.\n");
356      (void) fprintf(vis_stderr, "%s", error_string());
357      goto usage;
358    }
359  if(execMode == FALSE) {
360    hmgr1 = *hmgr;
361    if(Hrc_ManagerReadCurrentNode(hmgr1) == NIL(Hrc_Node_t)) {
362      (void) fprintf(vis_stderr, "** eqv error: The hierarchy manager is empty.  Read in design.\n");
363      return 1;
364    }
365    network1 = (Ntk_Network_t *) Hrc_NodeReadApplInfo(
366                    Hrc_ManagerReadCurrentNode(hmgr1), NTK_HRC_NODE_APPL_KEY);
367    if(network1 == NIL(Ntk_Network_t)) {
368      (void) fprintf(vis_stderr, "** eqv error: There is no network. Use flatten_hierarchy.\n");
369      return 1;
370    }
371    if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) == NIL(void)) {
372      (void) fprintf(vis_stderr, "** eqv error: Network has not been partitioned. Use build_partition_mdds.\n");
373      return 1;
374    }
375    fileName2 = argv[util_optind];
376    if(isBlif) {
377      if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) {
378        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
379        goto usage;
380      }
381    }
382    else {
383      if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) {
384        (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2);
385        return 1;
386      }
387      hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
388      fclose(fp);
389      if(hmgr2 == NIL(Hrc_Manager_t)) {
390        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
391        return 1;
392      }
393    }
394    network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2),
395                                           TRUE, (lsList) NULL);
396    if(network2 == NIL(Ntk_Network_t)) {
397      Hrc_ManagerFree(hmgr2);
398      (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n");
399      return 1;
400    }
401
402  }
403  else {
404    fileName1 = argv[util_optind];
405    fileName2 = argv[util_optind+1];
406    if(isBlif) {
407      if((hmgr1 = Io_BlifRead(fileName1, FALSE)) == NIL(Hrc_Manager_t)) {
408        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1);
409        return 1;
410      }
411      if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) {
412        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
413        if(hmgr1) {
414          Hrc_ManagerFree(hmgr1);
415        }
416        return 1;
417      }
418    }
419    else {
420      if((fp = Cmd_FileOpen(fileName1, "r", NIL(char *), 1)) == NIL(FILE)) {
421        (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName1);
422        return 1;
423      }
424      hmgr1 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
425      fclose(fp);
426      if(hmgr1 == NIL(Hrc_Manager_t)) {
427        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1);
428        goto usage;
429      }
430      if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) {
431        (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2);
432        if(hmgr1) {
433          Hrc_ManagerFree(hmgr1);
434        }
435        return 1;
436      }
437      hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
438      fclose(fp);
439      if(hmgr2 == NIL(Hrc_Manager_t)) {
440        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
441        if(hmgr1) {
442          Hrc_ManagerFree(hmgr1);
443        }
444        return 1;
445      }
446    }
447    network1 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr1),
448                                           TRUE, (lsList) NULL);
449    network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2),
450                                           TRUE, (lsList) NULL);
451
452    if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) {
453      if(network1 == NIL(Ntk_Network_t)) {
454        (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n");
455      }
456      if(network2 == NIL(Ntk_Network_t)) {
457        (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n");
458      }
459      Hrc_ManagerFree(hmgr1);
460      Hrc_ManagerFree(hmgr2);
461      return 1;
462    }
463    if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) {
464      if(network1 == NIL(Ntk_Network_t)) {
465        (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n");
466      }
467      if(network2 == NIL(Ntk_Network_t)) {
468        (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n");
469      }
470      Hrc_ManagerFree(hmgr1);
471      Hrc_ManagerFree(hmgr2);
472      return 1;
473    }
474  }
475
476  if(Ntk_NetworkReadNumCombInputs(network1) !=
477     Ntk_NetworkReadNumCombInputs(network2)) {
478    error_append("** eqv error: Different number of inputs in the two networks.\n");
479    if(!fileFlag) {
480      if(execMode) {
481        Hrc_ManagerFree(hmgr1);
482        Ntk_NetworkFree(network1);
483      }
484      Hrc_ManagerFree(hmgr2);
485      Ntk_NetworkFree(network2);
486      (void) fprintf(vis_stderr, "%s", error_string());
487      return 1;
488    }
489  }
490
491  if(fileFlag) {
492    rootsTable = st_init_table(strcmp, st_strhash);
493    leavesTable = st_init_table(strcmp, st_strhash);
494    check = ReadRootLeafMap(inputFile, rootsTable, leavesTable);
495    fclose(inputFile);
496    switch (check) {
497      case 0 : /* error */
498        st_free_table(rootsTable);
499        st_free_table(leavesTable);
500        (void) fprintf(vis_stderr, "** eqv error: No data in the input file.\n");
501        if(execMode) {
502          Hrc_ManagerFree(hmgr1);
503          Ntk_NetworkFree(network1);
504        }
505        Hrc_ManagerFree(hmgr2);
506        Ntk_NetworkFree(network2);
507        return 1;
508    case 1 : /* leaves only */
509        st_free_table(rootsTable);
510        inputMap = MapNamesToNodes(network1, network2, leavesTable);
511        st_foreach_item(leavesTable, gen, &name1, &name2) {
512          FREE(name1);
513          FREE(name2);
514        }
515        st_free_table(leavesTable);
516        if(inputMap == NIL(st_table)) {
517          (void) fprintf(vis_stderr, "%s", error_string());
518          if(execMode) {
519            Hrc_ManagerFree(hmgr1);
520            Ntk_NetworkFree(network1);
521          }
522          Hrc_ManagerFree(hmgr2);
523          Ntk_NetworkFree(network2);
524          return 1;
525        }
526        if((outputMap = MapCombOutputsByName(network1, network2)) ==
527           NIL(st_table)) {
528          st_free_table(inputMap);
529          if(execMode) {
530            Hrc_ManagerFree(hmgr1);
531            Ntk_NetworkFree(network1);
532          }
533          Hrc_ManagerFree(hmgr2);
534          Ntk_NetworkFree(network2);
535          (void) fprintf(vis_stderr, "%s", error_string());
536          return 1;
537        }
538        if(!TestRootsAndLeavesAreValid(network1, network2, inputMap,
539                                       outputMap)){
540          st_free_table(inputMap);
541          st_free_table(outputMap);
542          if(execMode) {
543            Hrc_ManagerFree(hmgr1);
544            Ntk_NetworkFree(network1);
545          }
546          Hrc_ManagerFree(hmgr2);
547          Ntk_NetworkFree(network2);
548          (void) fprintf(vis_stderr, "%s", error_string());
549          return 1;
550        }
551        break;
552    case 2 : /* roots only */
553        st_free_table(leavesTable);
554        outputMap = MapNamesToNodes(network1, network2, rootsTable);
555        st_foreach_item(rootsTable, gen, &name1, &name2) {
556          FREE(name1);
557          FREE(name2);
558        }
559        st_free_table(rootsTable);
560        if(outputMap ==NIL(st_table)) {
561          (void) fprintf(vis_stderr, "%s", error_string());
562          if(execMode) {
563            Hrc_ManagerFree(hmgr1);
564            Ntk_NetworkFree(network1);
565          }
566          Hrc_ManagerFree(hmgr2);
567          Ntk_NetworkFree(network2);
568          return 1;
569        }
570        if((inputMap = MapCombInputsByName(network1, network2)) ==
571           NIL(st_table)) {
572          st_free_table(outputMap);
573          if(execMode) {
574            Hrc_ManagerFree(hmgr1);
575            Ntk_NetworkFree(network1);
576          }
577          Hrc_ManagerFree(hmgr2);
578          Ntk_NetworkFree(network2);
579          (void) fprintf(vis_stderr, "%s", error_string());
580          return 1;
581        }
582        if(!TestRootsAndLeavesAreValid(network1, network2, inputMap,
583                                       outputMap)){
584          st_free_table(inputMap);
585          st_free_table(outputMap);
586          if(execMode) {
587            Hrc_ManagerFree(hmgr1);
588            Ntk_NetworkFree(network1);
589          }
590          Hrc_ManagerFree(hmgr2);
591          Ntk_NetworkFree(network2);
592          return 1;
593        }
594        break;
595    case 3 : /* both leaves and roots */
596        inputMap = MapNamesToNodes(network1, network2, leavesTable);
597        st_foreach_item(leavesTable, gen, &name1, &name2) {
598          FREE(name1);
599          FREE(name2);
600        }
601        st_free_table(leavesTable);
602        outputMap = MapNamesToNodes(network1, network2, rootsTable);
603        st_foreach_item(rootsTable, gen, &name1, &name2) {
604          FREE(name1);
605          FREE(name2);
606        }
607        st_free_table(rootsTable);
608        if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) {
609          (void) fprintf(vis_stderr, "%s", error_string());
610          if(inputMap) {
611            st_free_table(inputMap);
612          }
613          if(outputMap) {
614            st_free_table(outputMap);
615          }
616          if(execMode) {
617            Hrc_ManagerFree(hmgr1);
618            Ntk_NetworkFree(network1);
619          }
620          Hrc_ManagerFree(hmgr2);
621          Ntk_NetworkFree(network2);
622          return 1;
623        }
624        if(!TestRootsAndLeavesAreValid(network1, network2, inputMap,
625                                       outputMap)){
626          st_free_table(inputMap);
627          st_free_table(outputMap);
628          if(execMode) {
629            Hrc_ManagerFree(hmgr1);
630            Ntk_NetworkFree(network1);
631          }
632          Hrc_ManagerFree(hmgr2);
633          Ntk_NetworkFree(network2);
634          (void) fprintf(vis_stderr, "%s", error_string());
635          return 1;
636        }
637        break;
638    }
639  }
640  else {
641    inputMap = MapCombInputsByName(network1, network2);
642    outputMap = MapCombOutputsByName(network1, network2);
643    if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) {
644      if(inputMap) {
645        st_free_table(inputMap);
646      }
647      if(outputMap) {
648        st_free_table(outputMap);
649      }
650      if(execMode) {
651        Hrc_ManagerFree(hmgr1);
652        Ntk_NetworkFree(network1);
653      }
654      Hrc_ManagerFree(hmgr2);
655      Ntk_NetworkFree(network2);
656      (void) fprintf(vis_stderr, "%s", error_string());
657      return 1;
658    }
659  }
660
661  /* Start the timer before calling the equivalence checker. */
662  if (timeOutPeriod > 0){
663    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
664    (void) alarm(timeOutPeriod);
665    if (setjmp(timeOutEnv) > 0) {
666      (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod);
667      alarm(0);
668      return 1;
669    }
670  }
671
672  equivalent = Eqv_NetworkVerifyCombinationalEquivalence(network1, network2,
673                                                         inputMap, outputMap,
674                                                         AssignCommonOrder,
675                                                         partMethod1,
676                                                         partMethod2);
677
678  if(equivalent) {
679    (void) fprintf(vis_stdout, "Networks are combinationally equivalent.\n\n");
680  }
681  else {
682    (void) fprintf(vis_stdout, "%s", error_string());
683    (void) fprintf(vis_stdout, "Networks are NOT combinationally equivalent.\n\n");
684  }
685
686  if (printBddInfo) {
687    bdd_print_stats(Ntk_NetworkReadMddManager(network1), vis_stdout);
688  }
689
690  st_free_table(inputMap);
691  st_free_table(outputMap);
692  if(execMode) {
693    Hrc_ManagerFree(hmgr1);
694    Ntk_NetworkFree(network1);
695  }
696  Hrc_ManagerFree(hmgr2);
697  Ntk_NetworkFree(network2);
698
699  alarm(0);
700  return 0; /* normal exit */
701
702  usage:
703  (void) fprintf(vis_stderr, "usage: comb_verify [-b] [-f filename] [-h] [-o ordering method] [-t time]\n");
704  (void) fprintf(vis_stderr, "                   [-1 partMethod1] [-2 partMethod2] [-i] file1 [file2]\n");
705  (void) fprintf(vis_stderr, "   -b        input files are BLIF\n");
706  (void) fprintf(vis_stderr, "   -f file   variable name correspondence file\n");
707  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
708  (void) fprintf(vis_stderr, "   -o method variable ordering method\n");
709  (void) fprintf(vis_stderr, "   -t time   time out period (in seconds)\n");
710  (void) fprintf(vis_stderr, "   -1 method partitioning method for network1\n");
711  (void) fprintf(vis_stderr, "   -2 method partitioning method for network2\n");
712  (void) fprintf(vis_stderr, "   -i        print Bdd statistics\n");
713  return 1;             /* error exit */
714}
715
716/**Function********************************************************************
717
718  Synopsis [This function sits between the command line and the main routine
719  of sequential verification.]
720
721  Description [The function parses the command line.]
722
723  SideEffects []
724
725  SeeAlso [Eqv_NetworkVerifySequentialEquivalence]
726
727  CommandName [seq_verify]
728
729  CommandSynopsis [verify the sequential equivalence of two flattened networks]
730
731  CommandArguments [\[-b\] \[-f &lt;filename&gt;\] \[-h\] \[-p &lt;partition
732  method&gt;\] \[-t &lt;timeOut&gt;\] \[-B\] \[-i\] \[-r\] &lt;filename&gt; \[&lt;filename&gt;\]]
733
734  CommandDescription [Please read the documentation for the command
735  <code>comb_verify</code> before reading on. The concepts of roots and leaves
736  in this command are the same as for <code>comb_verify</code>, except for an
737  added constraint: the set of leaves has to be the set of all primary inputs.
738  This obviously produces the constraint that both networks have the
739  same number of primary inputs. Moreover, no pseudo inputs should be present
740  in the two networks being compared. The set of roots can be an arbitrary
741  subset of nodes.<p>
742
743  The command verifies whether any state, where the values of two
744  corresponding roots differ, can be reached from the set of
745  initial states of the product machine. If this happens, a debug trace is
746  provided.<p>
747
748  The sequential verification is done by building the product finite state
749  machine.<p>
750
751  The command has two execution modes, just as for <code>comb_verify</code>.
752  In the first mode, two BLIF-MV files are given as arguments to the
753  command:<p>
754
755  <pre>
756  vis> seq_verify foo.mv bar.mv
757  </pre>
758
759  In the second mode, a single BLIF-MV file is taken. This is network2. It is
760  assumed that network1 is from a hierarchy that has already been read in. If
761  a network is present at the current node (i.e. flatten_hierarchy has been
762  executed), it is used for verification; otherwise the command does
763  nothing.<p>
764
765  <pre>
766  vis> read_blifmv foo.mv
767  vis> flatten_hierarchy
768  vis> seq_verify bar.mv
769  </pre>
770
771  Command options:<p>
772
773  <dl>
774
775  <dt> -b
776  <dd> Specifies that the input files are BLIF files.
777  <p>
778
779  <dt> -f &lt;filename&gt;
780  <dd> Provides the correspondence between the leaves and roots of network1
781  and network2. leaves has to be the set of primary inputs of the
782  networks. roots can be any subset of nodes. If this option is not used, it
783  is assumed that the correspondence is by name, and that the roots are the
784  combinational outputs.  <p>
785
786  <dt> -h
787  <dd> Print the command usage.
788  <p>
789
790  <dt> -p &lt;partition method&gt;
791  <dd> Specifies the partitioning method for the product machine. Supported
792  methods are "total", "partial", and "inout" (see the command
793  <code>build_partition_mdds</code> for more information). If this option is
794  not specified, then the default method "inout" is used.
795  <p>
796
797  <dt> -t &lt;timeOut&gt;
798  <dd> Time in seconds allowed to perform equivalence checking.  The default
799  is infinity.<p>
800
801  <dt> -B
802  <dd> Use backward image computation to traverse the state space of
803  the product machine.  By default, forward image computaion is used.
804
805  <dt> -i
806  <dd> Print BDD statistics. This is the only way to see BDD stastics during
807  this command. print_bdd_stats after this command doesn't show information
808  related to this command.
809
810  <dt> -r
811  <dd> Enable BDD reordering during the equivalence check.  Note that
812  dynamic_var_ordering has no effect on whether reordering is enabled during
813  the execution of seq_verify.
814  </dl>
815
816  ]
817
818******************************************************************************/
819static int
820CommandSeqEquivalence(
821  Hrc_Manager_t **hmgr,
822  int argc,
823  char **argv)
824{
825  static int            timeOutPeriod;
826  static Hrc_Manager_t *hmgr1;
827  static Hrc_Manager_t *hmgr2;
828  static Ntk_Network_t *network1;
829  static Ntk_Network_t *network2;
830  int                   c;
831  int                   check;
832  FILE                 *fp;
833  static FILE          *inputFile;
834  char                 *fileName1;
835  char                 *fileName2;
836  char                 *name1;
837  char                 *name2;
838  st_generator         *gen;
839  static Part_PartitionMethod partMethod;
840  st_table             *outputMap = NIL(st_table);
841  st_table             *inputMap = NIL(st_table);
842  st_table             *rootsTable = NIL(st_table);
843  st_table             *leavesTable = NIL(st_table);
844  static boolean        fileFlag;
845  static boolean        execMode; /* FALSE: verify against the current network,
846                                     TRUE:  verify the two networks */
847  static boolean        equivalent;
848  boolean               isBlif = FALSE;
849  boolean               printBddInfo = FALSE;
850  static boolean        useBackwardReach;
851  boolean               reordering = FALSE;
852
853  /*
854   * These are the default values.  These variables must be declared static
855   * to avoid lint warnings.  Since they are static, we must reinitialize
856   * them outside of the variable declarations.
857   */
858  timeOutPeriod    = 0;
859  hmgr1            = NIL(Hrc_Manager_t);
860  hmgr2            = NIL(Hrc_Manager_t);
861  inputFile        = NIL(FILE);
862  partMethod       = Part_Default_c;
863  fileFlag         = FALSE;
864  equivalent       = FALSE;
865  useBackwardReach = FALSE;
866
867  error_init();
868  util_getopt_reset();
869  while((c = util_getopt(argc, argv, "bBf:p:hFt:ir")) != EOF) {
870    switch(c) {
871    case 'b':
872      isBlif = TRUE;
873      break;
874    case 'f':
875      if((inputFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 1)) ==
876         NIL(FILE)) {
877        (void) fprintf(vis_stderr,
878                       "** eqv error: File %s not found.\n", util_optarg);
879        return 1;
880      }
881      fileFlag = 1;
882      break;
883    case 'p':
884      if(!strcmp(util_optarg, "total")) {
885        partMethod =  Part_Total_c;
886      } else {
887        if(!strcmp(util_optarg, "partial")) {
888          partMethod =  Part_Partial_c;
889        } else {
890          if(!strcmp(util_optarg, "inout")) {
891            partMethod = Part_InOut_c;
892          } else {
893            (void) fprintf(vis_stderr,
894                           "** eqv error: Unknown partition method\n");
895            goto usage;
896          }
897        }
898      }
899      break;
900    case 't':
901      timeOutPeriod = atoi(util_optarg);
902      break;
903    case 'B':
904      useBackwardReach = TRUE;
905      break;
906    case 'h':
907      goto usage;
908    case 'i':
909      printBddInfo = TRUE;
910      break;
911    case 'r':
912      reordering = TRUE;
913      break;
914    default:
915      goto usage;
916    }
917  }
918  if(argc == 1) {
919    goto usage;
920  }
921  if(argc == util_optind+1) {
922    execMode = FALSE;
923  }
924  else
925    if(argc == util_optind+2) {
926      execMode = TRUE;
927    }
928    else {
929      error_append("** eqv error: Improper number of arguments.\n");
930      (void) fprintf(vis_stderr, "%s", error_string());
931      goto usage;
932    }
933  if(execMode == FALSE) {
934    hmgr1 = *hmgr;
935    if(Hrc_ManagerReadCurrentNode(hmgr1) == NIL(Hrc_Node_t)) {
936      (void) fprintf(vis_stderr, "** eqv error: The hierarchy manager is empty.  Read in design.\n");
937      return 1;
938    }
939    network1 = (Ntk_Network_t *) Hrc_NodeReadApplInfo(
940                    Hrc_ManagerReadCurrentNode(hmgr1), NTK_HRC_NODE_APPL_KEY);
941    if(network1 == NIL(Ntk_Network_t)) {
942      (void) fprintf(vis_stderr, "** eqv error: There is no network. Use flatten_hierarchy.\n");
943      return 1;
944    }
945    if(!Ntk_NetworkReadNumLatches(network1)) {
946      (void) fprintf(vis_stderr, "** eqv error: No latches present in the current network. Use comb_verify.\n");
947      return 1;
948    }
949    fileName2 = argv[util_optind];
950    if(isBlif) {
951      if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) {
952        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
953        goto usage;
954      }
955    }
956    else {
957      if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) {
958        (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2);
959        return 1;
960      }
961      hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
962      fclose(fp);
963      if(hmgr2 == NIL(Hrc_Manager_t)) {
964        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
965        return 1;
966      }
967    }
968    network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2),
969                                           TRUE, (lsList) NULL);
970    if(network2 == NIL(Ntk_Network_t)) {
971      Hrc_ManagerFree(hmgr2);
972      (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n");
973      return 1;
974    }
975    if(!Ntk_NetworkReadNumLatches(network2)) {
976      (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName2);
977      Hrc_ManagerFree(hmgr2);
978      Ntk_NetworkFree(network2);
979      return 1;
980    }
981  }
982  else {
983    fileName1 = argv[util_optind];
984    fileName2 = argv[util_optind+1];
985    if(isBlif) {
986      if((hmgr1 = Io_BlifRead(fileName1, FALSE)) == NIL(Hrc_Manager_t)) {
987        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1);
988        return 1;
989      }
990      if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) {
991        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
992        if(hmgr1) {
993          Hrc_ManagerFree(hmgr1);
994        }
995        return 1;
996      }
997    }
998    else {
999      if((fp = Cmd_FileOpen(fileName1, "r", NIL(char *), 1)) == NIL(FILE)) {
1000        (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName1);
1001        return 1;
1002      }
1003      hmgr1 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
1004      fclose(fp);
1005      if(hmgr1 == NIL(Hrc_Manager_t)) {
1006        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1);
1007        goto usage;
1008      }
1009      if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) {
1010        (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2);
1011        if(hmgr1) {
1012          Hrc_ManagerFree(hmgr1);
1013        }
1014        return 1;
1015      }
1016      hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
1017      fclose(fp);
1018      if(hmgr2 == NIL(Hrc_Manager_t)) {
1019        (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2);
1020        if(hmgr1) {
1021          Hrc_ManagerFree(hmgr1);
1022        }
1023        return 1;
1024      }
1025    }
1026    network1 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr1),
1027                                           TRUE, (lsList) NULL);
1028    network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2),
1029                                           TRUE, (lsList) NULL);
1030    if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) {
1031      if(network1 == NIL(Ntk_Network_t)) {
1032        (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n");
1033      }
1034      if(network2 == NIL(Ntk_Network_t)) {
1035        (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n");
1036      }
1037      Hrc_ManagerFree(hmgr1);
1038      Hrc_ManagerFree(hmgr2);
1039      return 1;
1040    }
1041
1042    if(!Ntk_NetworkReadNumLatches(network1)) {
1043      (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName1);
1044      Hrc_ManagerFree(hmgr1);
1045      Ntk_NetworkFree(network1);
1046      Hrc_ManagerFree(hmgr2);
1047      Ntk_NetworkFree(network2);
1048      return 1;
1049    }
1050    if(!Ntk_NetworkReadNumLatches(network2)) {
1051      (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName2);
1052      Hrc_ManagerFree(hmgr1);
1053      Ntk_NetworkFree(network1);
1054      Hrc_ManagerFree(hmgr2);
1055      Ntk_NetworkFree(network2);
1056      return 1;
1057    }
1058  }
1059  if(Ntk_NetworkReadNumPrimaryInputs(network1) !=
1060     Ntk_NetworkReadNumInputs(network1)) {
1061    error_append("** eqv error: Pseudo inputs present in network1. Unable to do verification.\n");
1062    (void) fprintf(vis_stderr, "%s", error_string());
1063    if(execMode) {
1064      Hrc_ManagerFree(hmgr1);
1065      Ntk_NetworkFree(network1);
1066    }
1067    Hrc_ManagerFree(hmgr2);
1068    Ntk_NetworkFree(network2);
1069    return 1;
1070  }
1071  if(Ntk_NetworkReadNumPrimaryInputs(network2) !=
1072     Ntk_NetworkReadNumInputs(network2)) {
1073    error_append("** eqv error: Pseudo inputs present in network2. Unable to do verification.\n");
1074    (void) fprintf(vis_stderr, "%s", error_string());
1075    if(execMode) {
1076      Hrc_ManagerFree(hmgr1);
1077      Ntk_NetworkFree(network1);
1078    }
1079    Hrc_ManagerFree(hmgr2);
1080    Ntk_NetworkFree(network2);
1081    return 1;
1082  }
1083  if(Ntk_NetworkReadNumPrimaryInputs(network1) !=
1084     Ntk_NetworkReadNumPrimaryInputs(network2)) {
1085    error_append("** eqv error: Different number of inputs in the two networks.\n");
1086    (void) fprintf(vis_stderr, "%s", error_string());
1087    if(execMode) {
1088      Hrc_ManagerFree(hmgr1);
1089      Ntk_NetworkFree(network1);
1090    }
1091    Hrc_ManagerFree(hmgr2);
1092    Ntk_NetworkFree(network2);
1093    return 1;
1094  }
1095
1096  /* Start the timer before calling the equivalence checker. */
1097  if (timeOutPeriod > 0){
1098    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
1099    (void) alarm(timeOutPeriod);
1100    if (setjmp(timeOutEnv) > 0) {
1101      (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n",
1102                     timeOutPeriod);
1103      alarm(0);
1104      return 1;
1105    }
1106  }
1107
1108  if(fileFlag) {
1109    rootsTable = st_init_table(strcmp, st_strhash);
1110    leavesTable = st_init_table(strcmp, st_strhash);
1111    check = ReadRootLeafMap(inputFile, rootsTable, leavesTable);
1112    fclose(inputFile);
1113    if(check == 0) {
1114      st_free_table(rootsTable);
1115      st_free_table(leavesTable);
1116      (void) fprintf(vis_stderr, "** eqv error: No data in the input file\n");
1117      alarm(0);
1118      return 1;
1119    }
1120    switch (check) {
1121    case 1 :
1122      st_free_table(rootsTable);
1123      outputMap = MapPrimaryOutputsByName(network1, network2);
1124      if((outputMap == NIL(st_table)) || !TestLeavesAreValid(network1,
1125                                                             network2,
1126                                                             leavesTable)) {
1127        st_foreach_item(leavesTable, gen, &name1, &name2) {
1128          FREE(name1);
1129          FREE(name2);
1130        }
1131        st_free_table(leavesTable);
1132        if(outputMap) {
1133          st_free_table(outputMap);
1134        }
1135        (void) fprintf(vis_stderr, "%s", error_string());
1136        if(execMode) {
1137          Hrc_ManagerFree(hmgr1);
1138          Ntk_NetworkFree(network1);
1139        }
1140        Hrc_ManagerFree(hmgr2);
1141        Ntk_NetworkFree(network2);
1142        (void) fprintf(vis_stderr, "%s", error_string());
1143        alarm(0);
1144        return 1;
1145      }
1146      equivalent = Eqv_NetworkVerifySequentialEquivalence(network1,
1147                                                          network2,
1148                                                          NIL(st_table),
1149                                                          leavesTable,
1150                                                          partMethod,
1151                                                          useBackwardReach,
1152                                                          reordering);
1153      st_foreach_item(leavesTable, gen, &name1, &name2) {
1154        FREE(name1);
1155        FREE(name2);
1156      }
1157      st_free_table(leavesTable);
1158      break;
1159    case 2 :
1160      st_free_table(leavesTable);
1161      inputMap = MapPrimaryInputsByName(network1, network2);
1162
1163      if((inputMap == NIL(st_table)) || !TestRootsAreValid(network1,
1164                                                           network2,
1165                                                           rootsTable)) {
1166        st_foreach_item(rootsTable, gen, &name1, &name2) {
1167          FREE(name1);
1168          FREE(name2);
1169        }
1170        st_free_table(rootsTable);
1171        if(inputMap) {
1172          st_free_table(inputMap);
1173        }
1174        (void) fprintf(vis_stderr, "%s", error_string());
1175        if(execMode) {
1176          Hrc_ManagerFree(hmgr1);
1177          Ntk_NetworkFree(network1);
1178        }
1179        Hrc_ManagerFree(hmgr2);
1180        Ntk_NetworkFree(network2);
1181        alarm(0);
1182        return 1;
1183      }
1184      equivalent = Eqv_NetworkVerifySequentialEquivalence(network1,
1185                                                          network2,
1186                                                          rootsTable,
1187                                                          NIL(st_table),
1188                                                          partMethod,
1189                                                          useBackwardReach,
1190                                                          reordering);
1191      st_foreach_item(rootsTable, gen, &name1, &name2) {
1192        FREE(name1);
1193        FREE(name2);
1194      }
1195      st_free_table(rootsTable);
1196      break;
1197    case 3 :
1198      if(TestRootsAreValid(network1, network2, rootsTable) &&
1199         TestLeavesAreValid(network1, network2, leavesTable)) {
1200        equivalent = Eqv_NetworkVerifySequentialEquivalence(network1,
1201                                                            network2,
1202                                                            rootsTable,
1203                                                            leavesTable,
1204                                                            partMethod,
1205                                                            useBackwardReach,
1206                                                            reordering);
1207        st_foreach_item(rootsTable, gen, &name1, &name2) {
1208          FREE(name1);
1209          FREE(name2);
1210        }
1211        st_free_table(rootsTable);
1212        st_foreach_item(leavesTable, gen, &name1, &name2) {
1213          FREE(name1);
1214          FREE(name2);
1215        }
1216        st_free_table(leavesTable);
1217      }
1218      else {
1219        if(execMode) {
1220          Hrc_ManagerFree(hmgr1);
1221          Ntk_NetworkFree(network1);
1222        }
1223        Hrc_ManagerFree(hmgr2);
1224        Ntk_NetworkFree(network2);
1225        st_foreach_item(rootsTable, gen, &name1, &name2) {
1226          FREE(name1);
1227          FREE(name2);
1228        }
1229        st_free_table(rootsTable);
1230        st_foreach_item(leavesTable, gen, &name1, &name2) {
1231          FREE(name1);
1232          FREE(name2);
1233        }
1234        st_free_table(leavesTable);
1235        (void) fprintf(vis_stderr, "%s", error_string());
1236        alarm(0);
1237        return 1;
1238      }
1239    }
1240  }
1241  else {
1242    outputMap = MapPrimaryOutputsByName(network1, network2);
1243    inputMap = MapPrimaryInputsByName(network1, network2);
1244    if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) {
1245      if(inputMap) {
1246        st_free_table(inputMap);
1247      }
1248      if(outputMap) {
1249        st_free_table(outputMap);
1250      }
1251      if(execMode) {
1252        Hrc_ManagerFree(hmgr1);
1253        Ntk_NetworkFree(network1);
1254      }
1255      Hrc_ManagerFree(hmgr2);
1256      Ntk_NetworkFree(network2);
1257      (void) fprintf(vis_stderr, "%s", error_string());
1258      alarm(0);
1259      return 1;    /* all primary outputs do not match */
1260    }
1261    st_free_table(inputMap);
1262    st_free_table(outputMap);
1263    equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, network2,
1264                                                        NIL(st_table),
1265                                                        NIL(st_table),
1266                                                        partMethod,
1267                                                        useBackwardReach,
1268                                                        reordering);
1269  }
1270  if(equivalent) {
1271    (void) fprintf(vis_stdout, "Networks are sequentially equivalent.\n\n");
1272  }
1273  else {
1274    (void) fprintf(vis_stdout,
1275                   "Networks are NOT sequentially equivalent.\n\n");
1276  }
1277
1278  if (printBddInfo) {
1279    bdd_print_stats(Ntk_NetworkReadMddManager(network2), vis_stdout);
1280  }
1281
1282  if(execMode) {
1283    Hrc_ManagerFree(hmgr1);
1284    Ntk_NetworkFree(network1);
1285  }
1286  Hrc_ManagerFree(hmgr2);
1287  Ntk_NetworkFree(network2);
1288
1289  alarm(0);
1290  return 0;  /* normal exit */
1291
1292  usage :
1293  (void) fprintf(vis_stderr, "usage: seq_verify [-b] [-f filename] [-h] [-p partition method] [-t time] [-B]\n\t\t  [-i] [-r] file1 [file2]\n");
1294  (void) fprintf(vis_stderr, "   -b        input files are BLIF\n");
1295  (void) fprintf(vis_stderr, "   -f file   variable name correspondence file\n");
1296  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
1297  (void) fprintf(vis_stderr, "   -p method partitioning method for product machine\n");
1298  (void) fprintf(vis_stderr, "   -t time   time out period (in seconds)\n");
1299  (void) fprintf(vis_stderr, "   -B        use backward image computation\n");
1300  (void) fprintf(vis_stderr, "   -i        print BDD statistics\n");
1301  (void) fprintf(vis_stderr, "   -r        enable BDD variable reordering\n");
1302  return 1;    /* error exit */
1303}
1304
1305/**Function********************************************************************
1306
1307  Synopsis    [Handle function for timeout.]
1308
1309  Description [This function is called when the time out occurs.]
1310
1311  SideEffects []
1312
1313******************************************************************************/
1314static void
1315TimeOutHandle(void)
1316{
1317  longjmp(timeOutEnv, 1);
1318}
Note: See TracBrowser for help on using the repository browser.