References and related work

ARM’s ISA-Formal Framework follows a similar set of ideas and has inspired the work on riscv-formal.

Other RISC-V formal verification projects and related materials:

• Kami: A Framework for (RISC-V) HW Verification (kami on github)

• Rewrite of Kami by SiFive

• Verifying a RISC-V Processor, Nirav Dave, Prashanth Mundkur, SRI International (l3riscv on github)

• RISC-V ISA Model in Bluespec BSV by Rishiyur S. Nikhil

• RISC-V ISA Model in Haskell by Adam Chlipala and group (MIT)

• RISC-V ISA Specification in Coq by MIT CSAIL

• RISC-V ISA Specification in Coq by SiFive

• RISC-V ISA specification work in Sail 2

• Sail: a language for describing instruction semantics

• riscv-fs: F# RISC-V Instruction Set formal specification

Please open an issue if you know of other RISC-V formal verification projects I should link to in this section.