On Thu, Jul 29, 2021 at 10:07 PM wrote:

[...] 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.

Thanks for that, I'll have a look. Stu