• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Riscv
        • Specification
          • Semantics
            • Exec-bgeu
            • Exec-bltu
            • Exec-blt
            • Exec-bge
            • Exec-bne
            • Exec-beq
            • Exec-jalr
            • Exec-jal
            • Exec-sra
            • Exec-op-imms-32
            • Exec-op
            • Exec-srl
            • Exec-op-32
            • Exec-branch
            • Exec-sll
            • Exec-op-imm-32
            • Exec-srlw
            • Exec-sraw
            • Exec-sltiu
            • Exec-remuw
            • Exec-op-imms64
            • Exec-op-imms32
            • Exec-op-imm
            • Exec-divuw
            • Exec-store
            • Exec-srliw
            • Exec-sraiw
            • Exec-sllw
            • Exec-remw
            • Exec-load
            • Exec-addiw
            • Exec-xori
            • Exec-srli64
            • Exec-srli32
            • Exec-srai64
            • Exec-srai32
            • Exec-slliw
            • Exec-remu
            • Exec-rem
            • Exec-mulhsu
            • Exec-divw
            • Exec-divu
            • Exec-sw
            • Exec-sltu
            • Exec-slti
            • Exec-slli64
            • Exec-slli32
            • Exec-ori
            • Exec-div
            • Exec-auipc
            • Exec-andi
            • Exec-slt
            • Exec-mulw
            • Exec-mulhu
            • Exec-addw
            • Exec-addi
            • Exec-xor
            • Exec-sub
            • Exec-or
            • Exec-mulh
            • Exec-lwu
            • Exec-and
            • Exec-subw
            • Exec-lhu
            • Exec-lh
            • Exec-lbu
            • Exec-lb
            • Exec-add
            • Exec-sh
            • Exec-sd
            • Exec-sb
            • Exec-mul
            • Exec-ld
            • Exec-lw
            • Exec-lui
            • Eff-addr
            • Exec-instr
          • Features
          • Instructions
          • Encoding
          • States
          • Reads-over-writes
          • Semantics-equivalences
          • Decoding
          • Execution
        • Executable
        • Specialized
        • Optimized
      • Taspi
      • Bitcoin
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Aleo
      • Bigmems
      • Builtins
      • Execloader
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Specification

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-bne
Semantics of the BNE instruction [ISA:2.5.2].
Exec-beq
Semantics of the BEQ instruction [ISA:2.5.2].
Exec-jalr
Semantics of the JALR instruction [ISA:2.5.1].
Exec-jal
Semantics of the JAL instruction [ISA:2.5.1].
Exec-sra
Semantics of the SRA 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
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-32
Semantics of the instructions with the OP-32 opcode [ISA:4.2.2] [ISA:12.1] [ISA:12.2].
Exec-branch
Semantics of the instructions with the BRANCH opcode [ISA:2.5.2].
Exec-sll
Semantics of the SLL instruction [ISA:4.2.2].
Exec-op-imm-32
Semantics of the non-shift instructions with the OP-IMM-32 opcode [ISA:4.2.1].
Exec-srlw
Semantics of the SRLW instruction [ISA:4.2.2].
Exec-sraw
Semantics of the SRAW instruction [ISA:4.2.2].
Exec-sltiu
Semantics of the SLTIU instruction [ISA:2.4.1].
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
Semantics of the non-shift instructions with the OP-IMM opcode [ISA:2.4.1].
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-srliw
Semantics of the SRLIW instruction [ISA:4.2.1].
Exec-sraiw
Semantics of the SRAIW instruction [ISA:4.2.1].
Exec-sllw
Semantics of the SLLW instruction [ISA:4.2.2].
Exec-remw
Semantics of the REMW instruction [ISA:12.2].
Exec-load
Semantics of the instructions with the LOAD opcode [ISA:2.6] [ISA:4.3].
Exec-addiw
Semantics of the ADDIW instruction [ISA:4.2.1].
Exec-xori
Semantics of the XORI instruction [ISA:2.4.1].
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-slliw
Semantics of the SLLIW instruction [ISA:4.2.1].
Exec-remu
Semanics of the REMU instruction [ISA:12.2].
Exec-rem
Semanics of the REM instruction [ISA:12.2].
Exec-mulhsu
Semanics of the MULHSU instruction [ISA:12.1].
Exec-divw
Semantics of the DIVW instruction [ISA:12.2].
Exec-divu
Semanics of the DIVU instruction [ISA:12.2].
Exec-sw
Semantics of the SW instruction [ISA:2.6].
Exec-sltu
Semantics of the SLTU instruction [ISA:2.4.2].
Exec-slti
Semantics of the SLTI instruction [ISA:2.4.1].
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-ori
Semantics of the ORI instruction [ISA:2.4.1].
Exec-div
Semanics of the DIV 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-slt
Semantics of the SLT instruction [ISA:2.4.2].
Exec-mulw
Semantics of the MULW instruction [ISA:12.1].
Exec-mulhu
Semanics of the MULHU instruction [ISA:12.1].
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-sub
Semantics of the SUB instruction [ISA:2.4.2].
Exec-or
Semantics of the OR instruction [ISA:2.4.2].
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-lhu
Semantics of the LHU instruction [ISA:2.6].
Exec-lh
Semantics of the LH instruction [ISA:2.6].
Exec-lbu
Semantics of the LBU instruction [ISA:2.6].
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-sd
Semantics of the SD instruction [ISA:4.3].
Exec-sb
Semantics of the SB instruction [ISA:2.6].
Exec-mul
Semanics of the MUL instruction [ISA:12.1].
Exec-ld
Semantics of the LW instruction [ISA:4.3].
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.