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