VW(1) VW(1)
NAME
vw - viewer for smv
SYNOPSIS
vw [file.[smv,v]]
DESCRIPTION
This is a graphical user interface for smv(1). Provides
source browsing, counterexample browsing, abstraction
editing, proof management, and spreadsheet-style simula-
tion. The file name is optional, and can be specified
instead by pulling down the "File" menu and choosing
"Open...". All input files are piped through a preproces-
sor much like the C preprocessor. Files with extension
".v", are interpreted as Synchonous Verilog, and are
translated to SMV by vl2smv(1).
There are no command line switches, as in smv(1). Any smv
compile-time options, such as -D and -I should be put in
the file "file.cflags". See smv(1) for definitions of
these switches. This file may also contain global options
that apply to all properties to be verified. If there is
no "file.cflags", some default options are used (see
smv(1) ). Model checking options that are generic, or spe-
cific to a given property, can be also be specified using
vw.
The vw graphical interface consistes of a main menu bar,
and a collection of "panes", each of which can be brought
into view by clicking its tab. These panes are described
below.
GETTING STARTED AND EXITING VW
To open a file, if you did not specify one on the command
line, either select "Open..." item from the "File" menu to
open an existing file, or "New..." to create a new file.
New files will be opened in the XEmacs text editor for
editing (see section on XEmacs below). If you modify any
source files, use the "Reopen" menu item to see these
changes in vw. Use "Quit" in the "File" menu to exit vw.
If you kill vw with keyboard interrupt, it won't remember
its state the next time you run it.
THE BROWSER PANE
Once a file is open, the browser shows a view on the name
hierarchy of the SMV program. This includes names of both
signals and assertions (properties to be proved). Any
name in this hierarchy (such as "foo.bar") is in either an
"open" or "closed" state. In the open state, all the chil-
dren of the name are shown immediately below and indented.
In the closed state, the children are not shown. If a
given name is closed, and has children that are not shown,
then a plus sign (+) appears after the name. Click the
plus sign or double-click the name to open it. Click the
minus sign, or double-click again to close it.
THE SOURCE PANE
When you click on a name in the name browser, the source
pane shows you where in the program source that name is
declared. You can also display a source line where the
given signal is assigned, or initialized, and if there is
a trace in the trace view window, you can display the
source line where the signal is assigned at the currently
selected time in a trace. You can choose one of these
options using the "Show" menu in the source pane.
Note, if the smv file is derived from a verilog file, or
another source language, the browser will try to trace the
definition back to the original source language file.
The "File" menu in the source pane shows a list of the
source files that are currently loaded into SMV (including
those that are included using "include" directives.
BROWSING THE SOURCE
When you select the name of a signal or assertion in the
browser, the GoTo menu provides to options: "Backward..."
and "Forward...". The latter produces a list of all the
signals the the selected signal depends on in the current
cone. The latter produces a list of all the signals that
depend on the current signal in the current cone. When
you select an item from the list, you "zap" to that sig-
nal. This is just as if you had clicked on the signal name
in the name browser. Thus, the signal becomes selected in
the browser, and the source view displays the definition
line of the signal. If necessary, ancestors of the signal
name will be "opened" in the browser in order to make the
signal name visible. At this point, you can use "GoTo" to
see the dependencies of the new signal, and thus work
backward or forward through the dependency graph of the
program.
The "History" menu contains a short history of the names
you have selected in the name browser. Selecting a name in
this menu causes you to "zap" to that name.
THE PROPERTIES PANE
A "property" in an smv program is anything that needs to
be verified. This includes assertions in temporal logic
and refinement checks. Every property has a name. Asser-
tions are normally named in the program source. An unnamed
assertion is given the name of the module instance in
which it appears. Refinement checks have names of the form
"x//y", where "x" is a signal name, and "y" is the name of
the layer being refined.
All the properties in your SMV program are listed in the
properties pane. For each, a "status" is given, which can
be either "verified", "unverified", or "assumed". A select
box allows you to choose to view "All properties", "unver-
ified properties", "Verified properties" or "Assumed prop-
erties". A property can be selected for verification by
clicking on it in the properties pane. The currently
selected property also appears at the bottom of the VW
window.
THE CONE PANE
The cone pane shows a list of all the signals that are in
the "cone" of the currently selected property. This is the
set of all signals on which the property depends, for a
given abstraction. For each signal, the cone pane shows
the layer or layers whose definitions of that signal are
used in the abstraction. For an explantion of why a given
layer was chosen for a given signal, click on that signal
and select "Explain abstraction" from the "Abstraction"
menu. The cone pane also shows you how many of the signals
in the cone are "state variables" and "combinational"
variables. You can choose to see the "Entire cone", "All
Variables", "State variables", or "Free variables" (the
latter are those variables that are unconstrained in the
abstraction).
VERIFYING PROPERTIES
To verify all of the properties in the program, select
"Verify" from the "Props" menu. To verify only the
selected property, select "Verify property" from the
"Props" menu, where "property" is the property name. This
will run the smv model checker in the background, and
notify you when the verification is completed.
To kill the verification in progress, select "Props:Kill
verification".
THE LOG PANE
During verication, a log of the verification process
appears in this pane. Assuming you are using the "-v 1"
option, you can observe this pane to see the sizes of the
BDD's as the model checking progresses.
THE RESULTS PANE
The results pane shows the results of the most recent ver-
ification run. Each property that was checked is listed,
along with its truth value. Clicking on a property in the
results pane will cause it to become the "current" prop-
erty, as if it had been selected in the properties pane.
In addition, if you click on a false property, a coun-
terexample for it will appear in the trace pane.
THE USING PANE
When a property is selected for verification, the "using"
pane displays a list of all the temporal logic assertions
that are used as assumptions when proving the current
property. For each property, it displays whether the prop-
erty is assumed "up to t", "up to t - 1", or "always".
THE TRACE PANE
The trace view displays counterexamples and simulation
traces. It is essentially a spreadsheet, where the rows
represent signals and the columns represent time. Ini-
tially, all of the signals in the cone appear in the trace
pane. If there is a large number of signals, it is some-
times more convenient to delete all the rows (select
Edit|Delete All), and then insert the signals you are
interested in. To insert a signal, drag it from the
Browser or the Cone pane to a cell in the Trace pane. This
will insert a new row in the Trace pane containing the
trace of the selected signal. If the signal has children,
a new row will be created for each child (thus, for exam-
ple, of you drag the "top level" into the trace pane, you
will all of the available traces.
An alternative method is to select a signal in the browser
or cone panes, click a row to insert in, and and choose
"Edit|Insert". This will open a new row, and insert the
selected signal name in the leftmost column. You can
select this signal by just pressing return. Or you can
type in the name of a signal and press return. Once you
have a set of signals you like in the trace pane, you can
save this set to a file by choosing "View|Save Trace
View..." in the trace pane. This configuration can be
restored by using "View|Restore Trace View...". Note that
this saves only the names of the signals, and not the
traces themselves, which may have changed when you later
restore the trace view.
Normally, SMV returns to a view of all the signals when-
ever a new trace is displayed. If you don't like this
behavior, check "View|Show Requested Traces" in the trace
pane.
Use "View|Zoom In" and "View|Zoom Out" to change the col-
umn scale of the trace display.
To see where in the source code a given signal was
assigned its value at a given time, click on a cell in the
trace pane, then switch to the source pane and select
"Show|Where Assigned In Trace".
Instead of using the mouse, you can also select cells in
the trace pane using the arrow keys on your keyboard, or
using "incremental search" (see INCREMENTAL SEARCH below).
MODIFYING TRACES AND SIMULATION
You can treat a trace in the trace view window like a
spreadsheet, modifying some values, and then recomputing
the entire trace to reflect these modifications.
This allows vw to be used as an interactive simulator
for smv programs, though a fairly inefficient one.
You can change the value in a cell by clicking on the cell
and choosing "Suggest value" or "Override value" from the
"Edit" menu. Then type a value into the cell and press
return. You can then recalculate the trace by choosing
"Run|Recalculate Trace". An "override" causes the given
value to be fixed no matter what value is actually
assigned by the program to the given signal at the given
time. A "suggestion" sets the value of the signal only if
the suggested value is among the possible nondeterministic
choices for that signal at that time.
To extend the trace, choose "Run|Extend Trace..." and
enter the number of columns to add. This will give you a
longer trace to work with. You can then enter some values
and recalculate.
Hint: if you have asynchronous processes in your model,
you can select a processes to run at a given time by using
"Override value" to set its "running" variable to one.
LOADING AND SAVING TRACES
The trace curently in the trace view window can be saved
to a file with "File|Save Trace". You can load a trace
into the trace view window with "File|Load Trace". A new
trace, consisting of only an initial state, can be created
with "File|New Trace".
SELECTING PROPERTY SPECIFIC OPTIONS
When you choose a property in the properties pane, the
"Options..." item in the "Props" menu becomes activated.
When you select this, a menu of model checking options is
presented. See the smv(1) entry for details on these
options. The options you select are stored in
"file.options" for use by future runs of the model
checker. Note that your choices here override the default
options.
If you have selected property "foo", you can copy the
options from property "bar" to "foo" by selecting
"Props:Copy options...", and the selecting "bar" from the
"Copy options from..." dialog.
EDITING AN ENVIRONMENT ABSTRACTION
When verifying a given property, you can define an
abstract view of the program to use when verifying the
property. You do this by choosing one or more "layers" to
define each signal. This defines the "environment" for
verifying the given property. Normally these choices are
made in the program source with the "using...prove" decla-
ration. However, you can override these choices on a
property by property basis using vw.
Once you have chosen a property, you can set the layer to
use for any given signal by clicking on that signal and
pulling down the "Abstraction" menu. Note that a signal
whose abstraction is not set inherits its abstraction from
its parent. Thus, you can set the abstraction for an
entire module instance by setting the abstraction for the
module instance name.
In an smv program without "layers", you have three
choices: "(none)", "." and "free". In the first case, you
allow smv to choose the abstraction for this signal. In
the second case, you are telling smv to use the signal
definition found in the "implementation" layer, the lowest
layer in the refinement hierarchy. Finally, if you choose
"free" then no definition will be used for this signal.
The signal will be free to take any value at any time.
Note that if you choose "free" for a given signal, you
remove a dependency from the property's environment. This
means that the size of the property's "cone" can be
reduced, and some signals may disappear from the name
browser when "filter cone" is selected.
If the smv program has defined "layers", then the name of
each layer will also appear in the "Abstraction" menu.
Choosing a given layer will cause the definition of the
selected signal to be taken from that layer, when verify-
ing the current property. There are three cases when your
choice of abstraction 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 case, it is not used at all. Note
that the dependency cone is a function of the chosen
abstraction.
Normally, vw shows you abstraction layer choices that the
model checker will actually use in the browser pane.
Radio buttons in the "View" menu allow you to toggle
between showing the "Requested layer" (the one you select)
and the "Actual layer" (the one smv will use).
ABSTRACTION FILES
The environment abstraction for a given property is stored
in an abstraction file (which you can also edit with a
text editor). The first time to make an abstraction selec-
tion for a given property, you will be asked if you want
to create an abstraction for that file. This will create a
file with an name of the form "#####.abs". It is a good
idea not to delete these files, unless you want to clear
all the abstractions.
The abstraction for a given property is considered an
"option" and is also copied by "Props:Copy options...".
You have the choice in this case to create a new copy of
the abstraction file or to share the same abstraction file
between the two properties. In the latter case, changes to
the abstraction of one property will affect the other.
If you want to edit an abstraction file by hand, you can
find the name of the abstraction file for a given property
by looking in "file.options", under the given property
name. The abstraction file name is the argument of the
"-abs" switch.
SAVING AND RESTORING THE ABSTRACTION FILE
If you are editing the abstraction for a given property
and want to save it to disk, choose "File:Save abstrac-
tion". If you make a mistake and want to get back the
saved version use "File:Restore abstraction". Note, how-
ever, that running the model checker will cause the
abstraction to be saved, and any previously saved file
will thus be overwritten.
PROPERTY GROUPS
A property group is a collection of properties that
behaves exactly like a single property from the point of
view of the foregoing discussion. You create and manage
property groups using the "group view" window. A list of
the currently existing groups is shown in the left-hand
pane of this window. When you select a group by clicking
on it, the properties it contains are listed in the right-
hand pane. To create a new group, click the "New group"
button and enter a name for the new group in the dialog
box. To add a signal to the currently listed group, select
the signal name in the name browser and click the "Add"
button. To delete a signal, select the signal name in
group view window and click the "Delete button".
Note that to verify a property group, or edit its options
and abstraction, you must first select it in the proper-
ties pane. This is not done automatically by selecting
the group in the "group view" window. Also note that a
group marked "verified" in the proeprties pane when all
the properties in the groups are verified.
There are two reasons for creating property groups. The
first is that you may have a collection of similar proper-
ties or refinements for which you would like to use the
same options and abstraction file. Since a group is
treated as a single property, there is only one option
setting and one abstraction file for the entire group.
The second reason for creating a group is that for effi-
ciency reasons, you may want to check all of the proper-
ties in the group in the same model checking run. This
means that the transition relation and reached state set
will be computed only once for the group. To get this
effect, select the option "check all properties together"
in the options menu (under "Props:Options...").
CONTROLLING VW FROM THE KEYBOARD
Most operations of vw can be controlled from the keyboard.
Any visible menu can be "pulled down" by holding down the
"Alt" key and typing the underlined letter in the menu
name. For example, the "File" menu can be accessed by typ-
ing Alt-f. Once the menu is displayed, a menu item can be
selected by typing the underlined letter in the menu item.
Thus, for example, to open a file, type "Alt-f o". Don't
use the shift key, even if the letter is capitalized.
Similarly, each pane can be accessed by holding down "Alt"
and typing the letter that is underlined on the pane's
tab. This also puts the keyboard focus on the selected
pane, which means that further keyboard commands are
directed to that pane. Pressing the tab key moves the key-
board focus to the next "widget" that is capable of
receiving keyboard input. Focus is indicated by a dark
outline around the widget. Thus, for example, to change
the selection in the cone pane from "Entire cone" to
"State variables", first type "Alt-c" to make the cone
pane visible, then press tab until the select box with
"Entire cone" is visible, then press the "down arrow" key
until "State variables" is highlighted, then press Enter.
INCREMENTAL SEARCH
Items in most of the panes of can be selected from the
keyboard using "incremental search" (exceptions are the
source and log panes). This is very much like the function
of the same name in GNU emacs. To use incremental search,
put the keyboard focus on the list that you want to search
(for example, type Alt-b to put the focus in the browser
pane). Then type "C-s" (i.e., Ctrl and s) to start
searching, and type a few letters contained in the signal
name you are searching for. Vw will outline the first sig-
nal in the browser containing that name. As you continue
typing characters, vw will move the the outline so that it
always indicates the first entry containing the characters
you have typed thus far. To see the next matching entry,
type "C-s" again, and so forth. To go back to the previous
match, press "C-r". To erase a character you have typed in
error, press Del. To stop the search and select the
currently outlined item, press Enter. To cancel the search
taking no action, press "C-g". You also start a search
backward from the currently selected entry by typing "C-
r". In the browser pane, once you have selected an entry,
you can open or close it by pressing Enter again. You can
also move up or down in the list using the arrow keys.
USING VW WITH XEMACS
Vw uses the XEmacs version 21.1 as its text editor. To use
this feature, you must have XEmacs installed on your sys-
tem. See www.xemacs.org for instructions on downloading
and installing XEmacs. In addition, you must put the line
(load-library "smv-hooks")
in your ~/.emacs file, and the files "smv-hooks.el" and
"smv-mode.el" must be in some directory in the list "load-
library-path".
Files ending in ".smv" will use smv-mode. This is very
similar to c-mode, except that it supports the smv syntax.
Further, in smv-mode, a pull-down menu option is provided
to run Vw on the current buffer.
Vw uses XEmacs via the gnuserv protocol. To edit a source
file, display it in the Source pane, and select the
"File|Open in emacs" item in the Source pane menu (not in
the main menu). The XEmacs "point" will be moved to the
currently highlighted line (for example, the line where a
syntax error occurred). After modifying the files, select
"File|Reopen" from the main menu. If you have any files in
XEmacs that are modified but not saved, you will be asked
if you want to save them. The modified sources will then
be reread into SMV. When you create a new SMV file with
the "File|New" menu item, SMV will also open the file in
XEmacs.
Note, SMV is only compatible with XEmacs version 21.1, and
not with FSF emacs.
SEE ALSO
smv(1),vl2smv(1)
K.L.McMillan,The SMV language
Kenneth L. McMillan, Symbolic Model Checking, Kluwer,
1993.
BUGS
See the release notes.
AUTHOR
Kenneth L. McMillan, Cadence Berkeley Labs
mcmillan@cadence.com
VW 25 Apr 2001 1