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