next up previous contents
Next: Path splitting Up: Proving liveness Previous: Proving liveness   Contents

Liveness lemmas

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.