Implementing the issue arbiter

Now we come to the problem of implementing an issue arbiter that guarantees the property issue_fair. That is, we want to choose issue_choice in such a way that every ready instruction is eventually issued. One way to do this is by using a rotating priority scheme. In this scheme, one requester (reservation station) is assigned highest priority. If this requester is rejected (i.e., requests but is not acknowledged), it retains the highest priority. Otherwise, priority rotates to the next requester. In this way, we can guarantee that, if a resource (execution unit) always eventually becomes available, then all requesters will eventually be served (or withdraw their request). Here is an implementation of the issue arbiter (we leave the choice nondeterministic in the case where the high priority requester is not requesting):

    issue_prio : TAG;

    if(st_ready[issue_prio])
      issue_choice := issue_prio;
    else issue_choice := {i : i in TAG};

    breaking(TAG)
       if(~(st_ready[issue_prio] & ~exe_rdy))
         next(issue_prio) := issue_prio + 1 mod TAGS;

Note that by incrementing issue_prio, we break the symmetry of the type TAG. This means we have to enclose the assignment within a breaking(TAG) declaration, so disable type checking of type TAG. Further, we now have to explicitly declare the number TAGS of reservation stations. So let's change the declaration of type TAG to the following:

  scalarset TAG 0..(TAGS-1);

Define TAGS to be some reasonable value (say 32). Similarly, set some reasonable number of execution units (say 4). Now, we need also to define a policy for choosing an available execution unit for issue. The simplest way to do this is to specify a nondeterministic choice among all the available (non-valid) execution units:

   issue_eu := {i ?? ~eu[i].valid : i in EU};

Now, remove the statement

  assume issue_fair[i];

and add instead:

   breaking(TAG) breaking(EU) forall(i in TAG)
     using
       st_ready//free, exe_rdy//free, eu//free
     prove issue_fair[i];

Note, the breaking statements are used so that we can use assignments in the proof that break they symmetry of these types. Note also that we free the input signals of the arbiter; the arbiter should satisfy the fairness property for all possible inputs.