• 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
        • Instructions
        • States
        • Decoding
        • Encoding
        • Features
        • Rv32im
          • Semantics32
          • States32
          • Execution32
        • 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

Rv32im

Specialized model for RV32IM.

This consists of a model of states and instruction execution for RV32IM. This was developed before the more general model with features. We plan to re-obtain this specialized model via transformation and specialization of the general one at some point, but until then we keep it around.

Subtopics

Semantics32
Semantics of instructions for RV32IM.
States32
Model of states for RV32IM.
Execution32
Model of execution for RV32IM.