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).