| .. _rvfi: |
| |
| RISC-V Formal Interface |
| ======================= |
| |
| Ibex supports the `RISC-V Formal Interface (RVFI) <https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md>`_. |
| This interface basically decodes the current instruction and provides additional insight into the core state thereby enabling formal verification. |
| Examples of such information include opcode, source and destination registers, program counter, as well as address and data for memory operations. |
| |
| |
| Formal Verification |
| ------------------- |
| |
| The signals provided by RVFI can be used to formally verify compliance of Ibex with the `RISC-V specification <https://riscv.org/specifications/>`_. |
| |
| Currently, the implementation is restricted to support the "I" and "C" extensions, and Ibex is not yet formally verified. |
| It predecessor "Zero-riscy" had been tested, but this required changes to the core as well as to the tool used in the process (`yosys <https://github.com/YosysHQ/yosys>`_). |
| The formal verification of the Ibex core is work in progress. |
