RV32I in ACL2

TL;DR

This paper introduces a straightforward ACL2-based simulator for the RISC-V 32-bit ISA, featuring verified encoding/decoding functions and formal proofs of core state properties, enhancing formal verification tools for RISC-V implementations.

Contribution

It presents a simple, verified ACL2 simulator for RV32I with separated decoding functions and automatic proofs, improving formal modeling and verification of RISC-V.

Findings

Verified encoding/decoding functions for RV32I instructions

Proved key state properties like read-over-write and well-formedness

Separation of decoding from semantics enhances model clarity

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.