[Next] [Up] [Previous]

Refinement maps

As before, now that we have an abstract model and an implementation, we will write refinement maps that relate the two, and then break these into cases that are small enough problems to verify with model checking. Surprisingly, the refinement maps that we will use are almost identical to the ones we used for the simple pipeline. That is, we have one lemma that states that operands obtained by the reservation stations are correct, and one that states that results returning from the execution units are correct.

Also as before, to write these specifications, we will add some auxiliary state to the implementation, to remember what the correct values of the operands and results are. Each reservation station will have an auxiliary structure containing values for opra, oprb and res. In addition, we'll include the source register indices srca and srcb (recall that last time we used these values for case splitting):

  aux : array TAG of struct {
    opra, oprb, res : WORD;
    srca, srcb : REG;
  }

Now, when we store an instruction in a reservation station, we want to record the correct values from the abstract model into the auxiliary structure:

   if(~stallout & opin = ALU){
     next(aux[st_choice].opra) := opra;
     next(aux[st_choice].oprb) := oprb;
     next(aux[st_choice].res)  := res;
     next(aux[st_choice].srca) := srca;
     next(aux[st_choice].srcb) := srcb;
   }

Now that we've recorded the correct values, we can specify our refinement maps. For the operands (lemma1) we state that if a given RS holds a valid operand, its value must match the correct value. For the ``a'' operand, we have:

   forall(k in TAG)
     layer lemma1 :
      if(st[k].valid & st[k].opra.valid)
        st[k].opra.val := aux[k].opra;

The ``b'' operand is similar. Now, for the result lemma (lemma2) we state that, if a result is returning on the result bus, tagged for a given reservation station, then its value is the correct result for that reservation station:

   forall (i in TAG)
     layer lemma2[i] :
      if(pout.tag = i & pout.valid)
        pout.val := aux[i].res;