• 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
      • Taspi
      • Bitcoin
      • Riscv
        • Instructions
        • States
        • Decoding
        • Encoding
        • Features
        • Semantics
        • Execution
      • 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
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Projects

Riscv

A library for RISC-V.

RISC-V is an open instruction set architecture (ISA) based on reduced-instruction-set-computer (RISC) principles. RISC-V is modular, with base instruction sets and optional extensions.

This ACL2 library includes a preliminary formalization of part of the the RISC-V ISA: unprivileged RV32IM and RV64IM (except for the FENCE, HINT, ECALL and EBREAK instructions), little endian memory access, fully readable and writable address space, no alignment checks. We plan to extend and improve this library.

This library is based on the following sources:

  • The The RISC-V Insruction Set Manual Volume 1, Unprivileged Architecture v. 20240411, referenced as `[ISA]' in the documentation of this library. Chapters and sections are referenced by appending their designations separated by colon, e.g. `[ISA:2.2]' references Section 2.2 of [ISA].
  • The The RISC-V Insruction Set Manual Volume 2, Privileged Architecture v. 20240411, referenced as `[ISAP]' in the documentation of this library. Chapters and sections are referenced by appending their designations separated by colon, e.g. `[ISAP:3.3]' references Section 3.3 of [ISAP].

These square-bracketed references may be used as nouns or parenthentically.

Subtopics

Instructions
Model of instructions.
States
Model of states.
Decoding
Decoding of instructions.
Encoding
Encoding of instructions.
Features
RISC-V features.
Semantics
Semantics of instructions.
Execution
Model of execution.