The proof

Now we proceed to define the abstractions used to prove the cases of the two lemmas. As before, when proving lemma1 we use lemma2 and vice versa. Also as before, we free the results in the abstract model when verifying operands, and free the operands when verifying the results.

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 f to undefined except for f[a][b] since this is the only element of the table that matters to our particular case.

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 $\neq$ 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 i on the result bus pout are correct, in the case where execution unit j is returning a result, the ``a'' operand is a, the ``b'' operand is b and the f[a][b] (the correct result) is c. Since a, b and c are all of the same type, we have $3! = 6$ cases to prove:

    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 a, b, and c. The most difficult case should be the last one, since it has three different values of type WORD. In fact, if you select this property and look in the cone pane, you should observe that the values of type WORD are represented by two boolean variables (enough to encode the values 0, 1,and 2, plus an abstract value). In addition, because the index data types are reduced to only those values occurring in the property, we have only one reservation station in the cone. If we access any RS's other than zero, we'll get an undefined value. However, this should not affect the truth of our property, since it only tests returning results that derive from reservation station zero. The other results will, of course, be incorrect in the reduced model, but our property ignores them. You can validate this argument by selecting ``Prop|Verify pout.val//lemma2[0][0][2][1][0]''. The property verifies quite quickly, because there are only 18 state variables in the cone (it takes less than half a second on my machine).

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:

1. 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.
2. 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.
3. Symmetry. The large number of cases produced by the above two steps are reduced to a small finite number by considerations of symmetry.
4. 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.