RV32I in ACL2
Logic in Computer Science
2025-07-28 v1
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 single-threaded object and we prove read-over-write, write-over-write, writing-the-read, and state well-formedness 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.
Cite
@article{arxiv.2507.19009,
title = {RV32I in ACL2},
author = {Carl Kwan},
journal= {arXiv preprint arXiv:2507.19009},
year = {2025}
}
Comments
In Proceedings ACL2 2025, arXiv:2507.18567