source: vis_dev/vis-2.3/share/help/seq_verifyCmd.txt @ 19

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

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