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.