RV32I in ACL2
The work
| Authors | Carl Kwan |
|---|---|
| Editors | |
| Type | article |
| Year | 2025 |
| Citekey | kwan2025rv32i |
Where it appeared
| Published in | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Publisher | Open Publishing Association |
| Volume | 423 |
| Pages | 46--50 |
Identifiers
| DOI | 10.4204/eptcs.423.4 |
|---|---|
| OpenAlex | W4412627440 |
Access
| Landing page | https://doi.org/10.4204/eptcs.423.4 |
|---|---|
| Free full text | https://eptcs.web.cse.unsw.edu.au/paper.cgi?ACL2in2025.4.pdf |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
We present a simple ACL2 simulator for the RISC-V 32-bit base instruction set architecture, written in the operational semantics style.Like many other ISA models, our RISC-V state object is a singlethreaded object and we prove read-over-write, write-over-write, writing-the-read, and state wellformedness theorems.Unlike some other models, we separate the instruction decoding functions from their semantic counterparts.Accordingly, we verify encoding / decoding functions for each RV32I instruction, the proofs for which are entirely automatic.
A copy is held
pdf, 240.6 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-09-22 14:27 UTC |
| Approved by | a person 2026-09-23 14:04 UTC |
Filed under
Cite it as
@article{kwan2025rv32i,
title = {RV32I in ACL2},
author = {Carl Kwan},
year = {2025},
journal = {Electronic Proceedings in Theoretical Computer Science},
publisher = {Open Publishing Association},
volume = {423},
pages = {46--50},
doi = {10.4204/eptcs.423.4},
}
This record lives at https://refs.drheap.org/kwan2025rv32i/ and will keep doing so.