Semantics32
Semantics of instructions for RV32I.
We define state-transforming functions that model
the effect of each instruction on the RV32I state.
For now we only support little endian access to memory,
in load and store instructions.
Also, for now we do no alignment checks.
Subtopics
- Exec32-bgeu
- Semantics of the BGEU instruction [ISA:2.5.2].
- Exec32-bltu
- Semantics of the BLTU instruction [ISA:2.5.2].
- Exec32-blt
- Semantics of the BLT instruction [ISA:2.5.2].
- Exec32-bge
- Semantics of the BGE instruction [ISA:2.5.2].
- Exec32-bne
- Semantics of the BNE instruction [ISA:2.5.2].
- Exec32-beq
- Semantics of the BEQ instruction [ISA:2.5.2].
- Exec32-jalr
- Semantics of the JALR instruction [ISA:2.5.1].
- Exec32-branch
- Semantics of the instructions with the BRANCH opcode
[ISA:2.5.2].
- Exec32-jal
- Semantics of the JAL instruction [ISA:2.5.1].
- Exec32-op
- Semantics of the instructions with the OP opcode
[ISA:2.4.2] [ISA:4.2.2] [ISA:13.1] [ISA:13.2].
- Exec32-store
- Semantics of the instructions with the STORE opcode [ISA:2.6].
- Exec32-op-imm
- Semantics of the non-shift instructions with the OP-IMM opcode
[ISA:2.4.1].
- Exec32-load
- Semantics of the instructions with the LOAD opcode [ISA:2.6].
- Exec32-sra
- Semantics of the SRA instruction [ISA:4.2.2].
- Exec32-sltiu
- Semantics of the SLTIU instruction [ISA:2.4.1].
- Exec32-op-imms
- Semantics of the shift instructions with the OP-IMM opcode
[ISA:2.4.1].
- Exec32-srl
- Semantics of the SRL instruction [ISA:4.2.2].
- Exec32-slti
- Semantics of the SLTI instruction [ISA:2.4.1].
- Exec32-remu
- Semanics of the REMU instruction [ISA:13.2].
- Exec32-rem
- Semanics of the REM instruction [ISA:13.2].
- Exec32-auipc
- Semantics of the AUIPC instruction [ISA:4.2.1].
- Exec32-xori
- Semantics of the XORI instruction [ISA:2.4.1].
- Exec32-srli
- Semantics of the SRLI instruction [ISA:2.4.1].
- Exec32-srai
- Semantics of the SRAI instruction [ISA:2.4.1].
- Exec32-ori
- Semantics of the ORI instruction [ISA:2.4.1].
- Exec32-divu
- Semanics of the DIVU instruction [ISA:13.2].
- Exec32-andi
- Semantics of the ANDI instruction [ISA:2.4.1].
- Exec32-addi
- Semantics of the ADDI instruction [ISA:2.4.1].
- Exec32-sltu
- Semantics of the SLTU instruction [ISA:2.4.2].
- Exec32-slt
- Semantics of the SLT instruction [ISA:2.4.2].
- Exec32-sll
- Semantics of the SLL instruction [ISA:4.2.2].
- Exec32-mulhsu
- Semanics of the MULHSU instruction [ISA:13.1].
- Exec32-lhu
- Semantics of the LHU instruction [ISA:2.6].
- Exec32-div
- Semanics of the DIV instruction [ISA:13.2].
- Exec32-xor
- Semantics of the XOR instruction [ISA:2.4.2].
- Exec32-slli
- Semantics of the SLLI instruction [ISA:2.4.1].
- Exec32-sh
- Semantics of the SH instruction [ISA:2.6].
- Exec32-mulhu
- Semanics of the MULHU instruction [ISA:13.1].
- Exec32-mulh
- Semanics of the MULH instruction [ISA:13.1].
- Exec32-lh
- Semantics of the LH instruction [ISA:2.6].
- Exec32-lbu
- Semantics of the LBU instruction [ISA:2.6].
- Exec32-sw
- Semantics of the SW instruction [ISA:2.6].
- Exec32-sub
- Semantics of the SUB instruction [ISA:2.4.2].
- Exec32-sb
- Semantics of the SB instruction [ISA:2.6].
- Exec32-or
- Semantics of the OR instruction [ISA:2.4.2].
- Exec32-lw
- Semantics of the LW instruction [ISA:2.6].
- Exec32-lb
- Semantics of the LB instruction [ISA:2.6].
- Exec32-and
- Semantics of the AND instruction [ISA:2.4.2].
- Exec32-mul
- Semanics of the MUL instruction [ISA:13.1].
- Exec32-add
- Semantics of the ADD instruction [ISA:2.4.2].
- Exec32-instr
- Semantics of instructions.
- Eff32-addr
- Effective address for a load or store instruction [ISA:2.6].
- Exec32-lui
- Semantics of the LUI instruction [ISA:4.2.1].
