riscv-formal-nmigen/README.md

# riscv-formal-nmigen

A port of [riscv-formal](https://github.com/SymbioticEDA/riscv-formal) to nMigen

## Dependencies

- [nMigen](https://github.com/m-labs/nmigen)
- [Yosys](https://github.com/YosysHQ/yosys)
- [SymbiYosys](https://github.com/YosysHQ/SymbiYosys)

## 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

### Minerva

`cd` to the root directory of this project and do:

```python
$ 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](./LICENSE)