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.

- Liveness lemmas
- Path splitting
- The circular compositional proof
- Fairness
- Implementing the issue arbiter