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

/**CFile***********************************************************************

  FileName    [resCmd.c]

  PackageName [res]

  Synopsis [Implements the different commands related to the residue
  verification.]

  Description [This file provides the wrapper functions for the commands
  involving the residue verification. The command res_verify receives at least
  one file describing an implementation and optionally a second one describing
  a specification of a circuit and a set of different options and calls the
  procedure to perform residue verification in the two systems. For more
  detailed information about the command res_verify, see also CommandResVerify]

  Author      [Kavita Ravi    <ravi@duke.colorado.edu> and
               Abelardo Pardo <abel@duke.colorado.edu>]
               
  Copyright [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

******************************************************************************/

#include "resInt.h" 

static char rcsid[] UNUSED = "$Id: resCmd.c,v 1.58 2010/04/10 00:38:26 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

static jmp_buf timeOutEnv;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int CommandResVerify(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void TimeOutHandle(void);
static st_table * ReadMatchingPairs(char *fileName, Ntk_Network_t *ntk1, Ntk_Network_t *ntk2);
static array_t * ReadOutputOrder(char *fileName, Ntk_Network_t *ntk1);
static array_t * GenerateDefaultOutputOrder(Ntk_Network_t *specNetwork);
static int CheckForMultiValueNode(Ntk_Network_t *network);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis [Initializes the Residue Verification package.]

  SideEffects []

  SeeAlso     [Tst_End]

******************************************************************************/
void
Res_Init(void)
{
  Cmd_CommandAdd("res_verify", CommandResVerify, /* doesn't changes_network */ 0);
}


/**Function********************************************************************

  Synopsis [Ends the residue verification package.]

  SideEffects []

  SeeAlso     [Tst_Init]

******************************************************************************/
void
Res_End(void)
{
  /*
   * For example, free any global memory (if any) which the test package is
   * responsible for.
   */
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Implements the res_verify command.]

  CommandName [res_verify]

  CommandSynopsis [Verifies a combinational circuit using residue
  arithmetic.]

  CommandArguments [\[-b\] \[-d &lt;n&gt;\]
  \[-h\] -i &lt;filename&gt; \[-m &lt;filename&gt;\] \[-n
  &lt;filename&gt;\] {-o &lt;filename&gt; | -O} \[-s &lt;filename&gt;\] \[-t
  &lt;timeOut&gt;\] ]
  
  CommandDescription [This command performs residue verification between two
  networks. The method used is based on residue arithmetic and the Chinese
  Remainder theorem; it is
  described in [1\] ftp://vlsi.colorado.edu/pub/fmcad96.ps.
  Verification is performed
  by interpreting the outputs of the circuits  as integers
  and verifying the residues of the outputs  with respect to a set of
  moduli. The choice of moduli is directed  by the Chinese Remainder Theorem in order
  to prove equivalence of the two circuits. This method works well with multipliers
  and possibly other arithmetic circuits (due to its  dependence on residue
  arithmetic).
  For the same reason, it is necessary to specify an output order
  which determines how the outputs are interpreted as integers.
  Discretion should be exercised in applying this method to general combinational
  circuits.

  <p>
  Residue verification is available only if vis is linked with the cu
  BDD package. (This is the default.) It reads both
  blif and blif-mv files. However, it does NOT support multi-valued
  variables. Residue verification is primarily for combinational
  verification, but may be applied to sequential circuits with the
  same state encoding. The latch outputs are then considered to be combinational inputs of the
  circuits and the latch inputs and reset are considered to be combinational
  outputs of the circuits. 
  
  <p>
  There are two ways to perform residue verification in this package. As a first option, two
  files describing two networks, the specification and the implementation, (in
  the same format, blif or blif-mv, see option -b) are given in the command
  line; the procedure
  tries to verify the equivalence of the combinational outputs as functions of
  the combinational inputs.

  <p>

  <code>
  vis> res_verify -o network.order -i network1.blif -s network2.blif <br>
  </code>

  <p>

  In this case both networks are read in, flattened and the verification is
  performed between the combinational outputs of both networks. The <tt>-i</tt>
  option denotes the implementation file and the <tt>-s</tt> option denotes
  the specification file. The -o option specifies
  the order of outputs for the circuits (See Command Options below for detailed
  explanation).
  

  <p> 
  A second way to perform the verification is as follows. The specification
  network is taken from a hierarchy  already read into VIS.  Then the <tt>res_verify </tt>
  command compares that specification against an implementation network obtained from
  the file in the command line. Any previous verification, performed with the
  specification, can be used towards the
  next verification task only if the same implementation circuit is being verified
  against and the same number of outputs have been  directly verified with sucess
  in the previous attempt. The typical sequence of commands given to perform such
  task would be:

  <p>
  <code> 
  vis> read_blifmv network1.mv <br>
  vis> flatten_hierarchy  <br>
  vis> res_verify -o network.order -i network2.mv <br>
  </code>

  <p>
  
  If the hierarchy has been read but no flattened network exists at the current
  node, the command will return without doing anything.

  If one of the networks used is the one in the current node in the hierarchy,
  then the information regarding the verification process will be stored in
  that network.

  <p>
  <B> Note: </b>
  It is important to keep the specification distinct from the implementation
  because most  parameters specified for the <tt> res_verify </tt> command
  are with respect to the specification. For example, the output order 
  is specified with respect to the specification.
  The file that is read in first in the second format, is considered to be the specification. 

  <p>
  There is an option to directly verify some outputs by building the
  BDDs for the corresponding outputs of the 2 circuits. In that case,
  if the user wants to use an initial ordering, the only way to do it is
  the second method and reading in the network, one may specify the initial
  order using static order.

  <p> 
  The command does not repeat residue verification if the same
  specification-implementation pair have been 
  verified with success and the same number of directly verified
  outputs have been verified in the previous attempt.

  <p>
  <b> Relevant flags to be set using the set command: </b> <p>
  <dl> 
  <dt> <b> residue_verbosity </b>
  <dd> Default is 0, turns on verbosity to the desired level between 0 and 5. 

  <dt> <b> residue_ignore_direct_verified_outputs </b>
  <dd> Default 0 (FALSE). If 1, then ignores directly verified outputs
  during residue verification. 

  <dt> <b> residue_top_var </b>
  <dd> Default "msb". The 2 possible values are "msb" and lsb"; this puts
  the most/least significant bit near the top or bottom of the residue decision diagram.
  
  <dt> <b> residue_autodyn_residue_verif </b>
  <dd> Default 0 (FALSE). If 1, turns on dynamic reordering during residue
  verification.
  
  <dt> <b> residue_residue_dyn_method </b>
  <dd> Default "groupsift". Specifies the method for dynamic reordering during
  residue verification. Other methods supported are "same" (same as before),
  "none", "random", "randompivot", "sift", "siftconverge", "symmsiftconverge",
  "symmsift", "window2", "window3", "window4", "window2converge",
  "window3converge", "window4converge", "groupsift", "groupsiftconverge",
  "anneal", "genetic", "linear", "linearconverge", "exact". 

  <dt> <b> residue_autodyn_direct_verif </b>
    <dd> Default 0 (FALSE). If 1, turns on dynamic reordering during direct
  verification.
  
  <dt> <b> residue_direct_dyn_method </b>
  <dd> Default "groupsift". Specifies the method for dynamic reordering during
  direct verification. Other methods supported are "same" (same as before),
  "none", "random", "randompivot", "sift", "siftconverge", "symmsiftconverge",
  "symmsift", "window2", "window3", "window4", "window2converge",
  "window3converge", "window4converge", "groupsift", "groupsiftconverge",
  "anneal", "genetic", "linear", "linearconverge", "exact".
  
  <dt> <b> residue_layer_schedule </b>
  <dd> Default "alap". This is a flag to specify the layering strategy of the
  networks. The 2 options are "asap" (as soon as possible) and "alap" (as
  late as possible).

  <dt> <b> residue_layer_size </b>
  <dd> Default largest layer size in network. Specifies the maximum layer
  size  that can be composed in (relevant for vector composition only).
  
  <dt> <b> residue_composition_method </b>
  <dd> Default "vector". Specifies the composition method to be used in
  composing the network into the residue ADD. The options are "vector",
  "onegate", "preimage" and "superG".
  <p>
  </dl>
  
  <b> Command Options: </b> <br>

  <dl>

  <dt> -b 
  <dd> If this option is specified, the specification and the implementation
  files read  are considered to be in blif-mv format. Default is blif
  format. <p>

  <dt> -d n
  <dd> This option specifies the number of outputs to be directly verified.
  That is, for <tt> n </tt> least significant outputs of the circuit, this command
  performs like comb_verify.
  The actual outputs are read off the output order array.
  Since the output order array is specified starting with the MSB, the number of
  directly verified outputs will be a chunk of the bottom part of the output order array.
  The option "-d all" sets the number of directly verified outputs to the
  number of combinational outputs in the circuit i.e., all outputs are directly
  verified.
  The direct verification for small BDD sizes is faster and overall reduces
  the number of primes to be used in residue verification. In general,
  one output is checked at a time against the corresponding output of the
  other network and consequently , this method may be fast and use less memory
  resources.<br>
  IMPORTANT: It is possible to specify an initial order for the direct
  verification. This is done by reading in the specification file and using
  static_order to specify the initial order. The implementation will get
  the same order as the specification. When specifying the initial order,
  one must be careful not to specify the -s option in the res_verify command.
  The -s option reads in the specification file again and the initial order
  is lost.  <p> 
  
  <dt> -h 
  <dd> Print the command usage.<p> 

  <dt> -i &lt;filename&gt; 
  <dd> Implementation network to perform verification against. The file must be
  in blif format unless <tt>-b</tt> is specified, in which case the file is
  taken to be in blif-mv format. The blif format is the default.<p>

  <dt> -m &lt;filename&gt; 
  <dd> Optional file name specifying the matching pair of output names between
  the two networks. If not specified, it is assumed that all outputs have
  identical names. This option is useful when verifying two circuits whose
  output names do not match. The file will give pairs of the form <tt>name1
  name2</tt> to be considered as corresponding  outputs in the verification
  process. In each pair, <tt> name1 </tt> may belong to the specification
  and <tt> name2 </tt> to the implementation or vice-versa. The matching
  procedure is not capable of dealing with some
  special situations. For example, when two outputs, one of each network have the same
  name, they must correspond to the same output. Partial orders may not be specified. <p> 

  <dt> -n &lt;filename&gt; 
  <dd> Optional file name specifying the matching pair of input names between
  the two networks. If not specified, it is assumed that all inputs have
  identical names. This option is useful when verifying two circuits whose
  input  names do not match. The file will give pairs of the form <tt>name1
  name2</tt> to be considered as corresponding  inputs in the verification
  process. In each pair, <tt> name1 </tt> may belong to the specification
  and <tt> name2 </tt> to the implementation or vice-versa. The matching
  procedure is not capable of dealing with some
  special situations. For example, when two inputs, one of each network have the same
  name, they must correspond to the same input. Partial orders may not be specified. <p> 

  <dt> -o &lt;filename&gt;
  <dd> Required file  specifying output order, starting with the MSB.
  The file must be a list of output names separated by spaces. 
  The list must belong to the specification network and must contain a
  full order i.e., must contain all the combinational output names.  It is advisable to use
  the -o option as far as possible to specify the order
  of the outputs.See also -O option.<p> 

  <dt> -O
  <dd> This option specifies whether the <code> res_verify </code> command should
  generate a default
  order for the outputs. If the -o option is not used, this option must be specified.
  The default order generated is random and is NOT the same as the input files.
  The set of outputs for the output order may be generated by using the print_network
  command to write the network into a file and extract the node name from the  lines containing the word
  "comb-output". The set of outputs can then be ordered as required.  <br>
  It is advisable to use the -o option as far as possible to specify the order
  of the outputs. The -o option overrides the -O option. See also -o option.<p>
  
  <dt> -s &lt;filename&gt; 
  <dd> Specification network. This network will be taken as the specification
  of the circuit. The result of the computation will be stored in this network.
  If this network is not provided, the current node of the
  hierarchy will be taken. The file must contain a blif description of a
  circuit unless the option <tt>-b</tt> is specified, in which case the file is
  considered in blif-mv format. If two networks are specified in the
  command line, both of them must have the same format, either blif or
  blif-mv. The blif format is the default.<p>

  <dt> -t &lt;timeOut &gt;

  <dd> Execution time in seconds allowed for verification before aborting.  The
  default is no limit.<p>

  </dl>
  ]

  SideEffects [It registers the information about the verification in the
  specification if this is the current node in the hierarchy manager.]

  SeeAlso            [Res_NetworkResidueVerify]

******************************************************************************/
static int
CommandResVerify(Hrc_Manager_t ** hmgr,
                 int  argc,
                 char ** argv)
{
  static int           timeOutPeriod; /* CPU seconds allowed */
  static array_t       *outputOrderArray;   /* required to specify the outputs
                                       * starting with MSB first */
  static Hrc_Manager_t *implHmgr;     /* Auxiliary hierarchy manager */
  static Hrc_Manager_t *specHmgr;     /* Auxiliary hierarchy manager */
  static Hrc_Node_t    *currentNode;  /* node in the hierarchy */
  static Ntk_Network_t *specNetwork;  /* spec network */
  static Ntk_Network_t *implNetwork;  /* implementation network */
  static st_table      *inputMatch;   /* List of pairs of input name match */
  static st_table      *outputMatch;  /* List of pairs of output name match */
  int                  outputsToVerifyDirectly; /* number of outputs to
                                                 * directly verify
                                                 */
  int                  c;             /* To process the command line options */
  /* Flush previous verification if any */
  int                  success;       /* Outcome of the verification */
  int                  status;        /* Status of the call to the function */
  char                 *specFileName;  /* File to read the specification from */
  char                 *impFileName;  /* File to read the implementation from */
  char                 *fileMatchOut; /* File specifying the output matching */
  char                 *fileMatchIn;  /* File specifying the input matching */
  char                 *fileOutputOrder; /*file name that contains the order of
                                           outputs starting with MSB */
  boolean              isInBlifMv;    /* Format to be read in */
  st_generator         *stGen;        /* generator to step through the table */
  char                 *key, *value;  /* variables for the st_table */
  int i;
  int defaultOutputOrder;             /* flag to indicate default order to
                                       * be taken, if no output order file
                                       * is specified
                                       */
  char                 *strptr;       /* variable to hold return value
                                       * of strtol
                                       */
  int                  allFlag;
  
  if (bdd_get_package_name() != CUDD) {
    fprintf(vis_stdout, "** res error: Residue Verification is available with the CUDD package only.\n");
    return 0;
  }
  /* Default values for some variables */
  timeOutPeriod = 0;
  allFlag = 1;
  outputsToVerifyDirectly = 0;
  outputOrderArray = NIL(array_t);
  implHmgr = NIL(Hrc_Manager_t);
  specHmgr = NIL(Hrc_Manager_t);
  currentNode = NIL(Hrc_Node_t);
  specNetwork = NIL(Ntk_Network_t);
  implNetwork = NIL(Ntk_Network_t);
  inputMatch = NIL(st_table);
  outputMatch = NIL(st_table);
  impFileName = NIL(char);
  specFileName = NIL(char);
  isInBlifMv = FALSE;
  fileMatchOut = NIL(char);
  fileMatchIn = NIL(char);
  status = 1;
  fileOutputOrder = NIL(char);
  defaultOutputOrder = 0;
  
  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "bd:hi:m:n:o:Os:t:")) != EOF) {
    switch(c) {
    case 'b':
      isInBlifMv = TRUE;
      break;
    case 'd':
      /* number of outputs to verify directly */
      /*      outputsToVerifyDirectly = atoi(util_optarg); */
      outputsToVerifyDirectly = (int)strtol(util_optarg, &strptr, 0);
      allFlag = strcmp(util_optarg, "all");
      break;
    case 'h':
      goto usage;
    case 'i':
      impFileName = util_optarg;
      break;
    case 'm':
      fileMatchOut = util_optarg;
      break;
    case 'n':
      fileMatchIn = util_optarg;
      break;
    case 'o':
      fileOutputOrder = util_optarg;
      break;
    case 'O':
      defaultOutputOrder = 1;
      break;
    case 's':
      specFileName = util_optarg;
      break;
    case 't':
      timeOutPeriod = atoi(util_optarg);
      break;
    default:
      goto usage;
    }
  }

  /* Obtain the Specification network either from file or hierarchy manager */
  if (specFileName != NIL(char)) {

    /* Read blif or blif-mv depending on the flag */
    error_init();
    if (isInBlifMv) {
      FILE *fp; /* Used to read from files */

      /* Open the file */
      fp = Cmd_FileOpen(specFileName, "r", NIL(char *), TRUE);
      if (fp != NULL) {
        specHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
                                 0, /* No Cannonical */
                                 0, /* No incremental */
                                 0  /* No verbosity */);
        fclose(fp);
      } else {
        fprintf(vis_stderr, "** res error: Specification file required(may not exist in path)\n");
        goto usage;
      }

    } /* End of then */ 
    else {
      specHmgr = Io_BlifRead(specFileName, 0 /* No verbosity */);
    } /* End of if-then-else */

    /* Check if the read has been performed correctly */
    if (specHmgr == NIL(Hrc_Manager_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
      goto cleanup;
    }
    
    /* Hierarchy manager successfully created */
    error_init();
    currentNode = Hrc_ManagerReadCurrentNode(specHmgr);
    specNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, (lsList)0);
    if (specNetwork == NIL(Ntk_Network_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
      goto cleanup;
    }
  } else {
    /* Check if any circuit has been read in */
    currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
    if (currentNode == NIL(Hrc_Node_t)) {
      (void) fprintf(vis_stderr, "The hierarchy manager is empty. ");
      (void) fprintf(vis_stderr, "Read in design.\n");
      goto cleanup;
    }

    /* Check if the network has been created with flatten_hierarchy */
    specNetwork = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
    if (specNetwork == NIL(Ntk_Network_t)) {
      goto cleanup;
    } /* End of if */
  }

  /* Obtain the implementation network from file */
  if (impFileName != NIL(char)) {

    /* Read blif or blif-mv depending on the flag */
    error_init();
    if (isInBlifMv) {
      FILE *fp; /* Used to read from files */

      /* Open the file */
      fp = Cmd_FileOpen(impFileName, "r", NIL(char *), TRUE);

      if (fp != NULL) {
        implHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
                                 0, /* No Cannonical */
                                 0, /* No incremental */
                                 0  /* No verbosity */);
        fclose(fp);
      } else {
        fprintf(vis_stderr, "** res error: Implementation file required(may not exist in path)\n");
        goto usage;
      }

    }  else { /* End of then */
      implHmgr = Io_BlifRead(impFileName, 0 /* No verbosity */);
    } /* End of if-then-else */

    /* Check if the read has been performed correctly */
    if (implHmgr == NIL(Hrc_Manager_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
      goto cleanup;
    }
    
    /* Hierarchy manager successfully created */
    error_init();
    currentNode = Hrc_ManagerReadCurrentNode(implHmgr);
    implNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, NULL);
    if (implNetwork == NIL(Ntk_Network_t)) {
      (void) fprintf(vis_stderr, "%s", error_string());
      (void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
      goto cleanup;
    }
  }
  else {
    /* The option -1 has not been provided in the command line */
    goto usage;
  }
  /* At this point both networks have been built */

  /* Check that no node in the two network is multi-valued */
  if (CheckForMultiValueNode(specNetwork)) {
    fprintf(vis_stderr, "** res error: Specification has multivalued network\n");
    fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
    goto cleanup;
  }
  if (CheckForMultiValueNode(implNetwork)) {
    fprintf(vis_stderr, "** res error: Implementation has multivalued network\n");
    fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
    goto cleanup;
  }
  
  /* Check that both networks have the same number of inputs and outputs */
  if ((Ntk_NetworkReadNumCombInputs(implNetwork) != 
       Ntk_NetworkReadNumCombInputs(specNetwork)) ||
      (Ntk_NetworkReadNumCombOutputs(implNetwork) != 
       Ntk_NetworkReadNumCombOutputs(specNetwork))) {

    (void) fprintf(vis_stderr, "** res error: Networks do not have equal number of inputs ");
    (void) fprintf(vis_stderr, "or outputs\n");
    goto cleanup;
  } /* End of if */  

  /* Check if there has been some name matching file provided for outputs. */
  if (fileMatchOut != NIL(char)) {
    outputMatch = ReadMatchingPairs(fileMatchOut, implNetwork, specNetwork);
    if (outputMatch == NIL(st_table)) {
      (void) fprintf(vis_stderr, "** res error: Error reading Output match file ");
      (void) fprintf(vis_stderr, "%s\n", fileMatchOut);
      goto cleanup;
    } /* End of if */
  } /* End of if */

  /* Check if there has been some name matching file provided for inputs. */
  if (fileMatchIn != NIL(char)) {
    inputMatch = ReadMatchingPairs(fileMatchIn, implNetwork, specNetwork);
    if (inputMatch == NIL(st_table)) {
      (void) fprintf(vis_stderr, "** res error: Error reading Input match file ");
      (void) fprintf(vis_stderr, "%s\n", fileMatchIn);
      /* Clean up */
      goto cleanup;
    } /* End of if */
  } /* End of if */

  /* Transfer names of outputs starting with MSB from the file to an
   * array_t
   */
  if (fileOutputOrder != NIL(char)) {
    outputOrderArray = ReadOutputOrder(fileOutputOrder, specNetwork);
  } else if (defaultOutputOrder) {
    outputOrderArray = GenerateDefaultOutputOrder(specNetwork);
  }
    
  if (outputOrderArray == NIL(array_t)) {
    /* Clean up */
    fprintf(vis_stderr, "** res error: Output order(msb first) required for residue method.\n");
    goto usage;
  } else if  (array_n(outputOrderArray) != Ntk_NetworkReadNumCombOutputs(specNetwork)) {
    fprintf(vis_stderr, "** res error: Number of Outputs seem to be %d\n", Ntk_NetworkReadNumCombOutputs(specNetwork));
    fprintf(vis_stderr, "** res error: The output order seems to contain %d outputs\n", array_n(outputOrderArray));
    fprintf(vis_stderr, "** res error: Partial Orders or mismatch in the above two numbers is not allowed in the -o option\n");
    goto usage;
  }
  /* Start the timer before calling the verifyer */
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);

    /* The second time setjmp is called, it returns here !!*/
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "Residue Verification timeout occurred after%d seconds.\n", 
                     timeOutPeriod);
      alarm(0);

      /* Note that there is a huge memory leak here. */
      goto cleanup;
    } /* End of if */
  }

  /* number of outputs to directly verify should be less than the
   * number of outputs for the circuit. If all flag set, number of
   * directly verified circuit, set it to number of combinational
   * outputs.
   */
  if (allFlag == 0) {
    outputsToVerifyDirectly = Ntk_NetworkReadNumCombOutputs(specNetwork);
  }
  if (outputsToVerifyDirectly > Ntk_NetworkReadNumCombOutputs(specNetwork)) {
    fprintf(vis_stderr, "** res error: More outputs to directly verify than that exist in the circuit\n");
    goto usage;
  }
    
  error_init();


  /* main procedure for residue verification */
  status = Res_NetworkResidueVerify(specNetwork,
                                    implNetwork,
                                    outputsToVerifyDirectly,
                                    outputOrderArray,
                                    outputMatch,
                                    inputMatch);
    
  /* Deactivate the alarm */
  alarm(0);
  
  /* If the computation succeded store the result in specNetwork */
  if (status == 0) {
    Res_ResidueInfo_t *residueInfo;

    residueInfo = (Res_ResidueInfo_t *) Ntk_NetworkReadApplInfo(specNetwork, 
                                                                RES_NETWORK_APPL_KEY);

    /* Print out the error string in case success is false */
    success = Res_ResidueInfoReadSuccess(residueInfo);
    switch (success) {
    case FALSE:
      (void) fprintf(vis_stdout, "Residue Verification failed !\n");
      break;
    case TRUE:
      (void) fprintf(vis_stdout, "Residue Verification successful\n");
      break;
    default:
      (void) fprintf(vis_stderr, "** res error: Residue Verification unable to produce ");
      (void) fprintf(vis_stderr, "result\n");
      break;
    }
  } else {
    (void) fprintf(vis_stderr, "%s", error_string());
  }

  /* Clean up */
  error_cleanup();
  goto cleanup;
  
    /* update with all functions */
usage:
  (void) fprintf(vis_stderr, "usage: res_verify [-b]  ");
  (void) fprintf(vis_stderr, "[-d n] [-h] -i impl file\n       ");
  (void) fprintf(vis_stderr, "[-m file] [-n file] -o file [-s spec file] ");
  (void) fprintf(vis_stderr, "[-t secs]\n");
  (void) fprintf(vis_stderr, "   -b        The file format to be read is ");
  (void) fprintf(vis_stderr, "blif-mv (default is blif)\n");
  (void) fprintf(vis_stderr, "   -d n      Number of outputs to verify ");
  (void) fprintf(vis_stderr, "directly\n");
  (void) fprintf(vis_stderr, "   -h        Print the usage of the command\n");
  (void) fprintf(vis_stderr, "   -i impl   Implementation file (required)\n");
  (void) fprintf(vis_stderr, "   -m file   File specifying the matching pair ");
  (void) fprintf(vis_stderr, "of names for the outputs\n");
  (void) fprintf(vis_stderr, "   -n file   File specifying the matching pair");
  (void) fprintf(vis_stderr, " of names for the inputs\n");
  (void) fprintf(vis_stderr, "   -o        Output order starting with MSB (required or -O required)\n");
  (void) fprintf(vis_stderr, "   -O        Default output order (required or -o required)\n");
  (void) fprintf(vis_stderr, "   -s file   Specification File\n");
  (void) fprintf(vis_stderr, "   -t secs   Seconds allowed for computation\n");

  
  /* Clean up */
cleanup:
  if ((specFileName == NIL(char)) && (specHmgr != NIL(Hrc_Manager_t))) {
    int zerorefcountbdds;
    bdd_manager *ddManager;
    Hrc_ManagerFree(specHmgr);
    if (specNetwork != NIL(Ntk_Network_t)) {
      ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
      if (ddManager != NIL(bdd_manager)) {
        zerorefcountbdds = bdd_check_zero_ref((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork));
        if (zerorefcountbdds) {
          fprintf(vis_stdout, "Number of Nodes with non zero ref count are %d\n", zerorefcountbdds);
          fprintf(vis_stdout, "Size of DD manager = %d\n", bdd_num_vars(ddManager));
        }
      }
    }
    Ntk_NetworkFree(specNetwork);
  }
  if (implHmgr != NIL(Hrc_Manager_t)) {
    Hrc_ManagerFree(implHmgr);
    /* dont free manager if not set here */
    if ((specNetwork != NIL(Ntk_Network_t)) &&
        ((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork) != NIL(bdd_manager))) {
      Ntk_NetworkSetMddManager(implNetwork, NIL(bdd_manager));
    }
    Ntk_NetworkFree(implNetwork);
  }
  if (outputMatch != NIL(st_table)) {
    st_foreach_item(outputMatch, stGen, &key, &value) {
      /* free only the key, cos the value appears as a key also */
      FREE(key);
    }
    st_free_table(outputMatch);
  } /* End of if */
  if (inputMatch != NIL(st_table)) {
    st_foreach_item(inputMatch, stGen, &key, &value) {
      /* free only the key, cos the value appears as a key also */
      FREE(key);
    }
    st_free_table(inputMatch);
  }
  if (outputOrderArray != NIL(array_t)) {
    char * name;
    arrayForEachItem(char *, outputOrderArray, i, name) {
      FREE(name);
    }
    array_free(outputOrderArray);
  }    
  return status;
}  /* End of CommandResVerify */


/**Function********************************************************************

  Synopsis           [Handle the timeout signal.]

  Description [This function is called when the time out occurs. In principle
  it could do something smarter, but so far it just transfers control to the
  point in the code where setjmp was called.]

  SideEffects [This function gains control at any point in the middle of the
  computation, therefore the memory allocated so far leaks.]

******************************************************************************/
static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */

/**Function********************************************************************

  Synopsis           [Builds a table with the pairs of names given in a file.]

  Description [Given a file, it opens the and reads lines of the form <tt>name1
  name2</tt> and stores the pairs (name1, name2) and (name2, name1) in a table
  that returns as result.]
  
  SideEffects        []
  
  SeeAlso            [CommandResVerify]

******************************************************************************/
static st_table *
ReadMatchingPairs(char *fileName,
                  Ntk_Network_t *ntk1,
                  Ntk_Network_t *ntk2)
{
  st_table *result = NIL(st_table);
  int check;
  char name1[80], name2[80]; /* Note the size of buffer is used in fscanf */
  char *ptr1, *ptr2;
  FILE *fp;
#if HAVE_MKSTEMP && HAVE_CLOSE
  int  fd;
#else
  char buffer[512];
#endif
  char *realFileName, *blifMvFileName, *visDirectoryName;
  char command[512];
  int cmdStatus;
  
  fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
  
  if (fp == NIL(FILE)) {
    FREE(realFileName);
    (void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
    return result;
  } /* End of if */
  
  if (fp != stdin){
    (void)fclose(fp);
  }  

#if HAVE_MKSTEMP && HAVE_CLOSE
  blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
  fd = mkstemp(blifMvFileName);
  if (fd == -1){
#else
  blifMvFileName = util_strsav(tmpnam(buffer));
  if (blifMvFileName == NIL(char)){
#endif
    FREE(realFileName);
    (void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
    (void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
    return NIL(st_table);
  }
#if HAVE_MKSTEMP && HAVE_CLOSE
  close(fd);
#endif
   /* Invoking an awk script */
  visDirectoryName = Vm_VisObtainLibrary();
  (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);
  /* the following is missing two new sed processings 
  (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);
  */
  cmdStatus = system(command);
  FREE(visDirectoryName);
  FREE(realFileName);
  if (cmdStatus != 0) {
    return NIL(st_table);
  }

  fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
  assert(fp != NIL(FILE));


  result = st_init_table(st_ptrcmp, st_ptrhash);
  while (!feof(fp)) {
    check = fscanf(fp, "%80s %80s", name1, name2);
    if (check != 2 && check != EOF) {
      st_free_table(result);
      result = NIL(st_table);
      return result;
    } /* End of if */
    
    if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t) &&
        Ntk_NetworkFindNodeByName(ntk2, name1) == NIL(Ntk_Node_t)) {
      (void) fprintf(vis_stderr, "** res error: While reading matching file. ");
      (void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n", 
                     name1);
      st_free_table(result);
      result = NIL(st_table);
      return result;
    }
    
    if (Ntk_NetworkFindNodeByName(ntk1, name2) == NIL(Ntk_Node_t) &&
        Ntk_NetworkFindNodeByName(ntk2, name2) == NIL(Ntk_Node_t)) {
      (void) fprintf(vis_stderr, "** res error: While reading matching file. ");
      (void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n", 
                     name2);
      st_free_table(result);
      result = NIL(st_table);
      return result;
    }

    ptr1 = util_strsav(name1);
    ptr2 = util_strsav(name2);
    st_insert(result, ptr1, ptr2);
    st_insert(result, ptr2, ptr1);
  } /* End of while */
  
  fclose(fp);
#if HAVE_UNLINK
  unlink(blifMvFileName);
#endif
  FREE(blifMvFileName);

  return result;
} /* End of ReadMatchingPairs */

/**Function********************************************************************
  
  Synopsis           [Builds an array with the names given in a file.]

  Description [Given a file, it opens the and reads lines of the form <tt>name1
  and stores the name1 in an array that returns as result.]

  SideEffects        []

  SeeAlso            [CommandResVerify]

******************************************************************************/
static array_t *
ReadOutputOrder(char *fileName,
                Ntk_Network_t *ntk1)
{
  FILE *fp;
#if HAVE_MKSTEMP && HAVE_CLOSE
  int  fd;
#else
  char buffer[512];
#endif
  array_t *result = NIL(array_t);
  int check;
  char name1[80]; /* Note the size of buffer is used in fscanf */
  char *ptr1;
  char *realFileName, *blifMvFileName, *visDirectoryName;
  char command[512];
  int cmdStatus;
  
  fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
  
  if (fp == NIL(FILE)) {
    FREE(realFileName);
    (void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
    return result;
  } /* End of if */

  if (fp != stdin){
    (void)fclose(fp);
  }  

#if HAVE_MKSTEMP && HAVE_CLOSE
  blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
  fd = mkstemp(blifMvFileName);
  if (fd == -1){
#else
  blifMvFileName = util_strsav(tmpnam(buffer));
  if (blifMvFileName == NIL(char)){
#endif
    FREE(realFileName);
    (void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
    (void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
    return NIL(array_t);
  }
#if HAVE_MKSTEMP && HAVE_CLOSE
  close(fd);
#endif
  /* Invoking an awk script */
  visDirectoryName = Vm_VisObtainLibrary();
  (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);
  /* the following is missing two new sed processings 
  (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);
  */
  cmdStatus = system(command);
  FREE(visDirectoryName);
  FREE(realFileName);
  if (cmdStatus != 0) {
    return NIL(array_t);
  }

  fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
  assert(fp != NIL(FILE));
  
  result = array_alloc(char *, 0);
  while (!feof(fp)) {
    check = fscanf(fp, "%80s", name1);
    if (check != EOF) {
      if (check != 1) {
        array_free(result);
        result = NIL(array_t);
        return result;
      } /* End of if */
      
      if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t)) {
        (void) fprintf(vis_stderr, "** res error: While reading output order file. ");
        (void) fprintf(vis_stderr, "** res error: Node %s not found in the network.\n", 
                       name1);
        array_free(result);
        result = NIL(array_t);
        return result;
      }
      ptr1 = util_strsav(name1);
      array_insert_last(char *, result, ptr1);
    }
  } /* End of while */
#ifdef DEBUG
  arrayForEachItem(char *,result, i, ptr1) {
    fprintf(vis_stdout, "%s\n", ptr1);
  }
#endif  

  fclose(fp);
#if HAVE_UNLINK
  unlink(blifMvFileName);
#endif
  FREE(blifMvFileName);

  return result;
} /* End of ReadMatchingPairs */


/**Function********************************************************************
  
  Synopsis           [Generates a default output order .]

  Description        [This order is as provided in the file]

  SideEffects        []

  SeeAlso            [CommandResVerify]

******************************************************************************/
static array_t *
GenerateDefaultOutputOrder(Ntk_Network_t *specNetwork)
{
  array_t *outputOrderArray;
  lsGen listGen;
  Ntk_Node_t *nodePtr;
  char *name, *ptr1;
  int i;

  i = 0;
  outputOrderArray = array_alloc(char *,
                                 Ntk_NetworkReadNumCombOutputs(specNetwork));
  Ntk_NetworkForEachCombOutput(specNetwork, listGen, nodePtr) {
    name = Ntk_NodeReadName(nodePtr);
    ptr1 = util_strsav(name);
    array_insert(char *, outputOrderArray, i, ptr1);
    i++;
  }
  return outputOrderArray;
}

/**Function********************************************************************
  
  Synopsis           [Checks if the network contains any multi-valued node .]

  Description        [Checks if the network contains any multi-valued node.
  Returns 0, if none exist and 1 if there are any]

  SideEffects        []

  SeeAlso            [CommandResVerify]

******************************************************************************/
static int
CheckForMultiValueNode(Ntk_Network_t *network)
{
  lsGen listGen;
  Ntk_Node_t *nodePtr;
  Var_Variable_t * var;
  
  Ntk_NetworkForEachNode(network, listGen, nodePtr) {
    var = Ntk_NodeReadVariable(nodePtr);
    if ((Var_VariableReadNumValues(var) > 2) ||
        (!Var_VariableTestIsEnumerative(var))) {
      return 1;
    }
  }
  return 0;
}