Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-methods projects. Many verification, synthesis, programming, and debugging tools rely on formal semantics of instruction sets, but different tools can use semantics in rather different ways. The best-known work applying single semantics across diverse tools relies on domain-specific languages like Sail, where the language and its translation tools are specialized to the realm of instruction sets. In the context of the open RISC-V instruction-set family, we decided to explore a different approach, with semantics written in a carefully chosen subset of Haskell. This style does not depend on any new language translators, relying instead on parameterization of semantics over type-class instances. Our case study is for the open RISC-V instruction-set family, and we have used a single core semantics to support testing, interactive proof, and model checking of both software and hardware, demonstrating that this functional-programming feature can support pleasant prototyping of ISA semantics.
GitHub repositories: Haskell baseline and related Coq code