Case splitting

Now, let's split our lemmas into cases, so that we only have to think about one possible path for data to follow from one refinement map to the other. We begin with the operand lemma.

Consider a result returning on the result bus. That result is the result value of a given reservation station i. It then (possibly) gets stored in a register j. Finally it gets read as an operand for reservation station k. This suggests a case split which will reduce the size of the verification problem to just two reservation stations and one register. For each operand arriving at reservation station k, we split cases based on the reservation station i that it came from (this is the ``tag'' of the operand) and the register j that it passed through (this is the source operand index, srca or srcb, that we store in the auxiliary state for just this purpose). We also want to split cases on the correct data value, since WORD is an undefined scalarset type. Thus, here is the case splitting declaration for the ``a'' operand:

  forall (i in TAG) forall (j in REG) forall (k in TAG) forall(c in WORD)
     subcase lemma1[i][j][c] 
     of st[k].opra.val//lemma1
     for st[k].opra.tag = i & aux[k].srca = j & aux[k].opra = c;

That is, we consider only the case where the tag (i.e. the producing reservation station) is i, and source register is j and the correct value is c. The ``b'' operand is similar.

For the result lemma (lemma2), we consider a pair of operands that start in some reservation station i and pass through execution unit j. Since i is a parameter of the lemma already, we are left with just j to split cases on (this is the value of the signal complete_eu). However, we now also have three data values to split cases on: the two operands a and b, and the result, c = f[a][b]. As before, this will reduce the data type WORD and the table f down to a tractable size. Thus, here is our case splitting declaration for lemma2:

  forall(i in TAG) forall(j in EU)
  forall(a in WORD) forall(b in WORD) forall(c in WORD)
     subcase lemma2[i][j][a][b][c]
     of pout.val//lemma2[i]
     for aux[i].opra = a & aux[i].oprb = b & f[a][b] = c
         &  complete_eu = j;

Finally, we have one last thing to prove, which is that the data output is correct according to the architectural model (layer arch). This is quite similar to the operand lemma. That is, every data output value was produced as a result by some instruction and then stored in the source register for the RD instruction. Therefore, when proving that data output values are correct, we will split cases on the producing reservation station (this is obtained from the tag of the source register) and the source register index. In addition, as before, we consider only the case where the correct value is some arbitrary constant c:

  forall (i in TAG) forall (j in REG) forall (k in TAG) forall(c in WORD)
     subcase arch[i][j][c]
     of dout//arch
     for srca = j & ir[j].tag = i & r[j] = c;