		Search-engine friendly clone of the ACL2 documentation.

Riscv

An ACL2 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 formalization of part of the the RISC-V ISA: unprivileged RV32IM, RV64IM, RV32EM, and RV64EM, (except for the FENCE, HINT, ECALL and EBREAK instructions), fully readable and writable address space, and no alignment checks for data in memory (but there are alignment checks for instructions).

We provide a generic model of RISC-V, parameterized over a growing set of features, and we also provide two specialized models tailored to RV32IM and RV64IM. We are working on re-obtaining the specialized models via transformation and specialization of the general model.

This library is based on the following sources:

The RISC-V Insruction Set Manual Volume 1, Unprivileged Architecture Version 20250508, 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 RISC-V Insruction Set Manual Volume 2, Privileged Architecture Version 20250508, 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

Specification: Specification of the RISC-V ISA.
Executable: Executable refinement of the RISC-V specification.
Specialized: Specialized versions of the RISC-V ISA.
Optimized: Optimized refinements of the RISC-V specification.