riscv-coq
Forvis_RISCV-ISA-Spec
| riscv-coq | Forvis_RISCV-ISA-Spec | |
|---|---|---|
| 1 | 1 | |
| 99 | 96 | |
| - | - | |
| 5.8 | 10.0 | |
| 2 months ago | almost 4 years ago | |
| Coq | Haskell | |
| BSD 3-clause "New" or "Revised" License | MIT License |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
riscv-coq
-
RISC-V CPU formal specification F# edition
>it allows to formally verify the correctness of a particular ISA
That must be hypothetical. Functionalness of the language doesn't make anything that is written in it automatically subject to formal verification. (mechanized or pen and paper). What kind of correctness properties does it actually allow to formally verify? I understand if it was the F* language, which is a full blown dependently typed proof checker, but with F#, which is defined by the implementation and 300 page English spec, I don't think you can verify anything interesting. As far as I know F# itself doesn't have mechanized formal semantics and its type system could be unsound.
https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv (don't know how complete they are) approaches actually allow to formally (mechanically) verify riscv properties.
Forvis_RISCV-ISA-Spec
-
RISC-V CPU formal specification F# edition
I completely agree. And I specifically draw your attention to the fact that this is not a formal verification, which it would be reasonable to do: Coq, Isabellll, Agda, F* etc. However, Formal Specification. Those. representation of the specification in a formalized form. Haskell example: https://github.com/rsnikhil/Forvis_RISCV-ISA-Spec.
In this case, the term "formal" refers to the formalization of the representation of the specification. And it seems to be already established.
What are some alternatives?
sail-riscv - Sail RISC-V model
riscv-fs - F# RISC-V Instruction Set formal specification
rtasm - Runtime Assembler for C++