		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, RV64IM, RV32EM, and RV64EM, (except for the FENCE, HINT, ECALL and EBREAK instructions), fully readable and writable address space, and no alignment checks. We plan to extend and improve this library.

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 plan to extend the general model to 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 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 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.