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
) 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

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

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

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

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.