Overview

write_reg is a macro shown in an ITL operation property for a simple pipelined processor's ADD instruction. The property decodes an instruction word into opcode, source registers regA and regB, and destination register regD, assumes the opcode is ADD_op and that the processor is not stalled or interrupted, and then proves the register-file update using:

at t: write_reg(regD, vreg(regA) + vreg(regB));

Semantics

The macro iterates over the architectural register indices 0..7. For the selected index i, it constrains the next value of vreg(k) to the low 16 bits of the supplied result. For every other register index, it constrains the next value of vreg(k) to equal its current value.

macro write_reg(i, res: unsigned): boolean :=
  foreach k in 0..7:
    if (k = i) then
      next(vreg(k)) = res(15 downto 0);
    else
      next(vreg(k)) = vreg(k);
    end if;
  end foreach;
end macro;

The paper explains the purpose of this style of assertion in terms of completeness: the property must not only state that the destination register receives the computed value, but also that the remaining registers do not change. That unchanged-register condition is included in write_reg.

Role in the ADD property

In the ADD operation property, write_reg specifies that execution of the instruction updates the destination architectural register with vreg(regA) + vreg(regB). The surrounding text states that, under the ADD execution assumptions, the property proves that one time step later the register file is updated with the correct value.

Architectural abstraction

The register file is referenced through the mapping function vreg, which represents the architectural register file. For a pipelined processor, the implementation registers may depend on multiple in-flight instructions; the mapping function hides the forwarding logic and presents a programmer-visible architectural state to the property.