VW(1) User Commands 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 edit- ing, and 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 on the command line, or in "#include" directives, with extension ".v", are interpreted as Syncho- nous 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 specific 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, select the "Open..." item from the "File" menu. If you modify any source files, you must 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 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. 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. If you are running vw in an emacs shell buffer, emacs will also display the file containing the name definition, and place a pointer "=>" on the line contining the definition. For this to work, you must have the line (load-library "smv-hooks") in your ~/.emacs file. 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 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 sig- nal. 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 depen- dencies 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. Assertions are normally named in the program source. An unnamed asser- tion 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. 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 vari- ables that are unconstrained in the abstraction). VERIFYING PROPERTIES To verify all of the properties in the program, select "Ver- ify" from the "Props" menu. To verify only the selected pro- perty, 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 verifica- tion 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 verif- ication 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. 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. 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 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 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". 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 pro- grams, 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 sug- gested 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. 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, con- sisting 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 sig- nal. This defines the "environment" 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 pul- ling 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 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 definition 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 show- ing 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 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. 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 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 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 win- dow. When you select a group by clicking on it, the proper- ties 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 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 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 properties in the group in the same model checking run. This means that the transition relation and reached state set will be com- puted only once for the group. To get this effect, select the option "check all properties together" in the options menu (under "Props:Options..."). 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 Last change: 23 Jan 1996 8