A port of [riscv-formal](https://github.com/SymbioticEDA/riscv-formal) to nMigen
rvfi | ||
LICENSE | ||
README.md |
riscv-formal-nmigen
A port of riscv-formal to nMigen
Dependencies
Breakdown
Directory | Description |
---|---|
rvfi |
RISC-V Formal Verification Framework (nMigen port) |
rvfi/insns |
Supported RISC-V instructions and ISAs |
rvfi/cores |
Example cores to be integrated with riscv-formal-nmigen (WIP) |
rvfi/cores/minerva |
The Minerva core |
Build
Minerva
cd
to the root directory of this project and do:
$ python -m rvfi.cores.minerva.verify
Scope
Support for the RV32I base ISA and RV32M extension are planned and well underway. Support for other ISAs in the original riscv-formal such as RV32C and their 64-bit counterparts may also be added in the future as time permits.
License
See LICENSE