source: vis_dev/vis-2.3/src/res/resCmd.c @ 93

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

vis2.3
File size: 41.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [resCmd.c]
4
5  PackageName [res]
6
7  Synopsis [Implements the different commands related to the residue
8  verification.]
9
10  Description [This file provides the wrapper functions for the commands
11  involving the residue verification. The command res_verify receives at least
12  one file describing an implementation and optionally a second one describing
13  a specification of a circuit and a set of different options and calls the
14  procedure to perform residue verification in the two systems. For more
15  detailed information about the command res_verify, see also CommandResVerify]
16
17  Author      [Kavita Ravi    <ravi@duke.colorado.edu> and
18               Abelardo Pardo <abel@duke.colorado.edu>]
19               
20  Copyright [This file was created at the University of Colorado at Boulder.
21  The University of Colorado at Boulder makes no warranty about the suitability
22  of this software for any purpose.  It is presented on an AS IS basis.]
23
24******************************************************************************/
25
26#include "resInt.h"
27
28static char rcsid[] UNUSED = "$Id: resCmd.c,v 1.58 2010/04/10 00:38:26 fabio Exp $";
29
30/*---------------------------------------------------------------------------*/
31/* Constant declarations                                                     */
32/*---------------------------------------------------------------------------*/
33
34
35/*---------------------------------------------------------------------------*/
36/* Type declarations                                                         */
37/*---------------------------------------------------------------------------*/
38
39
40/*---------------------------------------------------------------------------*/
41/* Structure declarations                                                    */
42/*---------------------------------------------------------------------------*/
43
44
45/*---------------------------------------------------------------------------*/
46/* Variable declarations                                                     */
47/*---------------------------------------------------------------------------*/
48
49static jmp_buf timeOutEnv;
50
51/*---------------------------------------------------------------------------*/
52/* Macro declarations                                                        */
53/*---------------------------------------------------------------------------*/
54
55
56/**AutomaticStart*************************************************************/
57
58/*---------------------------------------------------------------------------*/
59/* Static function prototypes                                                */
60/*---------------------------------------------------------------------------*/
61
62static int CommandResVerify(Hrc_Manager_t ** hmgr, int argc, char ** argv);
63static void TimeOutHandle(void);
64static st_table * ReadMatchingPairs(char *fileName, Ntk_Network_t *ntk1, Ntk_Network_t *ntk2);
65static array_t * ReadOutputOrder(char *fileName, Ntk_Network_t *ntk1);
66static array_t * GenerateDefaultOutputOrder(Ntk_Network_t *specNetwork);
67static int CheckForMultiValueNode(Ntk_Network_t *network);
68
69/**AutomaticEnd***************************************************************/
70
71
72/*---------------------------------------------------------------------------*/
73/* Definition of exported functions                                          */
74/*---------------------------------------------------------------------------*/
75
76/**Function********************************************************************
77
78  Synopsis [Initializes the Residue Verification package.]
79
80  SideEffects []
81
82  SeeAlso     [Tst_End]
83
84******************************************************************************/
85void
86Res_Init(void)
87{
88  Cmd_CommandAdd("res_verify", CommandResVerify, /* doesn't changes_network */ 0);
89}
90
91
92/**Function********************************************************************
93
94  Synopsis [Ends the residue verification package.]
95
96  SideEffects []
97
98  SeeAlso     [Tst_Init]
99
100******************************************************************************/
101void
102Res_End(void)
103{
104  /*
105   * For example, free any global memory (if any) which the test package is
106   * responsible for.
107   */
108}
109
110/*---------------------------------------------------------------------------*/
111/* Definition of internal functions                                          */
112/*---------------------------------------------------------------------------*/
113
114
115/*---------------------------------------------------------------------------*/
116/* Definition of static functions                                            */
117/*---------------------------------------------------------------------------*/
118
119/**Function********************************************************************
120
121  Synopsis    [Implements the res_verify command.]
122
123  CommandName [res_verify]
124
125  CommandSynopsis [Verifies a combinational circuit using residue
126  arithmetic.]
127
128  CommandArguments [\[-b\] \[-d &lt;n&gt;\]
129  \[-h\] -i &lt;filename&gt; \[-m &lt;filename&gt;\] \[-n
130  &lt;filename&gt;\] {-o &lt;filename&gt; | -O} \[-s &lt;filename&gt;\] \[-t
131  &lt;timeOut&gt;\] ]
132 
133  CommandDescription [This command performs residue verification between two
134  networks. The method used is based on residue arithmetic and the Chinese
135  Remainder theorem; it is
136  described in [1\] ftp://vlsi.colorado.edu/pub/fmcad96.ps.
137  Verification is performed
138  by interpreting the outputs of the circuits  as integers
139  and verifying the residues of the outputs  with respect to a set of
140  moduli. The choice of moduli is directed  by the Chinese Remainder Theorem in order
141  to prove equivalence of the two circuits. This method works well with multipliers
142  and possibly other arithmetic circuits (due to its  dependence on residue
143  arithmetic).
144  For the same reason, it is necessary to specify an output order
145  which determines how the outputs are interpreted as integers.
146  Discretion should be exercised in applying this method to general combinational
147  circuits.
148
149  <p>
150  Residue verification is available only if vis is linked with the cu
151  BDD package. (This is the default.) It reads both
152  blif and blif-mv files. However, it does NOT support multi-valued
153  variables. Residue verification is primarily for combinational
154  verification, but may be applied to sequential circuits with the
155  same state encoding. The latch outputs are then considered to be combinational inputs of the
156  circuits and the latch inputs and reset are considered to be combinational
157  outputs of the circuits.
158 
159  <p>
160  There are two ways to perform residue verification in this package. As a first option, two
161  files describing two networks, the specification and the implementation, (in
162  the same format, blif or blif-mv, see option -b) are given in the command
163  line; the procedure
164  tries to verify the equivalence of the combinational outputs as functions of
165  the combinational inputs.
166
167  <p>
168
169  <code>
170  vis> res_verify -o network.order -i network1.blif -s network2.blif <br>
171  </code>
172
173  <p>
174
175  In this case both networks are read in, flattened and the verification is
176  performed between the combinational outputs of both networks. The <tt>-i</tt>
177  option denotes the implementation file and the <tt>-s</tt> option denotes
178  the specification file. The -o option specifies
179  the order of outputs for the circuits (See Command Options below for detailed
180  explanation).
181 
182
183  <p>
184  A second way to perform the verification is as follows. The specification
185  network is taken from a hierarchy  already read into VIS.  Then the <tt>res_verify </tt>
186  command compares that specification against an implementation network obtained from
187  the file in the command line. Any previous verification, performed with the
188  specification, can be used towards the
189  next verification task only if the same implementation circuit is being verified
190  against and the same number of outputs have been  directly verified with sucess
191  in the previous attempt. The typical sequence of commands given to perform such
192  task would be:
193
194  <p>
195  <code>
196  vis> read_blifmv network1.mv <br>
197  vis> flatten_hierarchy  <br>
198  vis> res_verify -o network.order -i network2.mv <br>
199  </code>
200
201  <p>
202 
203  If the hierarchy has been read but no flattened network exists at the current
204  node, the command will return without doing anything.
205
206  If one of the networks used is the one in the current node in the hierarchy,
207  then the information regarding the verification process will be stored in
208  that network.
209
210  <p>
211  <B> Note: </b>
212  It is important to keep the specification distinct from the implementation
213  because most  parameters specified for the <tt> res_verify </tt> command
214  are with respect to the specification. For example, the output order
215  is specified with respect to the specification.
216  The file that is read in first in the second format, is considered to be the specification.
217
218  <p>
219  There is an option to directly verify some outputs by building the
220  BDDs for the corresponding outputs of the 2 circuits. In that case,
221  if the user wants to use an initial ordering, the only way to do it is
222  the second method and reading in the network, one may specify the initial
223  order using static order.
224
225  <p>
226  The command does not repeat residue verification if the same
227  specification-implementation pair have been
228  verified with success and the same number of directly verified
229  outputs have been verified in the previous attempt.
230
231  <p>
232  <b> Relevant flags to be set using the set command: </b> <p>
233  <dl>
234  <dt> <b> residue_verbosity </b>
235  <dd> Default is 0, turns on verbosity to the desired level between 0 and 5.
236
237  <dt> <b> residue_ignore_direct_verified_outputs </b>
238  <dd> Default 0 (FALSE). If 1, then ignores directly verified outputs
239  during residue verification.
240
241  <dt> <b> residue_top_var </b>
242  <dd> Default "msb". The 2 possible values are "msb" and lsb"; this puts
243  the most/least significant bit near the top or bottom of the residue decision diagram.
244 
245  <dt> <b> residue_autodyn_residue_verif </b>
246  <dd> Default 0 (FALSE). If 1, turns on dynamic reordering during residue
247  verification.
248 
249  <dt> <b> residue_residue_dyn_method </b>
250  <dd> Default "groupsift". Specifies the method for dynamic reordering during
251  residue verification. Other methods supported are "same" (same as before),
252  "none", "random", "randompivot", "sift", "siftconverge", "symmsiftconverge",
253  "symmsift", "window2", "window3", "window4", "window2converge",
254  "window3converge", "window4converge", "groupsift", "groupsiftconverge",
255  "anneal", "genetic", "linear", "linearconverge", "exact".
256
257  <dt> <b> residue_autodyn_direct_verif </b>
258    <dd> Default 0 (FALSE). If 1, turns on dynamic reordering during direct
259  verification.
260 
261  <dt> <b> residue_direct_dyn_method </b>
262  <dd> Default "groupsift". Specifies the method for dynamic reordering during
263  direct verification. Other methods supported are "same" (same as before),
264  "none", "random", "randompivot", "sift", "siftconverge", "symmsiftconverge",
265  "symmsift", "window2", "window3", "window4", "window2converge",
266  "window3converge", "window4converge", "groupsift", "groupsiftconverge",
267  "anneal", "genetic", "linear", "linearconverge", "exact".
268 
269  <dt> <b> residue_layer_schedule </b>
270  <dd> Default "alap". This is a flag to specify the layering strategy of the
271  networks. The 2 options are "asap" (as soon as possible) and "alap" (as
272  late as possible).
273
274  <dt> <b> residue_layer_size </b>
275  <dd> Default largest layer size in network. Specifies the maximum layer
276  size  that can be composed in (relevant for vector composition only).
277 
278  <dt> <b> residue_composition_method </b>
279  <dd> Default "vector". Specifies the composition method to be used in
280  composing the network into the residue ADD. The options are "vector",
281  "onegate", "preimage" and "superG".
282  <p>
283  </dl>
284 
285  <b> Command Options: </b> <br>
286
287  <dl>
288
289  <dt> -b
290  <dd> If this option is specified, the specification and the implementation
291  files read  are considered to be in blif-mv format. Default is blif
292  format. <p>
293
294  <dt> -d n
295  <dd> This option specifies the number of outputs to be directly verified.
296  That is, for <tt> n </tt> least significant outputs of the circuit, this command
297  performs like comb_verify.
298  The actual outputs are read off the output order array.
299  Since the output order array is specified starting with the MSB, the number of
300  directly verified outputs will be a chunk of the bottom part of the output order array.
301  The option "-d all" sets the number of directly verified outputs to the
302  number of combinational outputs in the circuit i.e., all outputs are directly
303  verified.
304  The direct verification for small BDD sizes is faster and overall reduces
305  the number of primes to be used in residue verification. In general,
306  one output is checked at a time against the corresponding output of the
307  other network and consequently , this method may be fast and use less memory
308  resources.<br>
309  IMPORTANT: It is possible to specify an initial order for the direct
310  verification. This is done by reading in the specification file and using
311  static_order to specify the initial order. The implementation will get
312  the same order as the specification. When specifying the initial order,
313  one must be careful not to specify the -s option in the res_verify command.
314  The -s option reads in the specification file again and the initial order
315  is lost.  <p>
316 
317  <dt> -h
318  <dd> Print the command usage.<p>
319
320  <dt> -i &lt;filename&gt;
321  <dd> Implementation network to perform verification against. The file must be
322  in blif format unless <tt>-b</tt> is specified, in which case the file is
323  taken to be in blif-mv format. The blif format is the default.<p>
324
325  <dt> -m &lt;filename&gt;
326  <dd> Optional file name specifying the matching pair of output names between
327  the two networks. If not specified, it is assumed that all outputs have
328  identical names. This option is useful when verifying two circuits whose
329  output names do not match. The file will give pairs of the form <tt>name1
330  name2</tt> to be considered as corresponding  outputs in the verification
331  process. In each pair, <tt> name1 </tt> may belong to the specification
332  and <tt> name2 </tt> to the implementation or vice-versa. The matching
333  procedure is not capable of dealing with some
334  special situations. For example, when two outputs, one of each network have the same
335  name, they must correspond to the same output. Partial orders may not be specified. <p>
336
337  <dt> -n &lt;filename&gt;
338  <dd> Optional file name specifying the matching pair of input names between
339  the two networks. If not specified, it is assumed that all inputs have
340  identical names. This option is useful when verifying two circuits whose
341  input  names do not match. The file will give pairs of the form <tt>name1
342  name2</tt> to be considered as corresponding  inputs in the verification
343  process. In each pair, <tt> name1 </tt> may belong to the specification
344  and <tt> name2 </tt> to the implementation or vice-versa. The matching
345  procedure is not capable of dealing with some
346  special situations. For example, when two inputs, one of each network have the same
347  name, they must correspond to the same input. Partial orders may not be specified. <p>
348
349  <dt> -o &lt;filename&gt;
350  <dd> Required file  specifying output order, starting with the MSB.
351  The file must be a list of output names separated by spaces.
352  The list must belong to the specification network and must contain a
353  full order i.e., must contain all the combinational output names.  It is advisable to use
354  the -o option as far as possible to specify the order
355  of the outputs.See also -O option.<p>
356
357  <dt> -O
358  <dd> This option specifies whether the <code> res_verify </code> command should
359  generate a default
360  order for the outputs. If the -o option is not used, this option must be specified.
361  The default order generated is random and is NOT the same as the input files.
362  The set of outputs for the output order may be generated by using the print_network
363  command to write the network into a file and extract the node name from the  lines containing the word
364  "comb-output". The set of outputs can then be ordered as required.  <br>
365  It is advisable to use the -o option as far as possible to specify the order
366  of the outputs. The -o option overrides the -O option. See also -o option.<p>
367 
368  <dt> -s &lt;filename&gt;
369  <dd> Specification network. This network will be taken as the specification
370  of the circuit. The result of the computation will be stored in this network.
371  If this network is not provided, the current node of the
372  hierarchy will be taken. The file must contain a blif description of a
373  circuit unless the option <tt>-b</tt> is specified, in which case the file is
374  considered in blif-mv format. If two networks are specified in the
375  command line, both of them must have the same format, either blif or
376  blif-mv. The blif format is the default.<p>
377
378  <dt> -t &lt;timeOut &gt;
379
380  <dd> Execution time in seconds allowed for verification before aborting.  The
381  default is no limit.<p>
382
383  </dl>
384  ]
385
386  SideEffects [It registers the information about the verification in the
387  specification if this is the current node in the hierarchy manager.]
388
389  SeeAlso            [Res_NetworkResidueVerify]
390
391******************************************************************************/
392static int
393CommandResVerify(Hrc_Manager_t ** hmgr,
394                 int  argc,
395                 char ** argv)
396{
397  static int           timeOutPeriod; /* CPU seconds allowed */
398  static array_t       *outputOrderArray;   /* required to specify the outputs
399                                       * starting with MSB first */
400  static Hrc_Manager_t *implHmgr;     /* Auxiliary hierarchy manager */
401  static Hrc_Manager_t *specHmgr;     /* Auxiliary hierarchy manager */
402  static Hrc_Node_t    *currentNode;  /* node in the hierarchy */
403  static Ntk_Network_t *specNetwork;  /* spec network */
404  static Ntk_Network_t *implNetwork;  /* implementation network */
405  static st_table      *inputMatch;   /* List of pairs of input name match */
406  static st_table      *outputMatch;  /* List of pairs of output name match */
407  int                  outputsToVerifyDirectly; /* number of outputs to
408                                                 * directly verify
409                                                 */
410  int                  c;             /* To process the command line options */
411  /* Flush previous verification if any */
412  int                  success;       /* Outcome of the verification */
413  int                  status;        /* Status of the call to the function */
414  char                 *specFileName;  /* File to read the specification from */
415  char                 *impFileName;  /* File to read the implementation from */
416  char                 *fileMatchOut; /* File specifying the output matching */
417  char                 *fileMatchIn;  /* File specifying the input matching */
418  char                 *fileOutputOrder; /*file name that contains the order of
419                                           outputs starting with MSB */
420  boolean              isInBlifMv;    /* Format to be read in */
421  st_generator         *stGen;        /* generator to step through the table */
422  char                 *key, *value;  /* variables for the st_table */
423  int i;
424  int defaultOutputOrder;             /* flag to indicate default order to
425                                       * be taken, if no output order file
426                                       * is specified
427                                       */
428  char                 *strptr;       /* variable to hold return value
429                                       * of strtol
430                                       */
431  int                  allFlag;
432 
433  if (bdd_get_package_name() != CUDD) {
434    fprintf(vis_stdout, "** res error: Residue Verification is available with the CUDD package only.\n");
435    return 0;
436  }
437  /* Default values for some variables */
438  timeOutPeriod = 0;
439  allFlag = 1;
440  outputsToVerifyDirectly = 0;
441  outputOrderArray = NIL(array_t);
442  implHmgr = NIL(Hrc_Manager_t);
443  specHmgr = NIL(Hrc_Manager_t);
444  currentNode = NIL(Hrc_Node_t);
445  specNetwork = NIL(Ntk_Network_t);
446  implNetwork = NIL(Ntk_Network_t);
447  inputMatch = NIL(st_table);
448  outputMatch = NIL(st_table);
449  impFileName = NIL(char);
450  specFileName = NIL(char);
451  isInBlifMv = FALSE;
452  fileMatchOut = NIL(char);
453  fileMatchIn = NIL(char);
454  status = 1;
455  fileOutputOrder = NIL(char);
456  defaultOutputOrder = 0;
457 
458  /*
459   * Parse command line options.
460   */
461  util_getopt_reset();
462  while ((c = util_getopt(argc, argv, "bd:hi:m:n:o:Os:t:")) != EOF) {
463    switch(c) {
464    case 'b':
465      isInBlifMv = TRUE;
466      break;
467    case 'd':
468      /* number of outputs to verify directly */
469      /*      outputsToVerifyDirectly = atoi(util_optarg); */
470      outputsToVerifyDirectly = (int)strtol(util_optarg, &strptr, 0);
471      allFlag = strcmp(util_optarg, "all");
472      break;
473    case 'h':
474      goto usage;
475    case 'i':
476      impFileName = util_optarg;
477      break;
478    case 'm':
479      fileMatchOut = util_optarg;
480      break;
481    case 'n':
482      fileMatchIn = util_optarg;
483      break;
484    case 'o':
485      fileOutputOrder = util_optarg;
486      break;
487    case 'O':
488      defaultOutputOrder = 1;
489      break;
490    case 's':
491      specFileName = util_optarg;
492      break;
493    case 't':
494      timeOutPeriod = atoi(util_optarg);
495      break;
496    default:
497      goto usage;
498    }
499  }
500
501  /* Obtain the Specification network either from file or hierarchy manager */
502  if (specFileName != NIL(char)) {
503
504    /* Read blif or blif-mv depending on the flag */
505    error_init();
506    if (isInBlifMv) {
507      FILE *fp; /* Used to read from files */
508
509      /* Open the file */
510      fp = Cmd_FileOpen(specFileName, "r", NIL(char *), TRUE);
511      if (fp != NULL) {
512        specHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
513                                 0, /* No Cannonical */
514                                 0, /* No incremental */
515                                 0  /* No verbosity */);
516        fclose(fp);
517      } else {
518        fprintf(vis_stderr, "** res error: Specification file required(may not exist in path)\n");
519        goto usage;
520      }
521
522    } /* End of then */ 
523    else {
524      specHmgr = Io_BlifRead(specFileName, 0 /* No verbosity */);
525    } /* End of if-then-else */
526
527    /* Check if the read has been performed correctly */
528    if (specHmgr == NIL(Hrc_Manager_t)) {
529      (void) fprintf(vis_stderr, "%s", error_string());
530      (void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
531      goto cleanup;
532    }
533   
534    /* Hierarchy manager successfully created */
535    error_init();
536    currentNode = Hrc_ManagerReadCurrentNode(specHmgr);
537    specNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, (lsList)0);
538    if (specNetwork == NIL(Ntk_Network_t)) {
539      (void) fprintf(vis_stderr, "%s", error_string());
540      (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
541      goto cleanup;
542    }
543  } else {
544    /* Check if any circuit has been read in */
545    currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
546    if (currentNode == NIL(Hrc_Node_t)) {
547      (void) fprintf(vis_stderr, "The hierarchy manager is empty. ");
548      (void) fprintf(vis_stderr, "Read in design.\n");
549      goto cleanup;
550    }
551
552    /* Check if the network has been created with flatten_hierarchy */
553    specNetwork = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
554    if (specNetwork == NIL(Ntk_Network_t)) {
555      goto cleanup;
556    } /* End of if */
557  }
558
559  /* Obtain the implementation network from file */
560  if (impFileName != NIL(char)) {
561
562    /* Read blif or blif-mv depending on the flag */
563    error_init();
564    if (isInBlifMv) {
565      FILE *fp; /* Used to read from files */
566
567      /* Open the file */
568      fp = Cmd_FileOpen(impFileName, "r", NIL(char *), TRUE);
569
570      if (fp != NULL) {
571        implHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
572                                 0, /* No Cannonical */
573                                 0, /* No incremental */
574                                 0  /* No verbosity */);
575        fclose(fp);
576      } else {
577        fprintf(vis_stderr, "** res error: Implementation file required(may not exist in path)\n");
578        goto usage;
579      }
580
581    }  else { /* End of then */
582      implHmgr = Io_BlifRead(impFileName, 0 /* No verbosity */);
583    } /* End of if-then-else */
584
585    /* Check if the read has been performed correctly */
586    if (implHmgr == NIL(Hrc_Manager_t)) {
587      (void) fprintf(vis_stderr, "%s", error_string());
588      (void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
589      goto cleanup;
590    }
591   
592    /* Hierarchy manager successfully created */
593    error_init();
594    currentNode = Hrc_ManagerReadCurrentNode(implHmgr);
595    implNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, NULL);
596    if (implNetwork == NIL(Ntk_Network_t)) {
597      (void) fprintf(vis_stderr, "%s", error_string());
598      (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
599      goto cleanup;
600    }
601  }
602  else {
603    /* The option -1 has not been provided in the command line */
604    goto usage;
605  }
606  /* At this point both networks have been built */
607
608  /* Check that no node in the two network is multi-valued */
609  if (CheckForMultiValueNode(specNetwork)) {
610    fprintf(vis_stderr, "** res error: Specification has multivalued network\n");
611    fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
612    goto cleanup;
613  }
614  if (CheckForMultiValueNode(implNetwork)) {
615    fprintf(vis_stderr, "** res error: Implementation has multivalued network\n");
616    fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
617    goto cleanup;
618  }
619 
620  /* Check that both networks have the same number of inputs and outputs */
621  if ((Ntk_NetworkReadNumCombInputs(implNetwork) != 
622       Ntk_NetworkReadNumCombInputs(specNetwork)) ||
623      (Ntk_NetworkReadNumCombOutputs(implNetwork) != 
624       Ntk_NetworkReadNumCombOutputs(specNetwork))) {
625
626    (void) fprintf(vis_stderr, "** res error: Networks do not have equal number of inputs ");
627    (void) fprintf(vis_stderr, "or outputs\n");
628    goto cleanup;
629  } /* End of if */ 
630
631  /* Check if there has been some name matching file provided for outputs. */
632  if (fileMatchOut != NIL(char)) {
633    outputMatch = ReadMatchingPairs(fileMatchOut, implNetwork, specNetwork);
634    if (outputMatch == NIL(st_table)) {
635      (void) fprintf(vis_stderr, "** res error: Error reading Output match file ");
636      (void) fprintf(vis_stderr, "%s\n", fileMatchOut);
637      goto cleanup;
638    } /* End of if */
639  } /* End of if */
640
641  /* Check if there has been some name matching file provided for inputs. */
642  if (fileMatchIn != NIL(char)) {
643    inputMatch = ReadMatchingPairs(fileMatchIn, implNetwork, specNetwork);
644    if (inputMatch == NIL(st_table)) {
645      (void) fprintf(vis_stderr, "** res error: Error reading Input match file ");
646      (void) fprintf(vis_stderr, "%s\n", fileMatchIn);
647      /* Clean up */
648      goto cleanup;
649    } /* End of if */
650  } /* End of if */
651
652  /* Transfer names of outputs starting with MSB from the file to an
653   * array_t
654   */
655  if (fileOutputOrder != NIL(char)) {
656    outputOrderArray = ReadOutputOrder(fileOutputOrder, specNetwork);
657  } else if (defaultOutputOrder) {
658    outputOrderArray = GenerateDefaultOutputOrder(specNetwork);
659  }
660   
661  if (outputOrderArray == NIL(array_t)) {
662    /* Clean up */
663    fprintf(vis_stderr, "** res error: Output order(msb first) required for residue method.\n");
664    goto usage;
665  } else if  (array_n(outputOrderArray) != Ntk_NetworkReadNumCombOutputs(specNetwork)) {
666    fprintf(vis_stderr, "** res error: Number of Outputs seem to be %d\n", Ntk_NetworkReadNumCombOutputs(specNetwork));
667    fprintf(vis_stderr, "** res error: The output order seems to contain %d outputs\n", array_n(outputOrderArray));
668    fprintf(vis_stderr, "** res error: Partial Orders or mismatch in the above two numbers is not allowed in the -o option\n");
669    goto usage;
670  }
671  /* Start the timer before calling the verifyer */
672  if (timeOutPeriod > 0) {
673    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
674    (void) alarm(timeOutPeriod);
675
676    /* The second time setjmp is called, it returns here !!*/
677    if (setjmp(timeOutEnv) > 0) {
678      (void) fprintf(vis_stdout, "Residue Verification timeout occurred after%d seconds.\n", 
679                     timeOutPeriod);
680      alarm(0);
681
682      /* Note that there is a huge memory leak here. */
683      goto cleanup;
684    } /* End of if */
685  }
686
687  /* number of outputs to directly verify should be less than the
688   * number of outputs for the circuit. If all flag set, number of
689   * directly verified circuit, set it to number of combinational
690   * outputs.
691   */
692  if (allFlag == 0) {
693    outputsToVerifyDirectly = Ntk_NetworkReadNumCombOutputs(specNetwork);
694  }
695  if (outputsToVerifyDirectly > Ntk_NetworkReadNumCombOutputs(specNetwork)) {
696    fprintf(vis_stderr, "** res error: More outputs to directly verify than that exist in the circuit\n");
697    goto usage;
698  }
699   
700  error_init();
701
702
703  /* main procedure for residue verification */
704  status = Res_NetworkResidueVerify(specNetwork,
705                                    implNetwork,
706                                    outputsToVerifyDirectly,
707                                    outputOrderArray,
708                                    outputMatch,
709                                    inputMatch);
710   
711  /* Deactivate the alarm */
712  alarm(0);
713 
714  /* If the computation succeded store the result in specNetwork */
715  if (status == 0) {
716    Res_ResidueInfo_t *residueInfo;
717
718    residueInfo = (Res_ResidueInfo_t *) Ntk_NetworkReadApplInfo(specNetwork, 
719                                                                RES_NETWORK_APPL_KEY);
720
721    /* Print out the error string in case success is false */
722    success = Res_ResidueInfoReadSuccess(residueInfo);
723    switch (success) {
724    case FALSE:
725      (void) fprintf(vis_stdout, "Residue Verification failed !\n");
726      break;
727    case TRUE:
728      (void) fprintf(vis_stdout, "Residue Verification successful\n");
729      break;
730    default:
731      (void) fprintf(vis_stderr, "** res error: Residue Verification unable to produce ");
732      (void) fprintf(vis_stderr, "result\n");
733      break;
734    }
735  } else {
736    (void) fprintf(vis_stderr, "%s", error_string());
737  }
738
739  /* Clean up */
740  error_cleanup();
741  goto cleanup;
742 
743    /* update with all functions */
744usage:
745  (void) fprintf(vis_stderr, "usage: res_verify [-b]  ");
746  (void) fprintf(vis_stderr, "[-d n] [-h] -i impl file\n       ");
747  (void) fprintf(vis_stderr, "[-m file] [-n file] -o file [-s spec file] ");
748  (void) fprintf(vis_stderr, "[-t secs]\n");
749  (void) fprintf(vis_stderr, "   -b        The file format to be read is ");
750  (void) fprintf(vis_stderr, "blif-mv (default is blif)\n");
751  (void) fprintf(vis_stderr, "   -d n      Number of outputs to verify ");
752  (void) fprintf(vis_stderr, "directly\n");
753  (void) fprintf(vis_stderr, "   -h        Print the usage of the command\n");
754  (void) fprintf(vis_stderr, "   -i impl   Implementation file (required)\n");
755  (void) fprintf(vis_stderr, "   -m file   File specifying the matching pair ");
756  (void) fprintf(vis_stderr, "of names for the outputs\n");
757  (void) fprintf(vis_stderr, "   -n file   File specifying the matching pair");
758  (void) fprintf(vis_stderr, " of names for the inputs\n");
759  (void) fprintf(vis_stderr, "   -o        Output order starting with MSB (required or -O required)\n");
760  (void) fprintf(vis_stderr, "   -O        Default output order (required or -o required)\n");
761  (void) fprintf(vis_stderr, "   -s file   Specification File\n");
762  (void) fprintf(vis_stderr, "   -t secs   Seconds allowed for computation\n");
763
764 
765  /* Clean up */
766cleanup:
767  if ((specFileName == NIL(char)) && (specHmgr != NIL(Hrc_Manager_t))) {
768    int zerorefcountbdds;
769    bdd_manager *ddManager;
770    Hrc_ManagerFree(specHmgr);
771    if (specNetwork != NIL(Ntk_Network_t)) {
772      ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
773      if (ddManager != NIL(bdd_manager)) {
774        zerorefcountbdds = bdd_check_zero_ref((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork));
775        if (zerorefcountbdds) {
776          fprintf(vis_stdout, "Number of Nodes with non zero ref count are %d\n", zerorefcountbdds);
777          fprintf(vis_stdout, "Size of DD manager = %d\n", bdd_num_vars(ddManager));
778        }
779      }
780    }
781    Ntk_NetworkFree(specNetwork);
782  }
783  if (implHmgr != NIL(Hrc_Manager_t)) {
784    Hrc_ManagerFree(implHmgr);
785    /* dont free manager if not set here */
786    if ((specNetwork != NIL(Ntk_Network_t)) &&
787        ((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork) != NIL(bdd_manager))) {
788      Ntk_NetworkSetMddManager(implNetwork, NIL(bdd_manager));
789    }
790    Ntk_NetworkFree(implNetwork);
791  }
792  if (outputMatch != NIL(st_table)) {
793    st_foreach_item(outputMatch, stGen, &key, &value) {
794      /* free only the key, cos the value appears as a key also */
795      FREE(key);
796    }
797    st_free_table(outputMatch);
798  } /* End of if */
799  if (inputMatch != NIL(st_table)) {
800    st_foreach_item(inputMatch, stGen, &key, &value) {
801      /* free only the key, cos the value appears as a key also */
802      FREE(key);
803    }
804    st_free_table(inputMatch);
805  }
806  if (outputOrderArray != NIL(array_t)) {
807    char * name;
808    arrayForEachItem(char *, outputOrderArray, i, name) {
809      FREE(name);
810    }
811    array_free(outputOrderArray);
812  }   
813  return status;
814}  /* End of CommandResVerify */
815
816
817/**Function********************************************************************
818
819  Synopsis           [Handle the timeout signal.]
820
821  Description [This function is called when the time out occurs. In principle
822  it could do something smarter, but so far it just transfers control to the
823  point in the code where setjmp was called.]
824
825  SideEffects [This function gains control at any point in the middle of the
826  computation, therefore the memory allocated so far leaks.]
827
828******************************************************************************/
829static void
830TimeOutHandle(void)
831{
832  longjmp(timeOutEnv, 1);
833} /* End of TimeOutHandle */
834
835/**Function********************************************************************
836
837  Synopsis           [Builds a table with the pairs of names given in a file.]
838
839  Description [Given a file, it opens the and reads lines of the form <tt>name1
840  name2</tt> and stores the pairs (name1, name2) and (name2, name1) in a table
841  that returns as result.]
842 
843  SideEffects        []
844 
845  SeeAlso            [CommandResVerify]
846
847******************************************************************************/
848static st_table *
849ReadMatchingPairs(char *fileName,
850                  Ntk_Network_t *ntk1,
851                  Ntk_Network_t *ntk2)
852{
853  st_table *result = NIL(st_table);
854  int check;
855  char name1[80], name2[80]; /* Note the size of buffer is used in fscanf */
856  char *ptr1, *ptr2;
857  FILE *fp;
858#if HAVE_MKSTEMP && HAVE_CLOSE
859  int  fd;
860#else
861  char buffer[512];
862#endif
863  char *realFileName, *blifMvFileName, *visDirectoryName;
864  char command[512];
865  int cmdStatus;
866 
867  fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
868 
869  if (fp == NIL(FILE)) {
870    FREE(realFileName);
871    (void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
872    return result;
873  } /* End of if */
874 
875  if (fp != stdin){
876    (void)fclose(fp);
877  } 
878
879#if HAVE_MKSTEMP && HAVE_CLOSE
880  blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
881  fd = mkstemp(blifMvFileName);
882  if (fd == -1){
883#else
884  blifMvFileName = util_strsav(tmpnam(buffer));
885  if (blifMvFileName == NIL(char)){
886#endif
887    FREE(realFileName);
888    (void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
889    (void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
890    return NIL(st_table);
891  }
892#if HAVE_MKSTEMP && HAVE_CLOSE
893  close(fd);
894#endif
895   /* Invoking an awk script */
896  visDirectoryName = Vm_VisObtainLibrary();
897  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| sed 's/(/<</g' | sed 's/)/>>/g' > %s", realFileName, blifMvFileName);
898  /* the following is missing two new sed processings
899  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| %s -f %s/ioBlifToMv.nawk > %s", realFileName, NAWK, visDirectoryName, blifMvFileName);
900  */
901  cmdStatus = system(command);
902  FREE(visDirectoryName);
903  FREE(realFileName);
904  if (cmdStatus != 0) {
905    return NIL(st_table);
906  }
907
908  fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
909  assert(fp != NIL(FILE));
910
911
912  result = st_init_table(st_ptrcmp, st_ptrhash);
913  while (!feof(fp)) {
914    check = fscanf(fp, "%80s %80s", name1, name2);
915    if (check != 2 && check != EOF) {
916      st_free_table(result);
917      result = NIL(st_table);
918      return result;
919    } /* End of if */
920   
921    if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t) &&
922        Ntk_NetworkFindNodeByName(ntk2, name1) == NIL(Ntk_Node_t)) {
923      (void) fprintf(vis_stderr, "** res error: While reading matching file. ");
924      (void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n", 
925                     name1);
926      st_free_table(result);
927      result = NIL(st_table);
928      return result;
929    }
930   
931    if (Ntk_NetworkFindNodeByName(ntk1, name2) == NIL(Ntk_Node_t) &&
932        Ntk_NetworkFindNodeByName(ntk2, name2) == NIL(Ntk_Node_t)) {
933      (void) fprintf(vis_stderr, "** res error: While reading matching file. ");
934      (void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n", 
935                     name2);
936      st_free_table(result);
937      result = NIL(st_table);
938      return result;
939    }
940
941    ptr1 = util_strsav(name1);
942    ptr2 = util_strsav(name2);
943    st_insert(result, ptr1, ptr2);
944    st_insert(result, ptr2, ptr1);
945  } /* End of while */
946 
947  fclose(fp);
948#if HAVE_UNLINK
949  unlink(blifMvFileName);
950#endif
951  FREE(blifMvFileName);
952
953  return result;
954} /* End of ReadMatchingPairs */
955
956/**Function********************************************************************
957 
958  Synopsis           [Builds an array with the names given in a file.]
959
960  Description [Given a file, it opens the and reads lines of the form <tt>name1
961  and stores the name1 in an array that returns as result.]
962
963  SideEffects        []
964
965  SeeAlso            [CommandResVerify]
966
967******************************************************************************/
968static array_t *
969ReadOutputOrder(char *fileName,
970                Ntk_Network_t *ntk1)
971{
972  FILE *fp;
973#if HAVE_MKSTEMP && HAVE_CLOSE
974  int  fd;
975#else
976  char buffer[512];
977#endif
978  array_t *result = NIL(array_t);
979  int check;
980  char name1[80]; /* Note the size of buffer is used in fscanf */
981  char *ptr1;
982  char *realFileName, *blifMvFileName, *visDirectoryName;
983  char command[512];
984  int cmdStatus;
985 
986  fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
987 
988  if (fp == NIL(FILE)) {
989    FREE(realFileName);
990    (void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
991    return result;
992  } /* End of if */
993
994  if (fp != stdin){
995    (void)fclose(fp);
996  } 
997
998#if HAVE_MKSTEMP && HAVE_CLOSE
999  blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
1000  fd = mkstemp(blifMvFileName);
1001  if (fd == -1){
1002#else
1003  blifMvFileName = util_strsav(tmpnam(buffer));
1004  if (blifMvFileName == NIL(char)){
1005#endif
1006    FREE(realFileName);
1007    (void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
1008    (void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
1009    return NIL(array_t);
1010  }
1011#if HAVE_MKSTEMP && HAVE_CLOSE
1012  close(fd);
1013#endif
1014  /* Invoking an awk script */
1015  visDirectoryName = Vm_VisObtainLibrary();
1016  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| sed 's/(/<</g' | sed 's/)/>>/g' > %s", realFileName, blifMvFileName);
1017  /* the following is missing two new sed processings
1018  (void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| %s -f %s/ioBlifToMv.nawk > %s", realFileName, NAWK, visDirectoryName, blifMvFileName);
1019  */
1020  cmdStatus = system(command);
1021  FREE(visDirectoryName);
1022  FREE(realFileName);
1023  if (cmdStatus != 0) {
1024    return NIL(array_t);
1025  }
1026
1027  fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
1028  assert(fp != NIL(FILE));
1029 
1030  result = array_alloc(char *, 0);
1031  while (!feof(fp)) {
1032    check = fscanf(fp, "%80s", name1);
1033    if (check != EOF) {
1034      if (check != 1) {
1035        array_free(result);
1036        result = NIL(array_t);
1037        return result;
1038      } /* End of if */
1039     
1040      if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t)) {
1041        (void) fprintf(vis_stderr, "** res error: While reading output order file. ");
1042        (void) fprintf(vis_stderr, "** res error: Node %s not found in the network.\n", 
1043                       name1);
1044        array_free(result);
1045        result = NIL(array_t);
1046        return result;
1047      }
1048      ptr1 = util_strsav(name1);
1049      array_insert_last(char *, result, ptr1);
1050    }
1051  } /* End of while */
1052#ifdef DEBUG
1053  arrayForEachItem(char *,result, i, ptr1) {
1054    fprintf(vis_stdout, "%s\n", ptr1);
1055  }
1056#endif 
1057
1058  fclose(fp);
1059#if HAVE_UNLINK
1060  unlink(blifMvFileName);
1061#endif
1062  FREE(blifMvFileName);
1063
1064  return result;
1065} /* End of ReadMatchingPairs */
1066
1067
1068/**Function********************************************************************
1069 
1070  Synopsis           [Generates a default output order .]
1071
1072  Description        [This order is as provided in the file]
1073
1074  SideEffects        []
1075
1076  SeeAlso            [CommandResVerify]
1077
1078******************************************************************************/
1079static array_t *
1080GenerateDefaultOutputOrder(Ntk_Network_t *specNetwork)
1081{
1082  array_t *outputOrderArray;
1083  lsGen listGen;
1084  Ntk_Node_t *nodePtr;
1085  char *name, *ptr1;
1086  int i;
1087
1088  i = 0;
1089  outputOrderArray = array_alloc(char *,
1090                                 Ntk_NetworkReadNumCombOutputs(specNetwork));
1091  Ntk_NetworkForEachCombOutput(specNetwork, listGen, nodePtr) {
1092    name = Ntk_NodeReadName(nodePtr);
1093    ptr1 = util_strsav(name);
1094    array_insert(char *, outputOrderArray, i, ptr1);
1095    i++;
1096  }
1097  return outputOrderArray;
1098}
1099
1100/**Function********************************************************************
1101 
1102  Synopsis           [Checks if the network contains any multi-valued node .]
1103
1104  Description        [Checks if the network contains any multi-valued node.
1105  Returns 0, if none exist and 1 if there are any]
1106
1107  SideEffects        []
1108
1109  SeeAlso            [CommandResVerify]
1110
1111******************************************************************************/
1112static int
1113CheckForMultiValueNode(Ntk_Network_t *network)
1114{
1115  lsGen listGen;
1116  Ntk_Node_t *nodePtr;
1117  Var_Variable_t * var;
1118 
1119  Ntk_NetworkForEachNode(network, listGen, nodePtr) {
1120    var = Ntk_NodeReadVariable(nodePtr);
1121    if ((Var_VariableReadNumValues(var) > 2) ||
1122        (!Var_VariableTestIsEnumerative(var))) {
1123      return 1;
1124    }
1125  }
1126  return 0;
1127}
Note: See TracBrowser for help on using the repository browser.