The abstract model

As before, our abstract model is a simple machine that executes instructions in order as they arrive. Additionally, in this case, it has the ability to stall. The choice of whether to stall or not is nondeterministic.

As before, we make the register index values and data values undefined scalarsets:

scalarset WORD undefined;
scalarset REG  undefined;

module main()
{
  ...
}

We define an uninterpreted function f for the ALU:

  f : array WORD of array WORD of WORD;
  next(f) := f;

Here is the abstract model:

  opin : {ALU,RD,WR,NOP};       /* opcode input */
  srca,srcb,dst : REG;          /* source and dest indices input */
  din,dout : WORD;              /* data input and output */
  r : array REG of WORD;        /* the register file */
  opra,oprb,res : WORD;         /* operands and result */
  stallout : boolean;           /* stall output (nondeterministic) */

  /* the abstract model */

  layer arch:
    if(~stallout)
      switch(opin){
        ALU : {
          opra := r[srca];
          oprb := r[srcb];
          res := f[opra][oprb];
          next(r[dst]) := res;
        }
        RD : {
          dout := r[srca];
        }
        WR : {
          next(r[dst]) := din;
        }
      }

Note that we've put our specification inside a layer called arch, so that we can refine the data output signal dout in the implementation. Also note that since we haven't specified a value for stallout it remains nondeterministic. In case of an ALU operation, our behavior is as before: apply the ALU operation f to the two source operands, and store the result in the register file. In case of a RD operation, we read the srca operand from the register file and assign it to dout, the data output. In case of a WR operation, we store the value of the data input, din, into the destination register. (Finally, in case of a NOP operation, we do nothing).