Overview
instrADD is shown as an operation property in the paper Generating an Efficient Instruction Set Simulator from a Complete Property Suite. It specifies the behavior of an ADD instruction in ITL as part of a property-suite-based processor model. In the complete-property-suite approach described by the paper, successfully verified properties can form a model of the verified design by uniquely describing transitions and output behavior; this model can then be exploited to generate an executable simulator. [C1]
Structure
The property is organized into the standard ITL-style sections shown in the figure: freeze, assume, and prove. [C2]
freeze section
The freeze section decomposes the instruction word at time t into fields used by the ADD operation: [C2]
opcode = instr(15 downto 11)@t
regA = instr(10 downto 8)@t
regB = instr( 7 downto 5)@t
regD = instr( 4 downto 2)@t
These fields represent the decoded opcode, the two source-register addresses, and the destination-register address. The accompanying text states that the instruction word is decomposed according to the specification into the opcode and the addresses of source and target registers. [C3]
assume section
The property applies when the decoded instruction is ADD and the processor is ready to execute it. The assumptions shown are: [C2]
at t: opcode = ADD_op;
at t: not stall;
at t: not interrupt;
The paper summarizes these constraints as requiring that there is actually an ADD instruction and that the processor is ready to execute it. [C3]
prove section
Under the ADD-ready assumptions, the property proves the architectural register update: [C2]
at t: write_reg(regD, vreg(regA) + vreg(regB));
The paper states that, under these constraints, it is proved that one time step later the register file is updated with the correct value. [C3]
Relationship to write_reg
instrADD uses the write_reg macro to express the register-file write. The macro is shown as iterating over registers k in 0..7; it updates the selected register with the low 16 bits of the result and leaves other registers unchanged. [C4]
Role in a complete property suite
The example appears in the context of generating an instruction set simulator from a complete property suite. The paper explains that, after successful verification, the property suite can serve as a model of the design, describing transitions and output behavior uniquely, and that this can be used to obtain an executable simulator. [C1]