>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> dear sir
vg> (1)For the code below readings shown by the command
vg> "print_network" are not understood. What does mdd=0 or 1 or -1
vg> indicates?
vg> (2)"print_network_stats" shows "edges =4",how?
vg> where i should refer in the site to understand mdd's.
You may want to read
@INPROCEEDINGS { Sriniv90 ,
ADDRESS = "Santa Clara, CA" ,
AUTHOR = "A. Srinivasan and T. Kam and S. Malik and R. K. Brayton" ,
BOOKTITLE = "Proceedings of the International Conference on
Computer-Aided Design (ICCAD)" ,
MONTH = nov ,
PAGES = "92-95" ,
TITLE = "Algorithms for Discrete Function Manipulation" ,
YEAR = "1990"
}
vg> (3 readings shown by "print_partition".
vg> what does rotate,margin,label,size,ratio means?
vg> ******************************************************
vg> module fa(a,b,sum);
vg> input a,b;
vg> output sum;
vg> assign sum=(a^b);
vg> endmodule
Let me use a slightly modified description as working example to
asnwer all the other questions. (The reason for the modification is
to have one latch.)
------------------------------ parity.v ------------------------------
module parity (clk,i,o);
input clk;
input i;
output o;
reg o;
initial o = 0;
always @ (posedge clk) o = o ^ i;
endmodule // fa
------------------------------ parity.v ------------------------------
If we run this code through vl2mv, we get:
------------------------------ parity.mv ------------------------------
# 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
------------------------------ parity.mv ------------------------------
When we read parity.mv into vis and type "print_hierarchy_stats" (or
"phs" for short), we get:
vis release 1.4 (compiled 20-May-01 at 4:02 AM)
Sourcing .visrc for Fabio.
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 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.
We now build the network for our design by calling "flatten_heirarchy"
("flt"), and then print stats about the result with "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, latche, 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 coresponds to one (binary) BDD variable.
The nodes that do not have an MDD variable assigned to them still have
mdd=-1.
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;
}
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.
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, as opposed to, for instance, hybrid), the values of some
parameters used in heuritic 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.
To summarize, from the Verilog file to the form in which VIS puts a
circuit for model checking. At each step, vis provides statistics.
Oftentimes, these statistics are a bit obscure for the causal user,
but with the "help" command, and the example above, one can make sense
of most of it.
Fabio
This archive was generated by hypermail 2b30 : Sun May 20 2001 - 16:25:10 MDT