A very simple example

Now, let's look at a trivial example of this. Let's return to our very simple example of transmitting a sequence of bytes. 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.

Note that our specification (layer spec) says that at all times the output value must be equal to the element of array bytes indicated by the index value out.idx. We would like to break this specification into cases and consider only one index value at a time. To do this, we add the following declaration:

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

In this case, the property we are splitting into cases is out.data//spec, the assignment to out.data in layer spec. The resulting cases are out.data//spec_case[i]. Note, however, that in the subcase declaration, we only give a layer name for the new cases, since the signal name is redundant. This declaration is exactly as if we had written

  forall (i in INDEX)
    layer spec_case[i]:
      if (out.idx = i)
        out.data := bytes[out.idx];

except that SMV recognizes that if we prove out.data//spec_case[i] for all i, we don't have to prove out.data//spec. Run this example, and look in the properties pane. You'll see that out.data//spec does not appear, but instead we have out.data//spec_case[0]. Note that only the case i = 0 appears, since INDEX is a scalarset type, and SMV knows that all the other cases are symmetric to this one. Now look in the cone pane. You'll notice that all of the elements of the array bytes are in the cone. This is because the definition of inp.data in layer spec references all of them. However, all of them except element 0 are in the undefined layer. This is a heuristic used by SMV: if a property references some specific value or values of a given scalarset type, then only the corresponding elements of arrays over that type are used. The rest are given the undefined value. You might try clicking on element bytes[1] and choosing Abstraction|Explain Layer to get an explanation of why this signal was left undefined. You can, of course, override this heuristic by explicitly specifying a layer for the other elements. In this case, however, the heuristic works, since property out.data//spec_case[0] verifies correctly.