[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