** Next:** The circular compositional proof
** Up:** Proving liveness
** Previous:** Liveness lemmas
** Contents**

####

Path splitting

Now we consider the problem of proving the operand liveness lemma.
As in the refinement proof, we observe that every operand consumed
by a given reservation station `i` was produced by some
reservation station `j`and stored in some source register `k`.
If we split cases on the producer reservation station and the
source register, we can show that the operand eventually arrives
in any one case, using just two reservation stations and one register
in the proof. Thus, add the following case splitting declaration for
the `opra` operand:

forall(i in TAG) forall(j in TAG) forall(k in REG)
subcase live1a[i][j][k] of live1a[i]
for st[i].opra.tag = j & aux[i].srca = k;

Recall that `st[i].opra.tag` is the producer reservation
station for the `opra` operand of reservation
station `i`, and `aux[i].srca` is the source register of
the `opra` operand, which we previously recorded in an
auxiliary variable. Thus, the subcase `live1a[i][j][k]` states
that (at all times), if reservation station `rs[i]` is holding
an instruction, whose `opra` operand is to be produced by
`rs[j]`, and stored in source register `ir[k]`, then
eventually the `opra` operand will become valid.
Note that in the refinement proof, we also had to split cases on the
data value. This is unnecessary in the liveness proof, however, since
liveness does not depend on data. Note, also that we will have to
assume that the producer reservation station eventually produces a
valid result. However, this is allowed by the circular compositional
rule, as we will see in the next section.

Now, for the results liveness lemma, we would like to prove that
if a reservation station holds an instruction, it will eventually
terminate. As before, we would like to split cases on the execution
unit that produces the result, so that we can deal with an arbitrary
number of execution units. This presents a slight problem, however,
since at the time the reservation station becomes valid, the execution
unit has not yet been chosen. In order to split cases, we therefore need
to refer to a future value of a variable, in particular, the value of
the execution unit choice at the time the instruction is issued. Fortunately,
we can do this using a temporal logic operator.

The temporal logic formula `p when q` is true at a given time
if `p` holds at the first occasion when `q` holds (and
is taken to be true if `q` never holds). It is
simply an abbreviation for ` ( q U (q & p))`. SMV recognizes
that at any given time, for any given variable `v`,

(v = i) when q

must be true for some value of `i` in the range of `v`.
This allows us to split cases on a future value of a variable instead
of the current. In this case, we can split the results lemma into cases
based on the the future choice of execution unit in the following way:
forall(i in TAG) forall(j in EU)
subcase live2[i][j] of live2[i]
for (aux[i].eu = j) when st[i].issued;

That is, we split cases on the value of the variable `aux[i].eu`
(the auxiliary variable that records execution unit choice) when
the instruction is issued.

** Next:** The circular compositional proof
** Up:** Proving liveness
** Previous:** Liveness lemmas
** Contents**
2003-01-07