End-to-end verification

Now we'll consider a more complex (though still trivial) implementation with multiple stages of delay. The goal is to verify the end-to-end delivery of data by considering each stage in turn, specifying a refinement map for each stage. The refinement map for each stage drives the input of the next. Suppose we replace the above implementation with the following implementation that has three time units of delay:

  stage1, stage2 : struct{
    valid : boolean;
    idx : INDEX;
    data : BYTE;
  }

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

We'll include a refinement map for each intermediate delay stage, similar to the maps for the input and output:

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

When verifying the output of one stage, we can drive the output of the previous stage from the abstract model, via the refinement map, thus decomposing the verification of each stage into a separate problem. Open this version in vw and select, for example, the property out.data[0]//spec. That is, we want to verify the final output against the refinement map. Select the Cone page, and notice that to define the data outputs of the stage2, SMV has chosen the layer spec, rather that the implementation definition. The number of state bits remaining (51) is still larger than in the previous case, however, because spec doesn't give any definition of the signals valid and idx, hence these are still driven by the implementation.

If you select ``Prop|Verify out.data[0]//spec'', you'll observe that we can still quickly verify this property, even thought the number of state variables is larger. Nonetheless, we would like to make the verification of the last stage independent of the previous stages, to be sure we can still verify it if the previous stages are made more complex. We can do this by explicitly ``freeing'' the signals stage2.valid and stage2.idx, that is, allowing these signals to range over any possible values of their types. This is the most abstract possible definition of a signal, and is provided by a built-in layer called free. To tell SMV explicitly to use the free layer for these signals, we add the following declaration:

  using
    stage2.valid//free, stage2.idx//free
  prove
    out.data//spec;

Open this new version, and select property out.data[0]//spec. Note the the number of state bits (in the Cone page) is now 39, as in our original problem. In fact, if you select ``Prop|Verify out.data[0]//spec'' you will probably get a very fast answer, since SMV will notice that the verification problem you are trying to solve is isomorphic to that of the one-stage implementation we started with. This information was saved in a file for future use when that property was verified.

To verify stage2, in the same way, we need to make similar using...prove declaration, as follows:

  using stage1.valid//free, stage1.idx//free prove stage2.data//spec;

Note that we don't need a corresponding declaration for stage1, since the input signals inp.valid and inp.idx have been left undefined, and are thus free in any event. With this addition, chose ``Prop|Verify all'', and observe that all the properties are verified very quickly, since they are all isomorphic.