** Next:** Fairness
** Up:** Proving liveness
** Previous:** Path splitting
** Contents**

####

The circular compositional proof

Now, in order to prove that an operand eventually arrives at a consumer
reservation station, we have to assume that the producer reservation
station eventually yields a result. Similarly, to prove the result of
a reservation station is eventually produced, we must assume that its
operands eventually arrive.

While this argument is circular on its face, we can eliminate the
circularity by introducing a time delay. Thus, to prove that operands
are live at time , we assume that results are live up to time
. This is sufficient, since if the consumer reservation station
is valid at time , the producer reservation must have been valid at
some time or earlier (that is, the producer instruction must
have arrived at an earlier time than the consumer instruction). In
essence, we show that an operand of an instruction must eventually
arrive assuming that all instructions arriving at earlier times
eventually terminate.

To implement this argument, use the following declarations:

forall (i in TAG) forall(j in TAG) forall(k in REG)
using pout//free, (live2[j]) prove live1a[i][j][k], live1b[i][j][k];
forall (i in TAG) forall(j in EU)
using opra//free, oprb//free, live1a[i], live1b[i], prove live2[i][j];

That is, we assume that the producer reservation station `j`
is live up to when proving the operands eventually arrive
at the consumer. The time delay is indicated by putting the
assumption `live2[j]` in parentheses. Then we can
assume that operands are live up to time when proving results
are live up to . SMV will detect the circularity, but notice
that it is broken by the time delay.
Note that, as in the refinement proof, we free the result bus
when verifying the operands and free the operands when verifying
the results. This breaks the system into two separate parts for
verification.

** Next:** Fairness
** Up:** Proving liveness
** Previous:** Path splitting
** Contents**
2003-01-07