source: vis_dev/vis-2.3/share/help/res_verifyCmd.txt

  res_verify - Verifies a combinational circuit using residue arithmetic.
     _________________________________________________________________

   res_verify [-b] [-d <n>] [-h] -i <filename> [-m <filename>] [-n <filename>]
   {-o <filename> | -O} [-s <filename>] [-t <timeOut>]

   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.

   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.

   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.

   vis> res_verify -o network.order -i network1.blif -s network2.blif

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

   A second way to perform the verification is as follows. The specification
   network is taken from a hierarchy already read into VIS. Then the res_verify
   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:

   vis> read_blifmv network1.mv
   vis> flatten_hierarchy
   vis> res_verify -o network.order -i network2.mv

   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.

   Note:  It  is  important  to  keep the specification distinct from the
   implementation because most parameters specified for the res_verify 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.

   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.

   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.

   Relevant flags to be set using the set command: 

   residue_verbosity 
          Default is 0, turns on verbosity to the desired level between 0 and
          5.

   residue_ignore_direct_verified_outputs 
          Default 0 (FALSE). If 1, then ignores directly verified outputs
          during residue verification.

   residue_top_var 
          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.

   residue_autodyn_residue_verif 
          Default 0 (FALSE). If 1, turns on dynamic reordering during residue
          verification.

   residue_residue_dyn_method 
          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".

   residue_autodyn_direct_verif 
          Default 0 (FALSE). If 1, turns on dynamic reordering during direct
          verification.

   residue_direct_dyn_method 
          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".

   residue_layer_schedule 
          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).

   residue_layer_size 
          Default largest layer size in network. Specifies the maximum layer
          size that can be composed in (relevant for vector composition only).

   residue_composition_method 
          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".

   Command Options: 

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

   -d n
          This option specifies the number of outputs to be directly verified.
          That is, for n 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.
          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.

   -h
          Print the command usage.

   -i <filename>
          Implementation network to perform verification against. The file must
          be in blif format unless -b is specified, in which case the file is
          taken to be in blif-mv format. The blif format is the default.

   -m <filename>
          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 name1 name2 to be considered as corresponding
          outputs in the verification process. In each pair, name1 may belong
          to the specification and name2 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.

   -n <filename>
          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 name1 name2 to be considered as corresponding inputs in the
          verification  process.  In  each  pair, name1 may belong to the
          specification and name2 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.

   -o <filename>
          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.

   -O
          This option specifies whether the res_verify 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.
          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.

   -s <filename>
          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 -b 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.

   -t <timeOut >
          Execution time in seconds allowed for verification before aborting.
          The default is no limit.
     _________________________________________________________________

   Last updated on 20100410 00h02