source: vis_dev/vis-2.1/share/help/seq_verifyCmd.txt @ 11

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

Add vis
File size: 3.4 KB
Line 
1
2  seq_verify - verify the sequential equivalence of two flattened networks
3     _________________________________________________________________
4
5   seq_verify  [-b]  [-f  <filename>]  [-h]  [-p  <partition method>] [-t
6   <timeOut>] [-B] [-i] [-r] <filename> [<filename>]
7
8   Please  read  the  documentation  for  the  command comb_verify before
9   reading  on.  The concepts of roots and leaves in this command are the
10   same  as  for  comb_verify, except for an added constraint: the set of
11   leaves  has  to  be  the  set  of  all  primary inputs. This obviously
12   produces  the  constraint  that  both networks have the same number of
13   primary  inputs.  Moreover,  no pseudo inputs should be present in the
14   two  networks  being  compared.  The  set of roots can be an arbitrary
15   subset of nodes.
16
17   The  command  verifies  whether  any  state,  where  the values of two
18   corresponding  roots  differ,  can  be reached from the set of initial
19   states  of  the  product  machine.  If  this happens, a debug trace is
20   provided.
21
22   The  sequential  verification  is  done by building the product finite
23   state machine.
24
25   The  command  has two execution modes, just as for comb_verify. In the
26   first mode, two BLIF-MV files are given as arguments to the command:
27
28  vis> seq_verify foo.mv bar.mv
29 
30
31   In  the second mode, a single BLIF-MV file is taken. This is network2.
32   It  is assumed that network1 is from a hierarchy that has already been
33   read   in.  If  a  network  is  present  at  the  current  node  (i.e.
34   flatten_hierarchy  has  been  executed),  it is used for verification;
35   otherwise the command does nothing.
36
37  vis> read_blifmv foo.mv
38  vis> flatten_hierarchy
39  vis> seq_verify bar.mv
40 
41
42   Command options:
43
44   -b
45          Specifies that the input files are BLIF files.
46
47   -f <filename>
48          Provides  the  correspondence  between  the leaves and roots of
49          network1  and  network2.  leaves  has  to be the set of primary
50          inputs  of  the  networks. roots can be any subset of nodes. If
51          this  option is not used, it is assumed that the correspondence
52          is by name, and that the roots are the combinational outputs.
53
54   -h
55          Print the command usage.
56
57   -p <partition method>
58          Specifies  the  partitioning  method  for  the product machine.
59          Supported  methods are "total", "partial", and "inout" (see the
60          command  build_partition_mdds  for  more  information). If this
61          option  is  not  specified,  then the default method "inout" is
62          used.
63
64   -t <timeOut>
65          Time  in  seconds  allowed to perform equivalence checking. The
66          default is infinity.
67
68   -B
69          Use  backward  image computation to traverse the state space of
70          the  product  machine.  By default, forward image computaion is
71          used.
72
73   -i
74          Print  BDD statistics. This is the only way to see BDD stastics
75          during this command. print_bdd_stats after this command doesn't
76          show information related to this command.
77
78   -r
79          Enable  DBB  reordering during the equivalence check. Note that
80          dynamic_var_ordering  has  no  effect  on whether reordering is
81          enabled during the execution of seq_verify.
82     _________________________________________________________________
83
84   Last updated on 20050519 10h16
Note: See TracBrowser for help on using the repository browser.