Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2507.19009 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909705169797120 |
|---|---|
| author | Kwan, Carl |
| author_facet | Kwan, Carl |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_19009 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | RV32I in ACL2 Kwan, Carl Logic in Computer Science 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. |
| title | RV32I in ACL2 |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.19009 |