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

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

Add vis
File size: 4.8 KB
Line 
1
2  comb_verify - verify the combinational equivalence of two flattened networks
3     _________________________________________________________________
4
5   comb_verify  [-b]  [-f  <filename>]  [-h]  [-o  <ordering method>] [-t
6   <timeOut>]  [-1  <partition  method>]  [-2  <partition  method>]  [-i]
7   <filename1> [<filename2>]
8
9   This  command  verifies the combinational equivalence of two flattened
10   networks.  In  particular,  any  set of functions (the roots), defined
11   over  any  set  of intermediate variables (the leaves), can be checked
12   for equivalence between the two networks. Roots and leaves are subsets
13   of the nodes of a network, with the restriction that the leaves should
14   form  a complete support for the roots. The correspondence between the
15   roots  and the leaves in the two networks is specified in a file given
16   by  the  option -f . The default option assumes that the roots are the
17   combinational outputs and the leaves are the combinational inputs.
18
19   When there is a pseudo input in the set of leaves, the range of values
20   it  can  take  should be the same as that of the multi-valued variable
21   corresponding  to  it,  for  comb_verify  to  function correctly. This
22   restriction will be removed in future.
23
24   There  are  two  ways  to  do combinational verification. In the first
25   mode, two BLIF-MV files are given as arguments to the command, e.g.
26
27  vis> comb_verify foo.mv bar.mv
28 
29
30   Verification  is  done for the flattened networks at the root nodes of
31   the two BLIF-MV hierarchies. In any error messages printed, "network1"
32   refers to the first file, and "network2" refers to the second. Both of
33   these  networks  are  freed  at  the  end of the command. This mode is
34   totally independent from any existing hierarchy previously read in. In
35   the  second mode, it is assumed that a hierarchy has already been read
36   in.  Then,  comb_verify  can be called with a single BLIF-MV file, and
37   this will do the comparison between the network present at the current
38   node  ("network1")  and  the network corresponding to the root node of
39   the  hierarchy  in the BLIF-MV file("network2"). A typical sequence of
40   commands is:
41
42  vis> read_blifmv foo.mv
43  vis> init_verify
44  vis> comb_verify bar.mv
45 
46
47   If a hierarchy has been read in but a flattened network does not exist
48   at  the  current  node  (flatten_hierarchy  has not been invoked), the
49   command does nothing. If a network exists at the current node, but the
50   variables  haven't  been ordered, then the variables are ordered and a
51   partition  created.  This partition is freed at the end. A side-effect
52   is  that  the variables are ordered. If a partition exists, then it is
53   used  if the vertices corresponding to the roots specified are present
54   in it, otherwise a new partition is created with the current ordering.
55   The  partition  created for the new network read in is always freed at
56   the end.
57
58   Command options:
59
60   -b
61          Specifies that the files are BLIF files and not BLIF-MV files.
62
63   -f <filename>
64          Provides  the  correspondence  between  the leaves and roots of
65          network1  and  network2.  If  this  option  is  not used, it is
66          assumed  that  the  correspondence  is  by name, leaves are the
67          combinational inputs, and roots are the combinational outputs.
68
69   -h
70          Print the command usage.
71
72   -t <timeOut>
73          Time  in  seconds  allowed to perform equivalence checking. The
74          default is infinity.
75
76   -o <ordering method>
77          Specifies the ordering method to be used for assigning a common
78          ordering to the leaves of network1 and network2. If this option
79          is   not  used,  ordering  is  done  using  a  default  method.
80          Currently, only the default method is available.
81
82   -1 <partition method>
83          Specifies  the  partitioning  method  to  be used for network1.
84          Supported  methods are "total", "partial", and "inout" (see the
85          command  build_partition_mdds  for  more  information). If this
86          option  is  not  specified,  then the default method "inout" is
87          used.
88
89   -2 <partition method>
90          Specifies  the  partitioning  method  to  be used for network2.
91          Supported  methods are "total", "partial", and "inout" (see the
92          command  build_partition_mdds  for  more  information). If this
93          option is not specified, then default method "inout" is used.
94
95   -i
96          Print  Bdd statistics. This is the only way to see bdd stastics
97          during this command. print_bdd_stats after this command doesn't
98          show information related to this command.
99     _________________________________________________________________
100
101   Last updated on 20050519 10h16
Note: See TracBrowser for help on using the repository browser.