riscv-fs
riscv-coq
riscv-fs | riscv-coq | |
---|---|---|
2 | 1 | |
276 | 99 | |
- | - | |
4.1 | 5.8 | |
4 months ago | about 2 months ago | |
F# | Coq | |
MIT License | BSD 3-clause "New" or "Revised" 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-fs
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.
What are some alternatives?
Forvis_RISCV-ISA-Spec - Formal specification of RISC-V Instruction Set
sail-riscv - Sail RISC-V model
rtasm - Runtime Assembler for C++
RISC-V-Guide - RISC-V Guide. Learn all about the RISC-V computer architecture along with the Development Tools and Operating Systems to develop on RISC-V hardware.
riscv_em - Simple risc-v emulator, able to run linux, written in C.
RVVM - The RISC-V Virtual Machine
arduino-bl808 - Arduino Core for Bouffalo Labs's RISC-V BL808 SOC