VW(1)                                                                    VW(1)



[1mNAME[0m
       vw - viewer for smv

[1mSYNOPSIS[0m
       [1mvw [22m[file.[smv,v]]

[1mDESCRIPTION[0m
       This  is a graphical user interface for [4msmv(1).[24m  Provides source brows-
       ing, counterexample browsing, abstraction  editing,  proof  management,
       and spreadsheet-style simulation. 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 preprocessor much like
       the C preprocessor.  Files with extension ".v", are interpreted as Syn-
       chonous Verilog, and are translated to SMV by [4mvl2smv(1).[0m

       There are no command line switches, as in [4msmv(1).[24m  Any smv compile-time
       options, such as -D and -I should be put  in  the  file  "file.cflags".
       See  [4msmv(1)[24m  for definitions of these switches. This file may also con-
       tain global options that apply to all properties  to  be  verified.  If
       there is no "file.cflags", some default options are used (see [4msmv(1)[24m ).
       Model checking options that are generic, or specific to a  given  prop-
       erty, can be also be specified using vw.

       The  vw graphical interface consistes of a main menu bar, and a collec-
       tion of "panes", each of which can be brought into view by clicking its
       tab. These panes are described below.


[1mGETTING STARTED AND EXITING VW[0m
       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 key-
       board interrupt, it won't remember its state the next time you run it.


[1mTHE BROWSER PANE[0m
       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 children 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.


[1mTHE SOURCE PANE[0m
       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.


[1mBROWSING THE SOURCE[0m
       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  signal.  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.


[1mTHE PROPERTIES PANE[0m
       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. Assertions 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", "unverified  properties",  "Verified  properties"  or
       "Assumed  properties".  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.


[1mTHE CONE PANE[0m
       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  sig-
       nal 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 "combina-
       tional"  variables. You can choose to see the "Entire cone", "All Vari-
       ables", "State variables", or "Free variables" (the  latter  are  those
       variables that are unconstrained in the abstraction).


[1mVERIFYING PROPERTIES[0m
       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".


[1mTHE LOG PANE[0m
       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.


[1mTHE RESULTS PANE[0m
       The results pane shows the results of the most recent verification 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" property, as if it had been selected in the properties  pane.
       In  addition, if you click on a false property, a counterexample for it
       will appear in the trace pane.


[1mTHE USING PANE[0m
       When a property is selected for verification, the "using" pane displays
       a  list  of  all the temporal logic assertions that are used as assump-
       tions when proving the current property. For each property, it displays
       whether the property is assumed "up to t", "up to t - 1", or "always".


[1mTHE TRACE PANE[0m
       The  trace  view  displays counterexamples and simulation traces. It is
       essentially a spreadsheet, where the rows  represent  signals  and  the
       columns  represent  time.  Initially,  all  of  the signals in the cone
       appear in the trace pane. If there is a large number of signals, it  is
       sometimes  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 example, 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 left-
       most 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 configu-
       ration can be restored by using  "View|Restore  Trace  View...".   Note
       that this saves only the names of the signals, and not the traces them-
       selves, which may have changed when you later restore the trace view.

       Normally, SMV returns to a view of all the signals whenever 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  column  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).


[1mMODIFYING TRACES AND SIMULATION[0m
       You can treat a trace in the trace view window like a spreadsheet, mod-
       ifying some values, and then  recomputing  the  entire  trace  to
       reflect  these modifications. This allows vw to be used as an  interac-
       tive 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 possi-
       ble 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.


[1mLOADING AND SAVING TRACES[0m
       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".




[1mSELECTING PROPERTY SPECIFIC OPTIONS[0m
       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 [4msmv(1)[24m  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.


[1mEDITING AN ENVIRONMENT ABSTRACTION[0m
       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 "environ-
       ment" for verifying the given property. Normally these choices are made
       in  the  program source with the "using...prove" declaration.  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  "Abstrac-
       tion"  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 abstrac-
       tion 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  depen-
       dency  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 verifying 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 def-
       inition of foo in layer bar, since this would  be  circular  reasoning.
       Similarly, to cannot chose a defintion 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).


[1mABSTRACTION FILES[0m
       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 selection 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.


[1mSAVING AND RESTORING THE ABSTRACTION FILE[0m
       If you are editing the abstraction for a given  property  and  want  to
       save  it to disk, choose "File:Save abstraction". If you make a mistake
       and want to get back the saved version use "File:Restore  abstraction".
       Note,  however,  that running the model checker will cause the abstrac-
       tion to be saved, and any previously saved file will thus be  overwrit-
       ten.


[1mPROPERTY GROUPS[0m
       A  property  group  is  a collection of properties that behaves exactly
       like a single property from the point of view of the foregoing  discus-
       sion. You create and manage property groups using the "group view" win-
       dow. 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 abstrac-
       tion, you must first select it in the properties  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  properties  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 efficiency reasons,
       you may want to check all of the properties 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...").


[1mCONTROLLING VW FROM THE KEYBOARD[0m
       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 typing 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 vis-
       ible,  then press the "down arrow" key until "State variables" is high-
       lighted, then press Enter.


[1mINCREMENTAL SEARCH[0m
       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  signal 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.


[1mUSING VW WITH XEMACS[0m
       Vw  uses  the  XEmacs version 21.1 as its text editor. To use this fea-
       ture, you must have XEmacs installed on your system. 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, dis-
       play 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.


[1mSEE ALSO[0m
       [1msmv(1),[22mvl2smv(1)
       [1mK.[22mL.[1mMcMillan,[22mThe SMV language
       [1mKenneth L. McMillan, [4m[22mSymbolic[24m [4mModel[24m [4mChecking,[24m [1mKluwer, 1993.[0m



[1mBUGS[0m
       See the release notes.


[1mAUTHOR[0m
       Kenneth L. McMillan, Cadence Berkeley Labs
       mcmillan@cadence.com





VW                                25 Apr 2001                            VW(1)
