mirror of
https://github.com/lowRISC/ibex.git
synced 2025-04-24 22:07:43 -04:00
830b7f7206
Restructure the existing documentation to group the content by intended audience. This produces four sections: * An introduction section, relevant to "newcomers" to Ibex. * An user guide, intended for hardware designers (integrators) and software developers who want to integrate Ibex, and develop software for it. * A reference guide, which provides background information on the design. This section is essential when working on Ibex, and also documents our design decisions. * A developer guide aimed at people modifying Ibex itself. It consists mostly of process and tool documentation: how to run the verification after a code change, how to use GitHub, etc. This commit is large, but text is mostly unchanged. A couple of introductions and tables of content were added, but no significant changes to the text have been made. These will be done in follow-ups. Signed-off-by: Philipp Wagner <phw@lowrisc.org>
18 lines
1 KiB
ReStructuredText
18 lines
1 KiB
ReStructuredText
.. _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.
|