[libre-riscv-dev] formal verification
ogurksjnv at firemail.cc
ogurksjnv at firemail.cc
Tue Mar 19 23:30:55 GMT 2019
I think it's crucial to have compliance with the RISC-V specs.
If some day Simple-V get into production level, it is necessary
to have it. Some links:
Forvis:
https://github.com/rsnikhil/Forvis_RISCV-ISA-Spec
Sail-RISCV:
https://github.com/rems-project/sail-riscv
Clifford Wolf (developer of Icebreaker) RISCV-Semantics:
https://github.com/cliffordwolf/riscv-semantics
SymbioticEDA RISCV-Formal:
https://github.com/SymbioticEDA/riscv-formal
Check also:
hope-RIPE (I think it was used by DOVER, from Draper):
https://github.com/draperlaboratory/hope-RIPE
CRASH/SAFE (lots of formal specs made by INRIA):
http://www.crash-safe.org/
More information about the libre-riscv-dev
mailing list