To begin with, let's take our implementation from the previous section and add two liveness lemmas. The first states (in temporal logic) that if a given reservation station holds a valid instruction, then its operands (opra or oprb) are eventually valid. Here is the lemma for opra:
forall (i in TAG)
live1a[i] : assert G (st[i].valid -> F st[i].opra.valid);
In other words, at all times, if rs[i] is valid, then
eventually the opra operand of rs[i] is valid.
Write a similar lemma for the oprb operand.
Now, for the result liveness, lemma, we have:
forall (i in TAG)
live2[i] : assert G (st[i].valid -> F ~st[i].valid);
That is, if rs[i] has a valid instruction, then eventually
the instruction completes, resulting in rs[i] being invalid.
Note, we could have stated that eventually the result bus has a
valid result with tag pout.tag = i. The two are equivalent,
since the reservation station goes to the invalid state if and only
if a corresponding result returns on the bus.