github-mirrors/cve2
1
0
Fork 0
mirror of https://github.com/openhwgroup/cve2.git synced 2025-04-23 21:47:20 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

Doc: Adapt RVFI section, add connection in intro

Browse source
This commit is contained in:
Pirmin Vogel 2019-06-06 15:12:19 +01:00
parent b32078138c
commit d7810941e3
2 changed files with 8 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

3
doc/introduction.rst
View file

@ -46,9 +46,8 @@ The two register-file flavors are described in :ref:`register-file`.
The control and status registers are explained in :ref:`cs-registers`.
:ref:`performance-counters` gives an overview of the performance monitors and event counters available in Ibex.
:ref:`exceptions-interrupts` deals with the infrastructure for handling exceptions and interrupts,
:ref:`debug-support` gives a brief overview on the debug infrastructure.
For information regarding formal verification support, check out :ref:`rvfi`.
History

19
doc/rvfi.rst
View file

@ -3,21 +3,16 @@
RISC-V Formal Interface
=======================
Ibex is adapted to support the interface defined by RISC-V Formal Interface
(`riscv-formal <https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md>`_).
The signals provide an insight to the state of the core.
Generally speaking the interface decodes the current instruction.
This includes the opcode, the source and destination registers,
the program counter and for memory operations the memory location and data.
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 the adherents of
Ibex to the RISC-V `specification <https://riscv.org/specifications/>`_.
Currently the implementation is restricted to support the `I` and `C` extensions.
The signals provided by RVFI can be used to formally verify compliance of Ibex with the `RISC-V specification <https://riscv.org/specifications/>`_.
At the moment Ibex is not formally verified, a previous version (zero-riscy)
was tested, but this required changes to the core as well as to the tool used
in the process (`yosys <https://github.com/YosysHQ/yosys>`_). Support is work in progress.
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.