Reading the Output of Print Commands in Vis

A model initially given as a Verilog description undergoes several transformations before Vis can run model checking on it. Vis provides several printing commands to inspect the various data structures. Oftentimes, the output of these commands is a bit obscure for the casual user, but with the "help" command, and the following example, one should be able to make sense of most of it.

Commands Related to the Hierarchy

Let us consider the following very simple description.
module parity (clk,i,o);
    input  clk;
    input  i;
    output o;
    reg    o;
    initial o = 0;
    always @ (posedge clk) o = o ^ i;
endmodule // fa

If we run this code through vl2mv, we get:
# vl2mv parity.v 
# version: 0.2
# date:    19:54:06 05/20/01 ()
.model parity 
# I/O ports
.outputs o
.inputs i
# o  = 0
.names o$raw_n0
0
# non-blocking assignments for initial
# o  = o  ^ i 
# o  ^ i 
.names o i _n2
.def 0
0 1 1
1 0 1
.names _n2 o$raw_n1
- =_n2
# conflict arbitrators
.names _n3
.def 0
 1
.names _n3 o$raw_n1 _n4 
.def 0
1 0 0
1 1 1
# non-blocking assignments 
# latches
.r o$raw_n0 o
0 0
1 1
.latch _n4 o
# quasi-continuous assignment
.end

When we read parity.mv into vis and type "print_hierarchy_stats" (or, using the aliases defined in master.visrc, "phs"), we get:
vis release 1.4 (compiled 20-May-01 at 4:02 AM)
vis> rlmv parity.mv 
vis> phs
Model name = parity, Instance name = parity
inputs = 1, outputs = 1, variables = 7, tables = 5, latches = 1, children = 0

Here the numbers of inputs, outputs, and latches should come as no surprise. Notice that clk is identified as the implicit clock by vl2mv, and is not present in parity.mv. The number of tables (5) is the number of ".names" in the .mv file. The number of variables (7) reflects the fact that there are seven variables in the .mv file; namely,
  o, i, o$raw_n0, _n2, o$raw_n1, _n3, _n4.
The number of children is 0 because no module is instantiated in parity. Other commands that are applicable at this stage are "print_latches" ("pl"), "print_io" ("pio"), and "print_models" ("pm").
vis> pl
o
vis> pio
inputs: i
outputs: o
vis> pm
Model name = parity
inputs = 1, outputs = 1, variables = 7, tables = 5, latches = 1
subckts = 0

Commands Related to the Network

We now build the network for our design by calling "flatten_hierarchy" ("flt"), and then print stats about the result with "print_network_stats" ("pns").
vis> flt
vis> pns
parity  combinational=4  pi=1  po=1  latches=1  pseudo=0  const=1  edges=6

This summarizes what we get with "print_network" ("pn"):
vis> pn
Nodes of network parity:
o$NS: mdd=-1, shadow;
o$INIT: mdd=-1, combinational; constant initial-input comb-output
_n2: mdd=-1, combinational;
o: mdd=-1, latch; output comb-input comb-output
_n4: mdd=-1, combinational; data-input comb-output
i: mdd=-1, primary-input; comb-input
o$raw_n1: mdd=-1, combinational;

At this point, no MDDs/BDDs have been built for this network. Hence, we find mdd=-1 for all nodes of the network.

A few noteworthy things have happened in going from the hierarchy to the network. First of all, o$NS and o$INIT have been created to go with state variable o. They are the nodes carrying the next value and the initial value of o.

Second, some redundant nodes have been removed by constant propagation, namely _n3 and o$raw_n0. For each node, we see its type and, after a semicolon, the list of its attributes. A comb-input is either a primary input or the output of a latch. That is, it is an input to the combinational logic of the sequential circuit. (Think of the Huffman model.) Similarly for a comb-output.

The number of edges is the total number of edges of the network graph or, as "help pns" explains, the total number of fanouts of each node. In our case the edges are:

  i        -> _n2
  _n2      -> o$raw_n1
  o$raw_n1 -> _n4
  _n4      -> o
  o$INIT   -> o
  o        -> _n2
for a total of 6. This information can be obtained by typing "print_network_dot." (See below for a short discussion of dot.)

We now run "static_order" to associate BDD variables to each comb-input. Let's see how this affects the output of "print_network."
vis> so
vis> pn
Nodes of network parity:
o$NS: mdd=2, shadow;
o$INIT: mdd=-1, combinational; constant initial-input comb-output
_n2: mdd=-1, combinational;
o: mdd=1, latch; output comb-input comb-output
_n4: mdd=-1, combinational; data-input comb-output
i: mdd=0, primary-input; comb-input
o$raw_n1: mdd=-1, combinational;

We see that primary input, latch, and next state nodes have been assigned an MDD id. An MDD variable is a variable that can take a finite set of values. Each MDD variable corresponds to one or more BDD variables. In this case, all variables are two-valued; hence, each MDD variable corresponds to one (binary) BDD variable. The nodes that do not have MDD variables assigned to them still have mdd=-1.

Commands Related to the Partition

The next step is "build_partition_mdds" ("part"). This command identifies a set of comb-inputs and comb-outputs (the partition) and builds MDDs for the comb-outputs in terms of the comb-inputs. (Some intermediate variables may be used as well for large networks, but we shall ignore this detail here.)

MDDs are similar to BDDs. They differ in that their variables are multi-valued (e.g., a variable may take values BLUE, RED, and GREEN) instead of binary. MDDs are implemented as an abstraction layer on top of BDDs. So, building the MDDs boils down to building the BDDs for the network. We then use "print_partition_stats" to inquire about the result.


vis> part
vis> pps
Method Frontier, 2 sinks, 3 sources, 4 total vertices, 4 mdd nodes

We can get more information by passing the -n option.
vis> pps -n
Network nodes represented as vertices in the partition:
o
i
_n4
o$INIT
Method Frontier, 2 sinks, 3 sources, 4 total vertices, 4 mdd nodes

The partition gives the MDDs of _n4 in terms of o, i. This is seen by examining the output of "print_partition" ("pp"). The partition, as explained by "help pp," is in the format of the dot graph layout program. Things like "rotate=90" are instructions to dot on how to draw the graph. The details can be found in the documentation of dot.
vis> pp
# vis release 1.4 (compiled 20-May-01 at 4:02 AM)
# partition name: parity
# generated: Sun May 20 14:57:57 2001
#
# Partition with 4 vertices and 2 edges
digraph "parity" {
  rotate=90;
  margin=0.5;
  label="parity";
  size="10,7.5";
  ratio="fill";
  node0 [label="o"]; 
  node1 [label="i"]; 
  node2 [label="_n4"]; 
  node3 [label="o$INIT"]; 
  node1 -> node2;
  node0 -> node2;
}

The result of running dot on the output of "pp" is the following drawing. Notice that "print_network_dot" and "print_partition" are practically restricted to small models.

Node o$INIT is also part of the partition because the initial state depends on it. Since it is a constant node, no variable is associated to it. Node o$INIT is classified as both a source and a sink of the graph, because it has neither incoming arcs nor outgoing arcs.

As explained by "help pps," the number of MDD nodes is the total number for all the functions in the partition.

Other Print Commands

VIS builds a transition relation from the partition MDDs to carry out model checking or reachability analysis. The transition relations for (forward) reachability analysis and (backward) model checking are in general (not in this case, though) slightly different, and VIS builds them on demand depending of the command to be executed. However, we can force VIS to build the forward transition relation by typing "print_image_info" ("pii"). For our circuit, it results in the following:
vis> pii
Printing Information about Image method: IWLS95
	Threshold Value of Bdd Size For Creating Clusters = 5000
		(Use "set image_cluster_size value" to set this to desired value)
	Verbosity = 0
		(Use "set image_verbosity value" to set this to desired value)
	W1 =  6 W2 = 1 W3 = 1 W4 = 2
		(Use "set image_W? value" to set these to desired values)
Shared size of transition relation for forward image computation is          1 BDD nodes (1    components)

It gives information on the image computation method in effect (IWLS95, rather than, for instance, hybrid), the values of some parameters used in heuristic algorithms (users almost never change them) and the total size of the transition relation. At this point, MDDs have disappeared, and everything is in terms of the underlying BDDs.

In this case, there is only one node in the transition relation because from each of the two possible states, it is possible to transit to both states in one cycle. Also, since the transition relation is small, it is represented by a single BDD, in which the primary input variable has been existentially quantified. These two things together imply that the transition relation is the BDD that is always 1.

The "print_fairness" ("pf") command shows what fairness constraints are in effect.


vis> pf
Fairness constraint:
TRUE;

In our case, we get TRUE because there are no fairness constraints in effect. All (infinite) paths are fair because TRUE holds infinitely often along every infinite path.

After "static_order" one can inspect statistics of the BDDs by typing "print_bdd_stats." The output of this command depends on the BDD package linked to Vis, and is described in that package's documentation. For CUDD, which is the default package, the documentation can be found here.

A final class of print commands is used to display the values of the options for various Vis commands. (E.g., "print_ardc_options.") The documentation for each such command is given by help command. That is, to get information on the meaning of the options used in approximate reachability analysis, one types "help print_ardc_options."

Contact 
©2002-2018 U.C. Regents