[Haskell-cafe] Invititation to provide feedback on RISC-V ISA Formal Specs
nikhil at acm.org
Thu May 9 14:30:16 UTC 2019
The RISC-V Foundation (riscv.org) has a task group to develop a Formal
Spec for the RISC-V Instruction Set Architecture. The group has been
pursuing several approaches:
- 3 are written in Haskell
- 1 is in SAIL, a DSL with dependent types, intended for ISA specs
- 1 is in Kami, a DSL in Coq
Most of them are complete enough to boot Linux, i.e., they are not for
toy subsets of the ISA. They are expected and intended to become the
"official" ISA spec for RISC-V, and to be used in anger, for compliance
formal verification of compilers, hardware designs, etc.
We would love to get community feedback on these approaches. The
following link provides an overview, and links to individual web sites
(all on GitHub) for the 5 approaches, and information on how to provide
Thanks very much in advance!
Rishiyur Nikhil, Chair, ISA Formal Spec Technical Group
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe