• 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
    • Riscv
      • Semantics
        • Exec-bgeu
        • Exec-bltu
        • Exec-blt
        • Exec-bge
        • Exec-jalr
        • Exec-bne
        • Exec-beq
        • Exec-sra
        • Exec-op-imms-32
        • Exec-srl
        • Exec-branch
        • Exec-sll
        • Exec-op-imms64
        • Exec-op-imms32
        • Exec-op-imm-32
        • Exec-op-32
        • Exec-op
        • Exec-srlw
        • Exec-srliw
        • Exec-sraw
        • Exec-sraiw
        • Exec-sltiu
        • Exec-remuw
        • Exec-op-imm
        • Exec-jal
        • Exec-store
        • Exec-srli64
        • Exec-srli32
        • Exec-srai64
        • Exec-srai32
        • Exec-sllw
        • Exec-remw
        • Exec-load
        • Exec-divuw
        • Exec-addiw
        • Exec-xori
        • Exec-slti
        • Exec-slliw
        • Exec-remu
        • Exec-rem
        • Exec-divw
        • Exec-sw
        • Exec-slli64
        • Exec-slli32
        • Exec-ori
        • Exec-mulhsu
        • Exec-divu
        • Exec-andi
        • Exec-addi
        • Exec-sltu
        • Exec-slt
        • Exec-mulhu
        • Exec-div
        • Exec-auipc
        • Exec-addw
        • Exec-xor
        • Exec-mulw
        • Exec-mulh
        • Exec-lwu
        • Exec-and
        • Exec-subw
        • Exec-sub
        • Exec-sh
        • Exec-sd
        • Exec-sb
        • Exec-or
        • Exec-lhu
        • Exec-lh
        • Exec-ld
        • Exec-lbu
        • Exec-lb
        • Exec-mul
        • Exec-add
        • Exec-lw
        • Exec-lui
        • Eff-addr
        • Exec-instr
      • Instructions
      • States
      • Decoding
      • Encoding
      • Features
      • Rv32im
      • Rv64im
      • Execution
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • 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
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Community
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Riscv

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.

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-imms-32

Semantics of a shift instruction with the OP-IMM-32 opcode [ISA:4.2.1].

Exec-srl

Semantics of the SRL instruction [ISA:4.2.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-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-op-32

Semantics of the instructions with the OP-32 opcode [ISA:4.2.2] [ISA:13.1] [ISA:13.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-srlw

Semantics of the SRLW instruction [ISA:4.2.2].

Exec-srliw

Semantics of the SRLIW instruction [ISA:4.2.1].

Exec-sraw

Semantics of the SRAW instruction [ISA:4.2.2].

Exec-sraiw

Semantics of the SRAIW instruction [ISA:4.2.1].

Exec-sltiu

Semantics of the SLTIU instruction [ISA:2.4.1].

Exec-remuw

Semantics of the REMUW 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-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-remw

Semantics of the REMW instruction [ISA:13.2].

Exec-load

Semantics of the instructions with the LOAD opcode [ISA:2.6].

Exec-divuw

Semantics of the DIVUW 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-remu

Semanics of the REMU instruction [ISA:13.2].

Exec-rem

Semanics of the REM instruction [ISA:13.2].

Exec-divw

Semantics of the DIVW instruction [ISA:13.2].

Exec-sw

Semantics of the SW instruction [ISA:2.6].

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-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-addi

Semantics of the ADDI instruction [ISA:2.4.1].

Exec-sltu

Semantics of the SLTU instruction [ISA:2.4.2].

Exec-slt

Semantics of the SLT instruction [ISA:2.4.2].

Exec-mulhu

Semanics of the MULHU instruction [ISA:13.1].

Exec-div

Semanics of the DIV instruction [ISA:13.2].

Exec-auipc

Semantics of the AUIPC instruction [ISA:4.2.1].

Exec-addw

Semantics of the ADDW instruction [ISA:4.2.2].

Exec-xor

Semantics of the XOR instruction [ISA:2.4.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-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-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-or

Semantics of the OR instruction [ISA:2.4.2].

Exec-lhu

Semantics of the LHU instruction [ISA:2.6].

Exec-lh

Semantics of the LH instruction [ISA:2.6].

Exec-ld

Semantics of the LW instruction [ISA:4.3].

Exec-lbu

Semantics of the LBU instruction [ISA:2.6].

Exec-lb

Semantics of the LB instruction [ISA:2.6].

Exec-mul

Semanics of the MUL instruction [ISA:13.1].

Exec-add

Semantics of the ADD instruction [ISA:2.4.2].

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.