source: vis_dev/vis-2.3/share/help/comb_verifyCmd.txt @ 101

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

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