SMV(1) SMV(1)
NAME
smv - symbolic model verifier
SYNOPSIS
smv -switch[val]... option=value... -Idir...
-Dsym=val... file.[smv,v]
DESCRIPTION
Verify or simulate a program in the SMV language, or Syn-
chronous Verilog language, using symbolic model checking
techniques. This is intended mainly for batch use. For
interactive use, see vw(1). All input files are piped
through a preprocessor much like the C preprocessor.
Files on the command line, or in "are interpreted as Syn-
chonous Verilog, and are translated to SMV by vl2smv(1).
If -check switch is present (see below), checks only the
properties with the given name, or descendants of the
given name. Results are stored in file "file.out". This
file contains one record for each assertion checked, spec-
ifying the the truth value of the assertion and if false,
a counterexample showing why the assertion is false. Addi-
tional command line options are read from the file.cflags,
if it exists. These options apply to all properties veri-
fied. Property-specific options are read from the file
"file.options". See "Options file" below for the format
of this file. If "file.cflags" does not exist, and options
for a given property are not specified in "file.options",
then the default options "-v 1 -f -h" are added to the
command line options. The default options can be disabled
on the command line with the switch "--".
Options are specified on the command line in the form
option=value, where "option" is the option name, and
"value" is its value. Each option has an abbreviation in
the form "-switch". For boolean options, this sets the
value of the switch to 1. For example, "-f" is equivalent
to "ForwardSearch=1". The only way to switch this option
off is "ForwardSearch=0". For non-boolean options, the
option value is the next word in the command line. For
example, "-v 1" is equivalent to "Verbose=1".
OPTIONS
This is a partial list of the available options, in the
"-switch" form only. Use "smv -help" for a complete list,
including the "option=value" form.
-- Do not use the default options.
-abs filename
Specifies the abstraction file.
-absref
Use proof-based abstraction when model checking.
This technique is most effective when large parts
of the system being verified are not relevant to
the property being verified.
-bmc Use bounded model checking. This technique searchs
for a counterexample of bounded length, using a SAT
solver. It can prodce a counterexample, but cannot
prove a property true. The length bound on the
counterexample is specified by the -l switch. The
bounded model checking tool "bmc" and the SAT
solver "sato" must be installed in your PATH.
-check name
Check the named assertion. If a structure is speci-
fied, all assertions contained in that structure
are checked.
-de Use conjunctive decompositions in model checking.
-Dsymbol=value
Define a symbol for the preprocessor, as in cc.
-enum Enumerate unknown values. This prevents propatation
of "unkown" values by introducing combinatinal
variables.
-f Compute reachable states by forward search and
restrict model checking to these states. This is
particularly useful when checking state machines
and protocols where the state-space is sparse. It
is not recommended for checking data paths.
-foo filename
Output final variable order (after model checking
and sifting) to file filename.
-fsift Sift just once, after all properties checked. Use-
ful only with -foo.
-Ipathname
Look in directory "pathname" for include files, as
in cc.
-i variable-order-file
Read the BDD variable order from the given file.
This allows the variable order to be modified with
a text editor. See "Variable order file" below for
the format of this file. See alo the -o switch.
-l length
Specify the maximum counterexample length (as the
number of transitions) for bounded model checking
(see the switch -bmc). A value of zero transitions
means search for a counterexample in the initial
state.
-lazy Only compile module instances on demand. This can
speed up loading very large input files by orders
of magnitude. However, the global circular check is
skipped when using this option, so you must run SMV
without -lazy to be certain your proof is valid.
-m module-name
Treat the named module as the main module.
-nopr Do not used partitioned transition relations.
-nocp Do not use conjunctive partitioning of the transi-
tion relation.
-nodp Do not use disjunctive partitioning of the transi-
tion relation.
-o variable-order-file
Output the variable BDD variable order to the given
file and stop without checking any assertions. See
also -i option.
-persist
Keep checking properties even after one is found to
be false.
-pf number
Profile any BDD's larger than the given number of
nodes.
-run trace-file
Run a the simulation trace described in the given
file. Format of this file is described below under
SIMULATION.
-sif Use external model checker via the SIF interface
(see below).
-sifliveness
The external solver supports liveness checking.
-sifsolver solver
Use solver as the external model checker.
-sift Use sifting to attempt to improve the variable
order.
-smcsat2
Use SAT-based model checking (version 2). Like
proof-based abstraction, this technique is most
effective when large parts of the system being ver-
ified are not relevant to the property being veri-
fied. If you are suffering from BDD explosion using
-absref, you may want to try this.
-stubs filename
This file lists names of structures (one to a line)
that are not to be used in the verification. This
is chiefly used to avoid parsing a very large mod-
ule in the hierarchy that is not relevant to the
assertions being checked.
-together
Check all properties in a property group in the
same model checker run. This means that the transi-
tion relation and the reached state set will be
computed only once for the group.
-v number
A non-zero value causes a transcript of the run to
be printed on the standard output. Higher numbers
cause more output.
-Z Initialize any uninitialized state variables to
zero. This is useful for large codes translated
from verilog that do not initialize registers. It
is also completely bogus.
THE OPTIONS FILE
The file "file.options" is used to set property specific
options. It consists of lines of the form:
name : "command line options";
(where the quotation marks are necessary). This sets the
options of any property which is a descendant of "name",
and not otherwise set.
ABSTRACTION FILES
When verifying a given property, you can use definitions
of signals at a chosen level of abstraction. This defines
the "environment" for verifying the given property. The
abstraction file consists of lines of the form
name//layer
where "name" is a name in the signal name hierarchy of the
program and "layer" is a layer in the program. When veri-
fying properties, the definiton of "name" will be taken
from "layer". Signals which have no entry in the abstrac-
tion file inherit their abstraction layer from their par-
ent. This makes it possible to set the abstraction layer
for an entire module instance with a single line in the
abstraction file.
In addition to the layers defined in the program, "layer"
may also take on the value "." (which stands for the low-
est, or "implementation" layer) and "free", which leaves
the signal undefined (free to take any value at any time).
If no layer is specified for a given signal, the highest
(most abstract) available layer is used.
There are three cases when the layer specified in the
abstraction file may not be used by the model checker:
1) If the given signal is not defined in the given layer,
the model checker will choose the next lower layer in
which the signal is defined.
2) If you are verifying refinement of foo//bar, you cannot
use the definition of foo in layer bar, since this would
be circular reasoning. Similarly, to cannot chose a defin-
tion at a higher layer. In this case, smv uses the next
layer below bar for the given signal.
3) The given signal may not be in the dependency cone of
the property. In this cae, it is not used at all. Note
that the dependency cone is a function of the chosen
abstraction.
PROPERTY GROUPS FILE
The file "file.groups" is used to define groups of proper-
ties that are treated as a single property. It consists of
lines of the form
group-name : {property-name, property-name, ... property-
name}
Note that a property name can be any name in the name
hierarchy. For example, if "foo" is a module instance,
then including "foo" in the group will include all proper-
ties contained in instance "foo", provided they are not
listed in another group under a more specific name. As an
example, suppose we have an array of properties p[0]
group1 : {p}
group2 : {p[2]}
The group1 will contain p[0], p[1] and p[3], while group2
contains p[2].
VARIABLE ORDERING
Smv uses Binary Decision Diagrams (BDDs) to represent sets
and relations in the model checking algorithm. A BDD is a
decision tree, in which variables always appear in the
same order as the tree is traversed from root to leaf.
The efficiency of BDDs is obtained by always combining
isomorphic subtrees, and by eliminating redundant decision
nodes in the tree. The degree of storage efficiency
obtained in this way depends stringly on the variable
ordering. There are built-in heuristics for selecting the
variable ordering, and these are invoked by the default
option "-h". If you disable this option (in the ".cflags",
or ".options" file, or by using the "--" option), the
variables appear in the BDDs in the same order in which
their types are declared in the program. This means that
variables declared in the same module are grouped
together, which is sometimes better than the heuristic
order. Sifting (see the -sift options above) can be used
to attempt to improve on the variable order. This takes
some extra time but usually saves space. It is recommended
to try "-sift" if the BDD sizes become very large, however
this is not a default option, as it often slows down the
verification process.
For the intrepid, the variable ordering may be adjusted by
hand. This can be done either by adding redundant vari-
able declarations to the program, so that the variables
are declared in the desired order, or by creating a vari-
able order file (see "Variable order file" below). A good
heuristic is to arrange the ordering so that variables
which often appear close to each other in formulas are
close together in the order, and global variables should
appear first. If the "-v 1" option (default) is used, the
sizes of BDD's are printed on the transcript. An impor-
tant number to look at is the number of BDD nodes repre-
senting the transition relation. It is very important to
minimize this number. Iterations are used to solve the
fixed point equations which characterize the various tem-
poral operators, and also to search for counterexamples.
With each iteration, the number of BDD nodes is printed.
Some of the options can improve performance. Experiment
with them if the run time or memory usage starts getting
out of hand.
VARIABLE ORDER FILE
A variable order file specifies the initial order for the
BDD variables. The syntax of this file is:
order:: item item ... item
item:: signal-name
signal-name.#
{ order }
item1 except item2
group item
A signal name can be any point in the signal name hierar-
chy (e.g., the name of a simple signal, or an array, or a
module instance). All the descendants of the given signal
name will appear in type definition order. Only the first
occurrence of a signal name counts. The construct "item1
except item2" causes signals in item2 to occur after item1
in the order, even if they occur in item1. For example,
if x is an array 0..3, then
x except x[2]
is the same as x[0] x[1] x[3] x[2]. The "group" construct
is used currently only with the -de option, which uses
"conjunctive decompositions". Finally, foo.n, where n is
a number denotes the the n-th encoding variable of foo,
counting from 0 (assuming foo is not a boolean). This is
useful to know in case you are editing an order file out-
put from smv.
SIMULATION
A simultation trace file is a sequence of assignments to
program variables. Each of these assignments overrides the
value of the given variables in the given state of program
execution. The format of this file is a sequence of
assignments of the form:
{a1, a2, ..., ak}
where each ai is of the form
vari = vali
or
vari := vali
The former case is a "suggestion" meaning that if vali is
among the possible choices for vari, then vali is chosen,
but otherwise the choice is unaffected. The latter case is
an "override" meaning that the value of vari is set to
vali and any assignment made to vari in the program is
ignored.
Note, the assignment may be empty: {}. If a simulation
trace file is specified with the -run option (see above),
the program is simulated for the given number of steps
with the given suggestions and overrides, and the result
is dumped to the result file (file.out). Note that no par-
ticular behavior is guaranteed for nondeterministic
choices that are determined by the trace input file. One
of the available values will be chosen, but this choice is
not made in any statistically useful way, and it is not
guaranteed that all possible choices will eventually be
taken.
Simulation output in the result file can be viewed with
vw(1).
USING VW WITH XEMACS
Smv can interact with the XEmacs text editor. To enable
this feature, you must put the line
(load-library "smv-hooks")
in your ~/.emacs file, and the file "smv-hooks.el" must be
in some directory in the list "load-library-path".
Once "smv-hooks" is loaded, files ending in ".smv" will
use smv-mode. This is very similar to c-mode, except that
it supports the smv syntax. Further, if you run smv from
inside an emacs shell buffer, emacs can display the file
containing an error, and place a pointer "=>" on the line
contining the def. To enable this, you must define the
environment variable "VW_EMACS".
Note, these features have been tested only using Xemacs
version 19.16. They may or may not work with other ver-
sions.
COMPATIBILITY WITH CARNEGIE MELLON SMV
This version of SMV is (mostly) source-compatible with
Carnegie Mellon SMV. Modules written in the two languages
may be mixed. In addition, SPEC declarations specifying
CTL formulas to check may be included in any module. These
specs can be named, in the following manner:
<name>:SPEC<formula>; In general, however, constructs from
the current language and the original Carnegie Mellon ver-
sion may not be mixed within a single module.
INTERFACING TO AN EXTERNAL MODEL CHECKER
SMV can interface to an external model checker via the SIF
file format. The protocol for doing this is described in
the file "smvsif.txt", which is distributed with SMV.
SEE ALSO
vw(1),vl2smv(1)
K.L.McMillan,The SMV language
Kenneth L. McMillan, Symbolic Model Checking, Kluwer,
1993.
BUGS
See the relase notes.
AUTHOR
Kenneth L. McMillan, Cadence Berkeley Labs
mcmillan@cadence.com
SMV (Cadence version) 23 Jan 1996 1