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.