Note finally, that we have only verified our implementation of Tomasulo's algorithm for one execution. We could easily enough verify our design for some small finite number of units as well. However, with multiple execution units, we can't abstract away all the execution units except the one we're interest in. This is because one of these abstracted units might return an incorrect tag, which would reset the state of our reservation station prematurely. You can see observe this phenomenon by changing the declaration of the type EU to the following:
scalarset EU 0..7;
Thus, we now have 8 execution units. If you open this modified version, and try verifying all the properties, you should obtain a counterexample for lemma2, in which reservation station 0 issues an instruction to execution unit zero, but then some other execution unit (which is abstracted by SMV's default heuristics) returns an undefined value as its tag, causing the state of reservation station 0 to be corrupted.
We can fix this problem by forcing SMV not to abstract the control information in the other execution units (though the data can still be left abstract, since we don't care abut it). To see this, change the proof declaration for lemma2 to the following:
forall(i in TAG) forall(j in EU) forall(k 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],
eu[k].tag, eu[k].ready, eu[k].valid
prove pout//lemma2[i][j][a][b][c];
The only change here is that we have said, for all execution units k, to include the implementation definitions of tag, ready and valid. The overrides the default behavior, which is to abstract these to undefined. Now, open this modified version, and try verifying all the properties. This should succeed, but take about a minute, instead of the five seconds required for the one-EU version. The reason is that we have greatly increased the number of state variables. If you select property pout//lemma2[0][0][2][1][0], you'll notice that the control bits of all the execution units are present in the cone, and as a result, the number of state bits is increased to 32.
As we have observed, the problem with eight execution units is still within the realm that can be solved with BDD's. However, if we want to verify the design for an arbitrary number of execution units, we'll need to deal with the problem of interference, the subject of the next section.