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
testing,
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
feedback:
https://github.com/riscv/ISA_Formal_Spec_Public_Review
Thanks very much in advance!
Rishiyur Nikhil, Chair, ISA Formal Spec Technical Group
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
