Up to now, we've proved that our implementation of Tomasulo's algorithm is a refinement of an abstract model (in this case a sequential implementation of the same instruction set). However, we should note that a circuit that simply asserted the stall signal at every time unit would also satisfy this specification. Thus, we have shown that every behavior of the implementation is correct, in the sense that no bad outputs are produced, but we haven't shown that the circuit necessarily does any actual work. To do this, we also need to prove a liveness property.
The most obvious specification for liveness of the implementation is that it always eventually does not stall. We will begin, however, by proving something stronger: that every instruction eventually completes. Notice that this is a sufficient but not necessary condition for liveness. That is, if an instruction's result is never used as the source operand of a later instruction, then that instruction's failure to terminate would not cause any future stalls of the machine. However, we would also like to make sure that no reservation station is permanently lost as a resource, even if its result is never needed. Thus, we will prove that whenever a reservation station is full, it eventually becomes empty.
The proof of liveness follows the same basic lines as the refinement proof. That is, we break the liveness problem into two lemmas: one for operands, and one for results. The first lemma states that the operands of any given valid reservation station are always eventually valid. The second lemma states that a result for a given valid reservation station always eventually returns. As before, we construct a circular compositional proof, using operand liveness to prove result liveness, and vice versa. We will also use the same path splitting approach and data type reductions as in the refinement proof.
The main difference from the refinement proof is that we will need to fill in more detail about the resource allocation policies in order for the implementation liveness to be guaranteed. Up to now, we have left a number of choices completely nondeterministic, for example, the choice of which reservation station issue to an execution unit. However, in order to ensure that every instruction eventually executes, we will require that this choice be made in a fair way. Also, we will have to guarantee that execution units always eventually finish. On the other hand, liveness does not depend in this case on data values, thus we will find that the data path logic does not enter into the proof.