29 lines
1008 B
Markdown
29 lines
1008 B
Markdown
# riscv-formal-nmigen
|
|
|
|
A port of [riscv-formal](https://github.com/SymbioticEDA/riscv-formal) to nMigen
|
|
|
|
## Dependencies
|
|
|
|
- [nMigen](https://github.com/m-labs/nmigen)
|
|
|
|
## 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](https://github.com/lambdaconcept/minerva) core |
|
|
|
|
## Build
|
|
|
|
This framework is not ready to be used to verify RISC-V compliant cores at the time of writing. Instructions for running the framework against such a core will be added once the framework is ready for use.
|
|
|
|
## 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](./LICENSE)
|