Fairness

Now, open the new version. You should see several new properties in the properties pane: instances of live1a, live1b and live2. Select, for example, live1a[1][0][0]. This says that operands are always eventually forwarded from producer 0, via source register 0, to consumer 1. It should verify correctly.

On the other hand, try to verify live2[0][0], which states that results for reservation station 0 always eventually arrive when using execution unit 0. For this property you should get a counterexample, where the reservation station is loaded with an instruction, obtains both its operands, and then waits forever to be issued to an execution unit. Note that many reasons are possible for this. For example, we have not specified issue_choice, which indicates the reservation station chosen for issue to an execution unit. Thus it is possible that reservation 0 is never chosen (a failure of fairness of the arbiter). Or, it is possible that reservation station 0 is chosen, but never at a moment that there is an available execution unit. Or, it is possible that issue_eu, which chooses an execution unit never chooses an available, or that there is never an available unit because no execution unit ever terminates. Or, because we are using an abstraction where all execution units except for eu[0] are abstracted away (because of the default data type reduction), it is possible that issue_eu always choose a unit other than zero, and this unit, being abstracted away, always claims to be busy (in fact, this is the counterexample that I got).

For the moment, let's rule out all these possibilities by simply assuming that an instruction does not remain unissued forever with its operands ready. Later, when we actually implement a policy for issue_choice and issue_eu, we'll discharge this assumption. Here is one way to state this assumption:

  forall (i in TAG) {
    issue_fair[i] : assert G F (st_ready[i] -> st_issue[i]);
    assume issue_fair[i];
  }

That is, it is not possible that a reservation station remains ready and not issued. We define these terms as follows:

  forall(i in TAG) {
    st_ready[i], st_issue[i] : boolean;
    st_ready[i] := st[i].valid & st[i].opra.valid & st[i].oprb.valid & ~st[i].issued;
    st_issue[i] := issue_choice = i & exe_rdy;
  }

Now, add issue_fair[i] to the assumptions used to prove live2[i][j]. With this addition, try again to verify live2[0][0]. You should get another counterexample, this time where an instruction does get issued to execution unit 0, but the execution unit never completes. To correct this problem, let's add the assumption that execution units always eventually complete:

  forall(i in EU){
    eu_fair[i] : assert G (eu[i].valid -> F ~eu[i].valid);
    assume eu_fair[i];
  }

That is, we assume that if an execution unit becomes valid (contains an instruction), it eventually becomes invalid (completes). We'll have to discharge this assumption later when we fill in the details of the execution units and the completion arbitration. Add the assumption eu_fair[j] to those used to prove live2[i][j]. Now, try again to verify live2[0][0]. You should find the property true. Now try ``Prop|Verify all''. All the properties should be true, although the system will warn that there are unproved assumptions (the properties issue_fair and eu_fair).