In reality, of course, we don't don't build hardware containing
uninterpreted functions. What we would like to do is to verify
the design for an arbitrary function `f`, and then ``plug in''
some specific definition of `f` (for example, `f` might
represent binary addition). We can declare an *interpretation*
for our function `f` as follows:

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

That is, `f` is a function that takes two operands of type
`WORD` and yields a `WORD`, and further, by definition,
`f(x,y) = x + y`. SMV gives us the option, in proving any
given property, to either use this interpretation of `f`,
or to leave `f` uninterpreted, as we did above.

For example, in our simple pipeline, we might like to split the proof
of correctness into two steps. First, we show that the ALU in our
pipeline implements the function `f` (using `f` as an
interpreted function). Then we show that the pipeline implements
its specification, leaving `f` uninterpreted, as above.
This allows us to completely separate the problems of correctness
of the pipeline design and correctness of the ALU. Reasoning
about the pipeline is simpler, because we can treat `WORD`
as a symmetric type.

Here's how we do that in practice. We would like `WORD`
to be a symmetric type, to simplify reasoning about the
pipeline. On the other hand, we want `WORD` to be a bit
vector type, since our machine operates on bit vectors.
Fortunately, SMV allows us to treat either scalars or bit
vectors as symmetric types, so let's declare `WORD` as follows:

scalarset WORD array 31..0 of boolean;

Now, here is the declaration of function `f`:

breaking(WORD) function f(x : WORD, y : WORD) : WORD := x + y;

We had to use the declaration `breaking(WORD)` because our
interpretation of `f` breaks the symmetry of type `WORD`.
This means that we if we are relying on the symmetry of `WORD` to
prove a property, we won't be able to use the interpretation of ` f`. Now, lets make a module that implements a ripple-carry binary
adder. Here is one possible version:

module adder32(x,y,z){ input x : WORD; input y : WORD; output z : WORD; carry : array 32..0 of boolean; carry[0] := 0; breaking(WORD){ forall(i = 0..31){ z[i] := x[i] ^ y[i] ^ carry[i]; carry[i+1] := (x[i] & y[i]) | (x[i] & carry[i]) | (y[i] & carry[i]); } } }

Notice the `breaking` definition that tells SMV we are going to do
something non-symmetric with type `WORD`. Now, let's use that module
in our implementation. We replace this:

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

alu : adder32(stage1.opra,stage1.oprb,alu_output);Now our implementation has a bit-level adder. First, let's show that this is equivalent to using function

layer alu_ok: alu_output := f(stage1.opra,stage1.oprb);To use this layer to prove our original specification of

alu_ok refines lemma2;To prove this specification of

breaking(WORD) using interpreted(f), stage1//free prove alu_output//alu_ok;The clause

Now, open
this version. For the
property `alu_output//lemma2[a][b][c]`, you'll notice that
we have the same six cases to prove as before. If you select one of these
cases, and look in the Cone pane, you'll see that layer `alu_ok`
has been used for `alu_output`. That is, SMV has used the function
`f` for the ALU instead of our ripple-carry adder. This is the only
available choice, since the ripple-carry adder breaks the symmetry
of `WORD`. Further, by default, function `f` has been left
uninterpreted. Thus, the verification of `alu_output//lemma2[a][b][c]`
is exactly the same as in the previous example.

On the other hand, we now also have to prove ` alu_output[31..0]//alu_ok`. That is, we must show that the ALU
actually implements function `f` at the bit level. If you select
one of these properties, you can observe in the cone pane that there
are up to 64 combinational variables (the ALU inputs) but no state
variables, since these are eliminated by the cone-of-influence
reduction. Since binary addition is easily handled by BDD's, we can
verify these properties in a very short time. If our ALU function
were, say, multiplication instead of addition, we would face much
greater difficulty. Matters would be somewhat simplified, however, by
the fact that we do not have to think about the pipeline when verifying
the ALU.

Try `Prop|Verify All` to check the proof. It should take just a few seconds.

In the rest of the tutorial, we will mostly use function symbols without interpretations. However, it should be understood that it is always possible to ``plug in'' interpretations for these functions without changing the high level proof, in the same manner that we have done here.