Abstract counterexamples

Verification runs that succeed are not generally very interesting. To convince yourself that the above proof strategy actually works, you might what to try introducing a bug into the implementation to see what happens. For example, let's remove the bypass logic from the operand fetch to see what happens. Replace the following code:

          /* fetch the a operand (with bypass) */
          
          if(pout.valid & ir[srca].resvd & pout.tag = ir[srca].tag){
            next(st[st_choice].opra.valid) := 1;
            next(st[st_choice].opra.tag) := ir[srca].tag;
            next(st[st_choice].opra.val) := pout.val;
          } else {
            next(st[st_choice].opra.valid) := ~ir[srca].resvd;
            next(st[st_choice].opra.tag) := ir[srca].tag;
            next(st[st_choice].opra.val) := ir[srca].val;
          }

with this:

          /* fetch the a operand (without bypass) */
          
          next(st[st_choice].opra.valid) := ~ir[srca].resvd;
          next(st[st_choice].opra.tag) := ir[srca].tag;
          next(st[st_choice].opra.val) := ir[srca].val;

Now, open the modified version and select ``Prop|Verify All''. You should get a counterexample for property

  st[0].opra.val//lemma1[1][0][0]

This is what happens in the counterexample. At step 1, an instruction with destination register 0, and result 0 is loaded into RS 0. At step 2 this is issued to an execution unit, and at step 3, the result returns on the result bus (pout.val is true). At the same time, a new instruction with ``a'' source register 0 is store in RS 1. However, because we have removed the bypass path, this instruction doesn't notice that its operand is currently returning on the result bus. Thus, it gets a tag 0 instead of a value for its ``a'' operand. Now, in step 4, a new instruction is loaded into RS 0, again with destination 0, but this time with some value other than zero as its result. Notice the the value of res (the abstract model result) at step 4 is NaN. In the reduced model, this represents any value other than zero. Then in step 5, this result returns on the result bus, with tag 0, and thus gets forwarded to RS 1, which is waiting for tag 0. Unfortunately, RS 1 is expecting a value of zero (see aux[0].opra, since it is really waiting for the result of an earlier instruction with tag 0. Thus our property is violated at step 6: the expected operand was zero, but the actual obtained operand (st[1].opra.val) is non-zero (represented by NaN). Even though the counterexample is abstract (i.e., it contains the abstract value NaN), it represents a class of real counterexamples (where, for example, the value 1 is obtained instead of 0).

In fact, the counterexample is abstract in another way. Notice that at step 5, a result returns on the the result bus pout.valid is true, even though the reservation station (st[0]) is not yet in the issued state. This is because the result bus is being driven by the refinement map lemma2 rather than by the real execution unit. Our refinement map didn't specify that a result would not return from an execution unit before it was issued. Interestingly, our design for the reservation stations and register file is sufficiently robust that a result arriving early in this way does not cause us to obtain correct operands output incorrect values. Thus, we are able to verify the implementation with rather ``loose'' refinement maps. This is a case of a more general phenomenon: the more robust the individual components of a design are, the simpler are the refinement maps.