Modeling, specifying and verifying

We will start with some very simple examples, to illustrate the process of entering a model, specifying properties, and running SMV to verifying them. You can enter the examples yourself, using a text editor (and thus become acquainted with SMV's response to syntax errors). Or, if you are reading this tutorial on-line, you can follow the hyperlinks to the corresponding files.

Consider, for example, the following description of a very simple combinational circuit, with some assertions added. This example is written in SMV's native language. Use a text editor to enter the following program into a file called ``prio.smv''.

module main(req1,req2,ack1,ack2)
{
  input req1,req2 : boolean;
  output ack1,ack2 : boolean;

  ack1 := req1;
  ack2 := req2 & ~req1;

  mutex : assert ~(ack1 & ack2);
  serve : assert (req1 | req2) -> (ack1 | ack2);
  waste1 : assert ack1 -> req1;
  waste2 : assert ack2 -> req2;
}

This example shows most of the basic elements of an SMV module. The module has four parameters, req1, req2, ack1 and ack2, of which the former two are inputs, and the latter two outputs. It contains:

• Type declarations. In this case the signals req1, req2, ack1 and ack2 are declared to be of type boolean.
• Signal assignments. These give logic functions for outputs ack1 and ack2 in terms of inputs req1 and req2.
• Assertions. These are properties to be proved.

The program models a (highly trivial) two bit priority-based arbiter, which could be implemented with a two-gate circuit. The assert statements specify a number of properties that we would like to prove about this circuit. For example, the property called mutex says that outputs ack1 and ack2 are not true at the same time. Note that & stands for logical ``and'' while ~ stands for logical ``not''. The property serve says that if either input req1 or req2 is true, then one of the two outputs ack1 or ack2 is true. Note that | stands for logical ``or'', while -> stands for ``implies''. Logically, a -> b is equivalent to ~a | b, and can be read ``a implies b'' or ``if a then b''.

We would like to verify these specifications formally, that is, for all possible input patterns (of which in this case there are only four). To do this under Unix, enter the following shell command:

vw prio.smv

On a PC under Windows, double-click the icon for the file ``prio.smv''. This will start the SMV viewer, called ``vw'', with the file ``prio.smv''. This interface has a number of tabbed pages, which can be accessed by clicking an the appropriate tab. When you start the interface, you see the browser, which is a tree representation of all the signals and assertions in your source file, and the source page, which shows the source file. If you made a syntax error in the source file, this error will be pointed out on the source page. Correct the error, and then choose ``Reopen'' from the ``File'' menu.

If you have no syntax errors, expand top level in the browser by double-clicking it, or by clicking the + icon. The + indicates that top level has children which are not currently visible. You should see under top level the names of all the signals and properties in your source file. Since none of these has children, they will not be marked with a +. Select one of these, and notice the highlight in the source page moves to the location in the program where that signal or property is declared. Select the signal ack2, and then in the source page, select ``Where assigned'' in the ``Show'' menu. The source line where ack2 is assigned will now be highlighted.

Now select ``Verify all'' from the ``Prop'' menu. SMV verifies the four properties in our program. The results page now shows the results of this verification run. In this case, all the properties are true.

Now let's modify the design so that one of the specifications is false. For example, change the line

    ack1 := req1;

to

    ack1 := req1 & ~req2;

Save the modified text file and choose ``Reopen'' from the ``File'' menu (or, if you are on-line, just click here to save typing). Then select ``Prop|Verify all'' again. Notice that this time the property serve is false. Also note, not all of the properties appear in the results pane. This is because SMV stops when it reaches the first property that is false. Thus, not all the properties were checked.

When a property is false, SMV produces a counterexample that shows a case when it doesn't hold. To see the counterexample for serve, select it in the results page by clicking on it. The trace page will appear, showing a counterexample - a truth assignment to all the signals that shows that our property is false. The counterexample shows the case when both inputs are true and both outputs are false.

The verifier keeps track of which properties have been verified since the most recent source file change. You can see which properties have been verified thus far, by selecting the properties page. Currently only mutex is verified. To verify waste1, for example, click on it in the properties page, and then choose ``Verify waste1'' from the ``Prop'' menu. Notice that only the property you select is verified in this case. The name of the property that is currently selected appears at the bottom of the window.