A simple example

To see how we can use induction in practice, let's return to our example of transmitting an array of bytes. This time, however, we will assume that the bytes are in an infinite sequence. They are received at the input in the order byte[0], byte[1], byte[2], ... and they must be transmitted to the output in that order.

To begin with, let's define our types:

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

ordset INDEX 0..;

Note that we defined INDEX as an ordset type, so we can prove properties by induction over indices.

We begin with the original refinement specification. As in section 4.2.3, we encapsulate it in a module, so we can reuse it for both input and output:

module byte_intf(bytes){

  bytes : array INDEX of BYTE;
  
  valid : boolean;
  idx : INDEX;
  data : BYTE;
  
  layer spec: 
    if(valid) data := bytes[idx];
}

To specify ordering we simply introduce a counter cnt that counts the number of bytes received thus far. If there is valid data at the interface, we specify that the index of that data is equal to cnt. Thus, add the following declarations to module byte_intf:

  cnt : INDEX;

  init(cnt) := 0;
  if(valid) next(cnt)  := cnt + 1;

  ordered: assert G (valid -> idx = cnt);

Note, we can include temporal properties, like the above property ordered inside modules. Thus, for each instance of the interface definition, we'll get one instance of this property. As our first implementation, we'll just use the trivial implementation that delays the input by one clock cycle. Here's what the main module looks like:

module main(bytes,inp,out){
  bytes : array INDEX of BYTE;
  input  inp : byte_intf(bytes);
  output out : byte_intf(bytes);
  
  /* the abstract model */
        
  next(bytes) := bytes;  

  /* the implementation */

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

To prove the correctness of the data output (with respect to the refinement specification), we use the same proof as before - we split into cases based on the index of the output:

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

Note that anything that can be done with a scalarset can also be done with an ordset.

So much for the data correctness - the interesting part is the correct ordering. For the proof of the ordering property, we're going to use induction over the value of the counter cnt. The intuition here is that, if the output index equals the counter when the counter is i, then at the next valid output the counter and index will both be one greater, and hence they will be equal for cnt = i + 1. This assumes, of course, that the input values are ordered correctly. To verify this, we must first break the output ordering property into cases based on the value of cnt:

  forall(i in INDEX)
    subcase ord_case[i] of out.ordered for out.cnt = i;

Then, we prove case i using case i-1 and the input ordering property. We leave inp.ordering as an assumption:

  forall(i in INDEX){
    using ord_case[i-1], inp.ordered prove ord_case[i];
    assume inp.ordered;
  }

Now, run this example, and observe the properties pane. You'll notice that we now have two cases of the property out.data//spec_case[i] to prove: i = 0, 2. In fact, these two cases are isomorphic, but since INDEX is defined as an ordset rather than a scalarset, SMV's type checking rules don't guarantee this. Thus, SMV will effectively prove the same property twice. Fortunately, each case takes only a fraction of a second.

Now observe that we also have two cases of ord_case[i] to prove. Select, for example, property ord_case[2] from the properties pane and observe the cone. You'll notice that each value of type INDEX requires two boolean variables to encode it. This is because there are four values in the reduced type: i-1, i and two abstract values to represent the ranges [0..i-1) and (i..infinity). Notice also that there are no data values in the cone, since the indices do not depend on the data. Thus, we have effectively separated the problem of correct ordering from correct delivery of data.

Now, try Prop|Verify all. All the cases should be verified in less than a second.

A note: for ordsets, a data type reduction may be specified, in lieu of SMV's default. The general form of the data type reduction for ordset types is:

   TYPE -> { min..min+a,  i-b..i+c,  max-d..max};

where min is the minimum value of TYPE, i is the induction parameter, and max is the maximum value of TYPE. Thus, SMV allows us to use any finite number of values around the induction parameter i and the extremal values. In this case, the number of cases that need to proved will be larger, however.