Semantics64
Semantics of instructions for RV64I.
We define state-transforming functions that model
the effect of each instruction on the RV64I 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
- Exec64-bgeu
- Semantics of the BGEU instruction [ISA:2.5.2].
- Exec64-bltu
- Semantics of the BLTU instruction [ISA:2.5.2].
- Exec64-blt
- Semantics of the BLT instruction [ISA:2.5.2].
- Exec64-bge
- Semantics of the BGE instruction [ISA:2.5.2].
- Exec64-bne
- Semantics of the BNE instruction [ISA:2.5.2].
- Exec64-beq
- Semantics of the BEQ instruction [ISA:2.5.2].
- Exec64-jalr
- Semantics of the JALR instruction [ISA:2.5.1].
- Exec64-branch
- Semantics of the instructions with the BRANCH opcode
[ISA:2.5.2].
- Exec64-jal
- Semantics of the JAL instruction [ISA:2.5.1].
- Exec64-op-imms-32
- Semantics of a shift instruction with the OP-IMM-32 opcode
[ISA:4.2.1].
- Exec64-op-32
- Semantics of the instructions with the OP-32 opcode
[ISA:4.2.2] [ISA:13.1] [ISA:13.2].
- Exec64-op
- Semantics of the instructions with the OP opcode
[ISA:2.4.2] [ISA:4.2.2] [ISA:13.1] [ISA:13.2].
- Exec64-srlw
- Semantics of the SRLW instruction.
- Exec64-sraw
- Semantics of the SRAW instruction [ISA:4.2.2].
- Exec64-op-imm-32
- Semantics of the non-shift instructions with the OP-IMM-32 opcode
[ISA:4.2.1].
- Exec64-op-imm
- Semantics of the non-shift instructions with the OP-IMM opcode
[ISA:2.4.1].
- Exec64-auipc
- Semantics of the AUIPC instruction [ISA:4.2.1].
- Exec64-store
- Semantics of the instructions with the STORE opcode
[ISA:2.6] [ISA:4.3].
- Exec64-sra
- Semantics of the SRA instruction [ISA:4.2.2].
- Exec64-sltiu
- Semantics of the SLTIU instruction [ISA:2.4.1].
- Exec64-remw
- Semantics of the REMW instruction [ISA:13.2].
- Exec64-remuw
- Semantics of the REMUW instruction [ISA:13.2].
- Exec64-op-imms
- Semantics of the shift instructions with the OP-IMM opcode
[ISA:2.4.1].
- Exec64-load
- Semantics of the instructions with the LOAD opcode
[ISA:2.6] [ISA:4.3].
- Exec64-srliw
- Semantics of the SRLIW instruction [ISA:4.2.1].
- Exec64-srl
- Semantics of the SRL instruction [ISA:4.2.2].
- Exec64-sraiw
- Semantics of the SRAIW instruction [ISA:4.2.1].
- Exec64-slti
- Semantics of the SLTI instruction [ISA:2.4.1].
- Exec64-sllw
- Semantics of the SLLW instruction.
- Exec64-remu
- Semanics of the REMU instruction [ISA:13.2].
- Exec64-rem
- Semanics of the REM instruction [ISA:13.2].
- Exec64-divw
- Semantics of the DIVW instruction [ISA:13.2].
- Exec64-divuw
- Semantics of the DIVUW instruction [ISA:13.2].
- Exec64-addiw
- Semantics of the ADDIW instruction [ISA:4.2.1].
- Exec64-xori
- Semantics of the XORI instruction [ISA:2.4.1].
- Exec64-srli
- Semantics of the SRLI instruction [ISA:2.4.1].
- Exec64-srai
- Semantics of the SRAI instruction [ISA:2.4.1].
- Exec64-ori
- Semantics of the ORI instruction [ISA:2.4.1].
- Exec64-divu
- Semanics of the DIVU instruction [ISA:13.2].
- Exec64-andi
- Semantics of the ANDI instruction [ISA:2.4.1].
- Exec64-addi
- Semantics of the ADDI instruction [ISA:2.4.1].
- Exec64-sltu
- Semantics of the SLTU instruction [ISA:2.4.2].
- Exec64-slt
- Semantics of the SLT instruction [ISA:2.4.2].
- Exec64-slliw
- Semantics of the SLLIW instruction [ISA:4.2.1].
- Exec64-sll
- Semantics of the SLL instruction [ISA:4.2.2].
- Exec64-mulhsu
- Semanics of the MULHSU instruction [ISA:13.1].
- Exec64-lwu
- Semantics of the LW instruction [ISA:4.3].
- Exec64-lhu
- Semantics of the LHU instruction [ISA:2.6].
- Exec64-div
- Semanics of the DIV instruction [ISA:13.2].
- Exec64-xor
- Semantics of the XOR instruction [ISA:2.4.2].
- Exec64-sw
- Semantics of the SW instruction [ISA:4.3].
- Exec64-slli
- Semantics of the SLLI instruction [ISA:2.4.1].
- Exec64-sh
- Semantics of the SH instruction [ISA:2.6].
- Exec64-mulw
- Semantics of the MULW instruction [ISA:13.1].
- Exec64-mulhu
- Semanics of the MULHU instruction [ISA:13.1].
- Exec64-mulh
- Semanics of the MULH instruction [ISA:13.1].
- Exec64-lw
- Semantics of the LW instruction [ISA:4.3].
- Exec64-lh
- Semantics of the LH instruction [ISA:2.6].
- Exec64-lbu
- Semantics of the LBU instruction [ISA:2.6].
- Exec64-addw
- Semantics of the ADDW instruction [ISA:4.2.2].
- Exec64-subw
- Semantics of the SUBW instruction [ISA:4.2.2].
- Exec64-sub
- Semantics of the SUB instruction [ISA:2.4.2].
- Exec64-sd
- Semantics of the SD instruction [ISA:4.3].
- Exec64-sb
- Semantics of the SB instruction [ISA:2.6].
- Exec64-or
- Semantics of the OR instruction [ISA:2.4.2].
- Exec64-ld
- Semantics of the LW instruction [ISA:4.3].
- Exec64-lb
- Semantics of the LB instruction [ISA:2.6].
- Exec64-and
- Semantics of the AND instruction [ISA:2.4.2].
- Exec64-mul
- Semanics of the MUL instruction [ISA:13.1].
- Exec64-add
- Semantics of the ADD instruction [ISA:2.4.2].
- Exec64-instr
- Semantics of instructions.
- Eff64-addr
- Effective address for a load or store instruction [ISA:2.6].
- Exec64-lui
- Semantics of the LUI instruction [ISA:4.2.1].
