Uninterpreted functions

Suppose that instead of specifying the exact function of the ALU in our abstract model, we simply use a symbol f to denote this function. Suppose further that we use the same function symbol in our implementation, and we are able to prove a refinement relation between the two. It would then follow that the refinement holds for any concrete function we might want to plug in place of f.

To introduce a function f that takes two WORD arguments and produces a WORD result, we can write:

  function f(x : WORD, y : WORD) : WORD;

This defines the type of the function, but doesn't give the function's definition. In fact, we could have gotten almost the same effect by simply declaring f as a two-dimensional array, like this:

  forall (a in WORD) forall (b in WORD)
    f[a][b] : WORD;

We could think of this array as the lookup table of the function. In fact, this is what SMV does, internally. The only difference between these two declarations, other than syntax, is that arrays can change value over time, while functions cannot.

Now, to evaluate function f over two arguments opra and oprb, we can write:

  res := f(opra,oprb);

This is just as if we had declared f as an array, and written:

  res := f[opra][oprb];

The trick here is that, without a data type reduction for type WORD, the lookup table for f will be of astronomical size. However, by case splitting, we can consider only the case when the arguments are some fixed values, and the result of the function is some fixed value. By doing this, we then have to consider only one element of the table for f at a time. This is a good thing, but it requires that WORD be a symmetric type (a scalarset or an ordset), so that we can reduced the very large number of cases (here $2^{32}\times 2^{32}\times 2^{32}$) to a tractable number (for example, 6).

So now let's rewrite our example using an uninterpreted function symbol f for the ALU function. First, let's redefine type WORD to be a scalarset:

  scalarset WORD undefined;

We don't have to say what the range of the type is. Instead, we'll verify our design for any word size. Now, in the main module, let's define an uninterpreted function f:

  function f(x : WORD, y : WORD) : WORD;

Finally, we'll replace the ALU functions in both abstract model and implementation with function f. In the abstract model, change

   res := opra + oprab;

to

   res := f(opra,oprb);

In the implementation, change

  alu_output := stage1.opra + stage1.oprb;

to

  alu_output := f(stage1.opra,stage1.oprb);

Now that we've modeled our problem with an uninterpreted function, we need to do a little further case splitting, so that we only have to think about a few values of WORD at a time.

For the operand lemma, we'll split cases on the correct operand value. That is, we'll prove that the operands we obtain are correct when the correct value is some fixed number j:

  forall(i in REG) forall(j in WORD)
    subcase lemma1[i][j] of stage1.opra//lemma1
      for stage1.aux.srca = i & stage1.aux.opra = j;

(and similarly for oprb). For the results lemma, we want to consider only one entry in the lookup table for f at a time. We'll split our result refinement map (lemma2) into cases based on the values of the two operands, and the value of function f for those two particular values. Thus for example, we might verify that the alu_output signal is correct only in the particular case when opra = 0 and oprb = 1 and when f(0,1) = 2. Here is a suitable case splitting declaration:

  forall (a in WORD) forall(b in WORD) forall(c in WORD)
    subcase lemma2[a][b][c] of alu_output//lemma2
      for stage1.aux.opra = a
        & stage1.aux.oprb = b
        & f(a,b) = c;

Our using...prove declarations are exactly the same as before, except that they have added parameters for the additional case splits:

  forall(i in REG) forall(j in WORD)
    using res//free, alu_output//lemma2 prove stage1//lemma1[i][j];

  forall (a in WORD) forall(b in WORD) forall(c in WORD)
    using opra//free, oprb//free, stage1//lemma1
      prove alu_output//lemma2[a][b][c];

Now, open the new version. For alu_output//lemma2[a][b][c], there are six cases to prove:

alu_output//lemma2[0][0][0]
alu_output//lemma2[1][0][0]
alu_output//lemma2[2][0][0]
alu_output//lemma2[0][1][0]
alu_output//lemma2[1][1][0]
alu_output//lemma2[2][1][0]

That is, SMV generates enough cases so that we see all the possible equality relationships between a, b and c (in fact, you might notice the SMV generates one redundant case, since [1][0][0] represents the same equality relation as [2][0][0], but this is harmless). For lemma 1, we now have just one case each for opra and oprb, since there is only one parameter of type WORD.

Select property alu_output//lemma2[0][0][0] and look at the cone. You'll notice that only one element of the lookup table for f appears in the cone: f[0][0]. This is because 0 is the only specific valued in the reduced type WORD. (SMV automatically chose a reduction for us, including just those values that specifically appear in the property we're proving). Verify this property. It's not surprising that the verification is rather fast, since there are only 5 state variables.

Now select property alu_output//lemma2[2][1][0]. Notice that in this case we have nine cases of f[a][b] in the cone (all the combinations of a,b = 0,1,2). This is because SMV isn't smart enough to figure out that the only element that actually matters is f[2][1]. We could, if we wanted to, include a declaration to make the remaining values undefined:

  forall (a in WORD) forall(b in WORD) forall(c in WORD)
    using f//undefined, f[a][b] prove alu_output//lemma1[a][b][c];

This would reduce the number of state variables quite a bit, but it isn't really necessary. Even with the extraneous variables, the verification is quite fast, as you may observe.

Finally, select Prop|Verify All to verify the remaining cases. We have now verified our trivial pipeline design for an arbitrary number of registers, an arbitrary word size, and an arbitrary ALU function.