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.
For the latter kinds of instructions,
we read unsigned operands in the semntic functions;
however, in semantics-equivalences we prove
equivalent definitions that read signed operands.
There is a fair amount of repetition in boilerplate in these functions.
We could consider shortening them via suitable macros.
Subtopics
- Exec-bgeu
- Semantics of the BGEU instruction [ISA:2.5.2].
- Exec-bltu
- Semantics of the BLTU instruction [ISA:2.5.2].
- Exec-blt
- Semantics of the BLT 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:12.1] [ISA:12.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:12.1] [ISA:12.2].
- Exec-sll
- Semantics of the SLL instruction [ISA:4.2.2].
- Exec-branch
- Semantics of the instructions with the BRANCH opcode
[ISA:2.5.2].
- Exec-srlw
- Semantics of the SRLW instruction [ISA:4.2.2].
- Exec-sraw
- Semantics of the SRAW instruction [ISA:4.2.2].
- Exec-remuw
- Semantics of the REMUW instruction [ISA:12.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-jal
- Semantics of the JAL instruction [ISA:2.5.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:12.2].
- Exec-op-imm
- Semantics of the non-shift instructions with the OP-IMM opcode
[ISA:2.4.1].
- Exec-load
- Semantics of the instructions with the LOAD opcode
[ISA:2.6] [ISA:4.3].
- Exec-divuw
- Semantics of the DIVUW instruction [ISA:12.2].
- Exec-store
- Semantics of the instructions with the STORE opcode
[ISA:2.6] [ISA:4.3].
- 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:12.2].
- Exec-divw
- Semantics of the DIVW instruction [ISA:12.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:12.2].
- Exec-ori
- Semantics of the ORI instruction [ISA:2.4.1].
- Exec-mulhsu
- Semanics of the MULHSU instruction [ISA:12.1].
- Exec-divu
- Semanics of the DIVU instruction [ISA:12.2].
- Exec-auipc
- Semantics of the AUIPC instruction [ISA:2.4.1] [ISA:4.2.1].
- Exec-andi
- Semantics of the ANDI instruction [ISA:2.4.1].
- 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:12.1].
- Exec-div
- Semanics of the DIV instruction [ISA:12.2].
- Exec-addw
- Semantics of the ADDW instruction [ISA:4.2.2].
- Exec-addi
- Semantics of the ADDI instruction [ISA:2.4.1].
- Exec-xor
- Semantics of the XOR instruction [ISA:2.4.2].
- Exec-mulw
- Semantics of the MULW instruction [ISA:12.1].
- Exec-mulh
- Semanics of the MULH instruction [ISA:12.1].
- Exec-lwu
- Semantics of the LW instruction [ISA:4.3].
- Exec-and
- Semantics of the AND instruction [ISA:2.4.2].
- Exec-subw
- Semantics of the SUBW instruction [ISA:4.2.2].
- Exec-sub
- Semantics of the SUB instruction [ISA:2.4.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-sd
- Semantics of the SD instruction [ISA:4.3].
- Exec-mul
- Semanics of the MUL instruction [ISA:12.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-add
- Semantics of the ADD instruction [ISA:2.4.2].
- 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:2.4.1] [ISA:4.2.1].
- Eff-addr
- Effective address for a load or store instruction [ISA:2.6].
- Exec-instr
- Semantics of instructions.
