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 jand 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.