		Search-engine friendly clone of the ACL2 documentation.

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.

We have a generic model of RISC-V, parameterized over a growing set of features, and we have two specialized models tailored to RV32IM and RV64IM. We plan to have the general model cover more features, and we plan to re-obtain the specialized models via transformation and specialization of the general model.

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

Semantics: Semantics of instructions.
Instructions: Model of instructions.
States: Model of states.
Decoding: Decoding of instructions.
Encoding: Encoding of instructions.
Features: RISC-V features.
Rv32im: Specialized model for RV32IM.
Rv64im: Specialized model for RV64IM.
Execution: Model of execution.