<div dir="ltr"><div><br></div><div>A couple of years ago I wrote "Forvis", a "complete" semantics of the</div>RISC-V instruction set in "extremely elementary" Haskell.<br><br>It's free and open-source, at: <a href="https://github.com/rsnikhil/Forvis_RISCV-ISA-Spec">https://github.com/rsnikhil/Forvis_RISCV-ISA-Spec</a><br><br>"Extremely Elementary" Haskell: small subset of Haskell 98.  No<br>    type classes, no monads (except the top-level driver that uses<br>    standard IO), no GHC extensions, nothing.  Just vanilla function<br>    definitions and vanilla algebraic types (a "Miranda" subset).<br><br>    Motivation: appeal to hardware designers, compiler writers, and others<br><div>    who are keenly interested in a clearly readable and executable precise<br></div><div>    spec of RISC-V semantics, but are not at all interested in learning Haskell.<br></div><br>It's about 12K-13K lines of Haskell, all in one 'src/' directory.<br><br>Full "standard ISA" coverage:<br><br>- Unprivileged ISA:<br>    - RV32I (32-bit) and RV64I (64-bit) basic Integer instructions<br>    - Standard ISA extensions M (Integer Mult/Div), A (Atomics), C<br>        (Compressed) and FD (Single- and Double-precision floating<br>        point)<br><br>- Privileged ISA: Modes M (Machine), S (Supervisor) and U (User),<br>     including full complement of CSRs (Control and Status Registers).<br>     This includes full trap and interrupt handling, and RISC-V<br>     Virtual Memory schemes Sv32, Sv39 and Sv48.<br><br>I've tested it on all the standard RISC-V ISA tests (pass), booted a<br>Linux kernel (about 200 Million RISC-V Instructions), and the much<br>smaller real-time OS FreeRTOS.  I'm sure it'll work for any other<br>RISC-V software as well.  For this, the sources contain additional<br>code to package the "CPU" into a small "system", by adding Haskell<br>models of memory and a UART.<br><br><div>I haven't looked at it since early 2020, but it should all still work fine.</div><br>Nikhil<br></div>