References and related work
===========================

ARM's `ISA-Formal
Framework <https://alastairreid.github.io/papers/cav2016_isa_formal.pdf>`__
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 <https://riscv.org/wp-content/uploads/2016/07/Wed1130_Kami_Framework_Murali_Vijayaraghavan.pdf>`__
   (`kami on github <https://github.com/mit-plv/kami>`__)
-  `Rewrite of Kami by SiFive <https://github.com/sifive/Kami>`__
-  `Verifying a RISC-V Processor, Nirav Dave, Prashanth Mundkur, SRI
   International <https://riscv.org/wp-content/uploads/2015/06/riscv-verification-workshop-june2015.pdf>`__
   (`l3riscv on github <https://github.com/SRI-CSL/l3riscv>`__)
-  `RISC-V ISA Model in Bluespec BSV by Rishiyur S.
   Nikhil <https://github.com/rsnikhil/RISCV_ISA_Formal_Spec_in_BSV>`__
-  `RISC-V ISA Model in Haskell by Adam Chlipala and group
   (MIT) <https://github.com/mit-plv/riscv-semantics>`__
-  `RISC-V ISA Specification in Coq by MIT
   CSAIL <https://github.com/mit-plv/riscv-coq>`__
-  `RISC-V ISA Specification in Coq by
   SiFive <https://github.com/sifive/RiscvSpecFormal>`__
-  `RISC-V ISA specification work in Sail
   2 <https://github.com/riscv/sail-riscv>`__
-  `Sail: a language for describing instruction
   semantics <http://www.cl.cam.ac.uk/~pes20/sail/>`__
-  `riscv-fs: F# RISC-V Instruction Set formal
   specification <https://github.com/mrLSD/riscv-fs>`__

Please `open an
issue <https://github.com/YosysHQ/riscv-formal/issues/new>`__ if you
know of other RISC-V formal verification projects I should link to in
this section.
