Our problem in verifying Tomasulo's algorithm with an arbitrary number of execution units is that we are forced consider only one execution unit at a time, in order to obtain a finite-state verification problem. Thus, we consider the correctness only of the results of one particular execution unit. When we perform this verification, the other execution units are abstracted to an undefined value Thus, although we are not concerned with the correctness of the data values they produce, they may still upset the control state in the given reservation station by returning spurious tags.

To rule out this possibility, we add a non-interference lemma. This states that while a reservation station is expecting a result from a given execution unit, no other unit returns a result for that particular RS. In general, such a lemma is needed whenever the state of one system component might be corrupted by a spurious message from other components that have been abstracted away.

In order to state the condition that a given reservation station does not receive an unexpected result, we first have to add some auxiliary state information to tell us which execution unit the reservation station is actually expecting a result from. To do this, we add an additional field to the auxiliary state array:

forall (i in TAG) aux[i].eu : TAG;Now, each time that a given reservation station issues an instruction to an execution unit, we record the index of that execution unit in the auxiliary state:

if(exe_valid)next(aux[issue_choice].eu) := issue_eu;

We can now state the non-interference lemma as follows:

lemma3 : assert G (pout.valid -> (complete_eu = aux[pout.tag].eu));

That is, `lemma3` states that, at all times, if a result is returning
on the `pout` bus, with a given tag `pout.tag`, then the unit
returning the result (`complete_eu`) must be the unit that the
indicated reservation station is waiting for (`aux[pout.tag].eu`).

Now, lets see if we can prove `lemma3`. The first thing we'll have
to do is to break the lemma into cases, so we only have to consider
one reservation station and one execution unit. So let's add the
following case splitting declaration:

forall(i in TAG) forall(j in EU) subcase lemma3[i][j] of lemma3 for pout.tag = i & complete_eu = j;That is, we only consider the case where the returning result is for reservation station

forall(i in TAG) forall(j in EU) using (lemma3) prove lemma3[i][j];The parentheses around

Now that we've proved that other executions can't interfere, let's return
to the proof of `lemma2` (correctness of returning results). We want
to prove that a result coming back on the result bus is correct, *assuming*
that no previous interference has occurred. To do this, add `(lemma3)`
to the assumptions used to prove `lemma2`. You should get a declaration
like the following:

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], (lemma3) prove pout//lemma2[i][j][a][b][c];

Notice that we only assume the non-interference lemma up to
time when proving `lemma2` up to time . In fact,
SMV won't allow us to use `lemma3` up to time . This
is because `lemma2` is a refinement map. Thus, we might well
choose to use it use it when proving `lemma3`, which would result in
a circularity. Fortunately, the weaker assumption is sufficient to
prove the lemma. To confirm this, open
the new version, and choose
``Prop|Verify all''.

With the addition of a non-interference lemma, we have now proved that our implementation of Tomasulo's algorithm works for any word size, any ALU function, any number of registers, any number of reservation stations, and any number of execution units.