Implementation

In the implementation, we have two main data structures: the register file and the array of reservation stations. We define these as follows:

  ir : array REG of
    struct{
      resvd : boolean;
      tag : TAG;
      val : WORD;
    }
  
  st : array TAG of
    struct{
      valid : boolean;
      opra, oprb : st_opr;
      dst : REG;
      issued : boolean;
    }

Each register has a bit resvd, which is true when it is holding a tag (we say it is ``reserved'') and false when it is holding a value. Each reservation station has a bit valid to indicate is is holding a valid instruction, a bit issued to indicate its instruction has been issued to an execution unit, and two operand fields, opra and oprb. The operand type is defined as follows:

typedef st_opr struct{
  valid : boolean;
  tag : TAG;
  val : WORD;
}

Each operand has a bit valid. When valid is true, it holds a value, otherwise it holds a tag. The type TAG is an index into the reservation station array, and is declared as follows:

  scalarset TAG undefined;

The result bus is called pout and is declared as follows:

  pout : struct{
    valid : boolean;
    tag : TAG;
    val : WORD;
  }

We also need arbitrary choices for the reservation station to store a new instruction into, and the reservation to issue to an execution unit at any given time:

  st_choice : TAG;
  issue_choice : TAG;

Now, we begin with the implementation behavior. Initially, all the reservation stations are empty, and all the registers are unreserved:

  forall(i in TAG)
    init(st[i].valid) := 0;
  forall(i in REG)
    init(ir[i].resvd) := 0;

There are three basic operations that occur on the register file and reservation stations:

• incoming instructions stored in a RS,
• instruction issue to execution unit and
• instruction completion (writeback to register file).

These three operations appear in the following default...in structure:

  default
    {...instruction completion logic...}
  in default
    {...incoming instruction logic...}
  in
    {...instruction issue logic...}

This is done to specify the relative priority of the three operations in case they write to the same register at the same time. However, in principle they shouldn't interfere with each-other, except in one case where we need a register bypass.

Now, here is the implementation of instruction completion:

    if(pout.valid){
      forall(i in REG)
        if(ir[i].resvd & ir[i].tag = pout.tag){
          next(ir[i].resvd) := 0;
          next(ir[i].val) := pout.val;
        }
      
      forall(i in TAG){
        if(~st[i].opra.valid & st[i].opra.tag = pout.tag){
          next(st[i].opra.valid) := 1;
          next(st[i].opra.val) := pout.val;
        }
        if(~st[i].oprb.valid & st[i].oprb.tag = pout.tag){
          next(st[i].oprb.valid) := 1;
          next(st[i].oprb.val) := pout.val;
        }
        if(st[i].issued && pout.tag = i)
          next(st[i].valid) := 0;
      }
    }

The signal pout.tag tells us which instruction the returning result is for. We match it against the tags in the register file - if any reserved register has this tag, we store the returning value in it, and mark it unreserved. Similarly, we match the tag against any reservation stations that are valid - if one of the operands has this tag, we store the result in it, and mark it valid. Finally, the reservation station whose index is pout.tag has now completed, so we mark it invalid.

Now, here's the code for incoming instructions. Note, we have to consider a special case where an operand of the incoming instruction is returning on the result bus at precisely this moment. In this case, we bypass the register file and send the result directly to the reservation station:

    if(~stallout)
      switch(opin){
        ALU : {
          
          /* store the instruction in an RS */
          
          next(ir[dst].resvd) := 1;
          next(ir[dst].tag) := st_choice;
          next(st[st_choice].valid) := 1;
          next(st[st_choice].issued) := 0;
          
          /* 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;
          }
          
          /* fetch the a operand (with bypass) */
          
          if(pout.valid & ir[srcb].resvd & pout.tag = ir[srcb].tag){
            next(st[st_choice].oprb.valid) := 1;
            next(st[st_choice].oprb.tag) := ir[srcb].tag;
            next(st[st_choice].oprb.val) := pout.val;
          } else {
            next(st[st_choice].oprb.valid) := ~ir[srcb].resvd;
            next(st[st_choice].oprb.tag) := ir[srcb].tag;
            next(st[st_choice].oprb.val) := ir[srcb].val;
          }
        }
        
        RD : dout := ir[srca].val;
        
        WR : {
          next(ir[dst].val) := din;
          next(ir[dst].resvd) := 0;
        }
      }

Note that when when fetching an operand from a reserved register, if the tag matches the returning result on pout, we directly move the pout data into the operand field of the reservation station. Otherwise, we move the contents of the register (whether a tag or a value).

Finally, here is the code for instruction issue:

    if(st[issue_choice].valid
       & st[issue_choice].opra.valid
       & st[issue_choice].oprb.valid
       & ~st[issue_choice].issued
       & exe_rdy)
      {
        exe_valid := 1;
        next(st[issue_choice].issued) := 1;
      }
    else exe_valid := 0;
    
    exe_tag  := issue_choice;
    exe_opra :=  st[issue_choice].opra.val;
    exe_oprb :=  st[issue_choice].oprb.val;
  }

If the RS chosen for issue has a valid instruction, and if both its operands are valid, and if it is not already issued, and if an execution unit is available, we send an instruction to the execution units, and mark the RS as issued.

There are two reasons why the above operations might result in a stall: the reservation station chosen for an incoming instruction might be full, or the register chosen for reading out might be reserved. Thus, here is the definition of stallout:

  ASSIGN stallout := 
    opin = ALU & st[st_choice].valid 
    | opin = RD & ir[srca].resvd;

Now, for the execution units, we will use a fairly abstract model. Each execution unit computes its result, and stores it for an arbitrary length of time, before signaling that it is ready. Here is our data structure for an execution unit:

  eu : array EU of struct{
    valid, ready : boolean;
    res : WORD;
    tag : TAG;
  }

We also need two arbitrary choices for execution units to receive the issued instruction, and to send completed results to the result bus:

  issue_eu, complete_eu : EU;

Initially, let's use only one execution unit, to simplify the proof. Later, we'll see how to handle multiple execution units.

  scalarset EU 0..0;

Here is the rest of the code for the execution unit(s):

   exe_rdy,exe_valid : boolean;
   exe_tag : TAG;
   exe_opra, exe_oprb : WORD;

   forall(i in EU)
     init(eu[i].valid) := 0;
   
   default{
     if(~eu[issue_eu].valid){
       next(eu[issue_eu].valid) := exe_valid;
       next(eu[issue_eu].res) := f[exe_opra][exe_oprb];
       next(eu[issue_eu].tag) := exe_tag;
     }
   } in {
     pout.valid := eu[complete_eu].valid & eu[complete_eu].ready;
     pout.val := eu[complete_eu].res;
     pout.tag := eu[complete_eu].tag;
     if(pout.valid)
       next(eu[complete_eu].valid) := 0;
   }

Initially, all the execution units are invalid. If the unit chosen for issue is not valid, we mark it valid, and store in it the result of applying the function f to the two operands. We also store the tag of the issuing instruction.

If the unit chosen for completion is valid and ready, we pass its result on to the result bus (pout) and mark it invalid. Note that ready is a completely nondeterministic bit here, modeling an unknown delay in the execution unit. Also note that in practice, we would define some policy for choosing a unit to issue to and a unit to complete (presumably we do not want to choose to issue to an already valid unit, for example). This would likely involve introducing a priority encoder or round-robin policy, which would break the symmetry of the EU type. Symmetry breaking is a topic for another section, however.

The last part of the implementation is the witness function for the initial state of the abstract model register file:

   layer arch:
     forall(i in REG)
       init(r[i]) := ir[i].val;