Here is the proof for the operand lemma `lemma1` and
the data output (both of these assume `lemma2`):

forall (i in TAG) forall (j in REG) forall (k in TAG) forall(c in WORD) using res//free, pout//free, pout.val//lemma2[i] prove st[k]//lemma1[i][j][c], dout//arch[i][j][c];

Notice the we also freed the signals in the `pout` bus (other than
the value itself, which is given by `lemma2`), so that none of the
execution unit logic appears in the cone.

For the results lemma (`lemma2`), we take a similar tack: we use
`lemma2` for the operands, and otherwise free them in order
to eliminate the operand fetch logic from the cone:

forall(i in TAG) forall(j in EU) forall(a in WORD) forall(b in WORD) forall(c in WORD) using opra//free, oprb//free, st[i]//lemma1, f//undefined, f[a][b] prove lemma2[i][j][a][b][c];Notice we've set all the elements of the lookup table for

Now, open
the file. For `st[k].opra.val//lemma1[i][j][c]`, the
``a'' operand correctness lemma, you'll notice we have
two cases to prove:

st[0].opra.val//lemma1[0][0][0] st[1].opra.val//lemma1[0][0][0]

This is because both `i` (the producer RS) and `k` (the
consumer RS) are both of type `TAG`. Thus SMV must verify one
case where `i = k` and one case where `i k`. All the
other cases are equivalent to one of these by permuting values of
type `TAG`. Now, select property `st[1].opra.val//lemma1[0][0][0]`
(this is the more interesting of the two cases, since it involves two
reservation stations). Now, look in the Cone pane. You should observe that
all of the state variables of type `TAG` (such as `st[1].opra.tag`)
require two bits to encode them. This is because the type `TAG` has
been reduced to three values: 0, 1, and an abstract value representing
all the other tags. On the other hand, register indices (such as `srca`)
have been reduced to just two values, and hence are represented
by a single boolean value. These reductions were made by default,
because we didn't specify data type reductions for the undefined
scalarsets.

Notice also that we have freed signals in such a way as to cut off any
connection to the execution units in the abstract model and the
implementation. Thus, for example, the function `f` does not
appear in the cone. Finally, as a result of the data type reductions,
we have only register zero and RS's zero and one in the
Cone. Accesses to any other elements of these arrays will yield the
undefined value. The result of all these reductions is that the
cone contains only 25 state bits. Try verifying the property. Because
of the small number of state bits, it verifies on my machine in
a little under one second.

Now let's consider the results lemma (`lemma2`). This appears
as a collection of cases of the form:

pout.val//lemma2[i][j][a][b][c]which states that results for RS

pout.val//lemma2[0][0][0][0][0] pout.val//lemma2[0][0][0][1][0] pout.val//lemma2[0][0][1][0][0] pout.val//lemma2[0][0][1][1][0] pout.val//lemma2[0][0][2][0][0] pout.val//lemma2[0][0][2][1][0]This is enough to represent all the possible equality relationships between

Now choose ``Prop|Verify All'' to verify the remaining cases. It should take on the order of five seconds to do this. We have verified an out-of-order execution unit with an arbitrary number of registers and reservation stations, an arbitrary size data word and an arbitrary function. The basic strategy we used to do this was the same as for the simpler pipelined unit:

**Refinement maps and auxiliary state**. We broke the problem into two parts, by writing refinement maps that specify the correct values for the operands and results obtained in the implementation. To do this, the correct values are obtained from the abstract model, and stored in auxiliary state.**Path splitting**. We broke the large data structures (the register file and RS array) down into just a few components by splitting cases on the path taken by a data item from one refinement map to another.**Symmetry**. The large number of cases produced by the above two steps are reduced to a small finite number by considerations of symmetry.**Data type reductions**. After case splitting, we can reduce the large (or infinite) types, such as data words, to small finite types by grouping all the irrelevant values into a single abstract value. A special case of this is the uninterpreted function abstraction, in which we use a large table to represent and arbitrary function, but then split cases in such a way that we use only one element of the table for each case, after the data type reduction.

As a result of this strategy, the problem has been reduced to 11 rather small finite-state lemmas.