		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, 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

Decoding: Decoding of instructions.
Instructions: Model of instructions.
States: Model of states.
Semantics: Semantics of instructions.
Execution: Model of execution.