Semantics
Semantics of instructions.
We introduce functions that say how
each instruction operates on the state.
We restrict this to valid instructions in valid states
with respect to the RISC-V features.
For some integer instructions, like SLT and SLTU,
it is important whether the operands are read as signed or unsigned.
For other instructions, like ADD it does not matter,
so long as they are both read signed or unsigned
(not one signed and the other unsigned);
for these instructions, we add theorem showing two definitions equivalent,
one that reads signed operands and one that reads unsigned operands.
There is a fair amount of repetition in boilerplate in these functions.
We could consider shortening them via suitable macros.
Subtopics
- Exec-bltu
- Semantics of the BLTU instruction [ISA:2.5.2].
- Exec-blt
- Semantics of the BLT instruction [ISA:2.5.2].
- Exec-bgeu
- Semantics of the BGEU instruction [ISA:2.5.2].
- Exec-bge
- Semantics of the BGE instruction [ISA:2.5.2].
- Exec-jalr
- Semantics of the JALR instruction [ISA:2.5.1].
- Exec-bne
- Semantics of the BNE instruction [ISA:2.5.2].
- Exec-beq
- Semantics of the BEQ instruction [ISA:2.5.2].
- Exec-sra
- Semantics of the SRA instruction [ISA:4.2.2].
- Exec-op
- Semantics of the instructions with the OP opcode
[ISA:2.4.2] [ISA:4.2.2] [ISA:13.1] [ISA:13.2].
- Exec-srl
- Semantics of the SRL instruction [ISA:4.2.2].
- Exec-op-imms-32
- Semantics of a shift instruction with the OP-IMM-32 opcode
[ISA:4.2.1].
- Exec-op-32
- Semantics of the instructions with the OP-32 opcode
[ISA:4.2.2] [ISA:13.1] [ISA:13.2].
- Exec-srlw
- Semantics of the SRLW instruction [ISA:4.2.2].
- Exec-sraw
- Semantics of the SRAW instruction [ISA:4.2.2].
- Exec-sll
- Semantics of the SLL instruction [ISA:4.2.2].
- Exec-remuw
- Semantics of the REMUW instruction [ISA:13.2].
- Exec-op-imms64
- Semantics of the shift instructions with the OP-IMM opcode
[ISA:2.4.1] in 64-bit mode.
- Exec-op-imms32
- Semantics of the shift instructions with the OP-IMM opcode
[ISA:2.4.1] in 32-bit mode.
- Exec-op-imm-32
- Semantics of the non-shift instructions with the OP-IMM-32 opcode
[ISA:4.2.1].
- Exec-branch
- Semantics of the instructions with the BRANCH opcode
[ISA:2.5.2].
- Exec-addi
- Semantics of the ADDI instruction [ISA:2.4.1].
- Exec-srliw
- Semantics of the SRLIW instruction [ISA:4.2.1].
- Exec-sraiw
- Semantics of the SRAIW instruction [ISA:4.2.1].
- Exec-sltiu
- Semantics of the SLTIU instruction [ISA:2.4.1].
- Exec-remw
- Semantics of the REMW instruction [ISA:13.2].
- Exec-op-imm
- Semantics of the non-shift instructions with the OP-IMM opcode
[ISA:2.4.1].
- Exec-jal
- Semantics of the JAL instruction [ISA:2.5.1].
- Exec-divuw
- Semantics of the DIVUW instruction [ISA:13.2].
- Exec-sub
- Semantics of the SUB instruction [ISA:2.4.2].
- Exec-store
- Semantics of the instructions with the STORE opcode [ISA:2.6].
- Exec-srli64
- Semantics of the SRLI instruction [ISA:2.4.1] in 64-bit mode.
- Exec-srli32
- Semantics of the SRLI instruction [ISA:2.4.1] in 32-bit mode.
- Exec-srai64
- Semantics of the SRAI instruction [ISA:2.4.1] in 64-bit mode.
- Exec-srai32
- Semantics of the SRAI instruction [ISA:2.4.1] in 32-bit mode.
- Exec-sllw
- Semantics of the SLLW instruction [ISA:4.2.2].
- Exec-remu
- Semanics of the REMU instruction [ISA:13.2].
- Exec-load
- Semantics of the instructions with the LOAD opcode [ISA:2.6].
- Exec-divw
- Semantics of the DIVW instruction [ISA:13.2].
- Exec-addiw
- Semantics of the ADDIW instruction [ISA:4.2.1].
- Exec-xori
- Semantics of the XORI instruction [ISA:2.4.1].
- Exec-slti
- Semantics of the SLTI instruction [ISA:2.4.1].
- Exec-slliw
- Semantics of the SLLIW instruction [ISA:4.2.1].
- Exec-rem
- Semanics of the REM instruction [ISA:13.2].
- Exec-ori
- Semantics of the ORI instruction [ISA:2.4.1].
- Exec-mulhsu
- Semanics of the MULHSU instruction [ISA:13.1].
- Exec-divu
- Semanics of the DIVU instruction [ISA:13.2].
- Exec-andi
- Semantics of the ANDI instruction [ISA:2.4.1].
- Exec-add
- Semantics of the ADD instruction [ISA:2.4.2].
- Exec-sw
- Semantics of the SW instruction [ISA:2.6].
- Exec-sltu
- Semantics of the SLTU instruction [ISA:2.4.2].
- Exec-slt
- Semantics of the SLT instruction [ISA:2.4.2].
- Exec-slli64
- Semantics of the SLLI instruction [ISA:2.4.1] in 64-bit mode.
- Exec-slli32
- Semantics of the SLLI instruction [ISA:2.4.1] in 32-bit mode.
- Exec-mulhu
- Semanics of the MULHU instruction [ISA:13.1].
- Exec-div
- Semanics of the DIV instruction [ISA:13.2].
- Exec-addw
- Semantics of the ADDW instruction [ISA:4.2.2].
- Exec-mulw
- Semantics of the MULW instruction [ISA:13.1].
- Exec-mulh
- Semanics of the MULH instruction [ISA:13.1].
- Exec-lwu
- Semantics of the LW instruction [ISA:4.3].
- Exec-auipc
- Semantics of the AUIPC instruction [ISA:4.2.1].
- Exec-xor
- Semantics of the XOR instruction [ISA:2.4.2].
- Exec-subw
- Semantics of the SUBW instruction [ISA:4.2.2].
- Exec-or
- Semantics of the OR instruction [ISA:2.4.2].
- Exec-lhu
- Semantics of the LHU instruction [ISA:2.6].
- Exec-lbu
- Semantics of the LBU instruction [ISA:2.6].
- Exec-and
- Semantics of the AND instruction [ISA:2.4.2].
- Exec-sd
- Semantics of the SD instruction [ISA:4.3].
- Exec-mul
- Semanics of the MUL instruction [ISA:13.1].
- Exec-lh
- Semantics of the LH instruction [ISA:2.6].
- Exec-ld
- Semantics of the LW instruction [ISA:4.3].
- Exec-lb
- Semantics of the LB instruction [ISA:2.6].
- Exec-sh
- Semantics of the SH instruction [ISA:2.6].
- Exec-sb
- Semantics of the SB instruction [ISA:2.6].
- Exec-lw
- Semantics of the LW instruction [ISA:2.6].
- Exec-lui
- Semantics of the LUI instruction [ISA:4.2.1].
- Eff-addr
- Effective address for a load or store instruction [ISA:2.6].
- Exec-instr
- Semantics of instructions.
