A very simple example

Let's return to our very simple example of transmitting a sequence of bytes (section 4.6.1). For reference, here is the specification again:

scalarset BIT 0..7;
scalarset INDEX 0..31;
typedef BYTE array BIT of boolean;

module main(){

  /* the abstract model */
        
  bytes : array INDEX of BYTE;
  next(bytes) := bytes;  

  /* the input and output signals */

  inp, out : struct{
    valid : boolean;
    idx : INDEX;
    data : BYTE;
  }

  /* the refinement maps */

  layer spec: {
    if(inp.valid) inp.data := bytes[inp.idx];
    if(out.valid) out.data := bytes[out.idx];
  }

And let's use our original very trivial implementation:

  init(out.valid) := 0;
  next(out) := inp;
}

That is, the output is just the input delayed by one time unit.

As before, let's break the specification up into cases, one for each index value:

  forall (i in INDEX)
    subcase spec_case[i] of out.data//spec for out.idx = i;

If you run this example, and look in the cone pane, you'll see that there are five state variables in the cone for both inp.idx and out.idx. This is expected, since five bits are needed to encode 32 values. However, notice that for case i, if the index value at the output is not equal to i, we don't care what the output is. Our property spec_case[i] only specifies the output at those times when out.idx = i. We can therefore group all of the index values not equal to i into a class, represented by a single abstract value (NaN), and expect that the specification might still be true. To do this, add the following declaration:

  forall (i in INDEX)
    using INDEX->{i} prove out.data//spec_case[i];

This tells SMV to reduce the data type INDEX to an abstract type consisting of just the value i and NaN (note, we don't specify NaN explicitly). Now, open the new version, and observe the cone. You'll notice the state variables inp.idx and out.idx now require only one boolean variable each to encode them, since their type has been reduced to two values. Now try verifying the property out.data//spec_case[0]. The result is true, since the values we reduced to the abstract value don't actually matter for the particular case of the specification we are verifying.

Now, let's suppose that we don't know in advance what the size of the array of bytes will be. Using data type reductions, we can prove the correctness of our implementation for any size array (including an infinite array). To do this, change the declaration

scalarset INDEX 0..31;

to the following:

scalarset INDEX undefined;

This tells SMV that INDEX is a symmetric type, but doesn't say exactly what the values in the type are. In such a case, SMV must have a data type reduction for INDEX to prove any properties, because it can only verify properties of finite state systems. Now run the new version. You'll notice that the result is exactly the same as in the previous case. One boolean variable is used to encode values of type INDEX, and the specification is found to be true. In fact, in the previous case, SMV didn't in any way use the fact that type INDEX was declared to have the specific range 0..31. Thus it's not surprising that when we remove this information the result is the same. By using finite state verification techniques, we have proved a property of a system with an infinite number of states (and an infinite number of systems with finite state spaces).

One might ask what would happen if, using a scalarset of undefined range, we omitted the data type reduction. Wouldn't that give us an infinite state verification problem? Try removing the declaration

  forall (i in INDEX)
    using INDEX->{i} prove out.data//spec_case[i];

from the problem and run the resulting file. You'll observe that nothing has changed from the previous case. Since SMV can't handle undefined scalarsets without a data type reduction, it guesses a reduction. It simply includes in the reduced type all the specific values of the given type that appear in the property. In this case, there is only one, the index i.