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

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

2003-01-07