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 $t$, we assume that results are live up to time $t-1$. This is sufficient, since if the consumer reservation station is valid at time $t$, the producer reservation must have been valid at some time $t-1$ 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 $t-1$ 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 $t$ when proving results are live up to $t$. 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.