blob: 8dd7f437d00b91481fdbc7797528173f930bbbcc [file] [log] [blame] [view]
# Ibex RISC-V Core Wrapper DV document
## Goals
* Verify compliance with the RISC-V specifications used by OpenTitan.
* Verify Ibex's security hardening features.
* Ensure correct functionality is maintained across all possible behaviours of Ibex's external interfaces when integrated into OpenTitan.
* Verify additional features provided by the wrapper.
## Design features
`rv_core_ibex` wraps a dual core lockstep configuration of [Ibex](https://www.github.com/lowrisc/ibex), an RV32IMC CPU with security hardening features.
The wrapper adapts Ibex's top-level interfaces to be suitable for use with OpenTitan.
In addition rv_core_ibex provides some extra functionality controlled via bus accessible registers.
For more information please see the [Ibex RISC-V Core Wrapper Technical Specification](../README.md).
## Current Status
* Ibex Verification is tracked in the [Ibex documentation](https://ibex-core.readthedocs.io/en/latest/03_reference/verification_stages.html)
* Verification follows the OpenTitan [HW development stages](../../../../doc/project_governance/development_stages.md)
* [Nightly regression results](https://dev.azure.com/lowrisc/lowrisc-private/_build?definitionId=11)
* These are from the Ibex private-ci which is restricted to OpenTitan project members
## Verification strategy
The main Ibex testbench is not contained in the OpenTitan repository.
Verification is primarily done by the testbench in the Ibex repository, see the [Ibex Testplan](https://ibex-core.readthedocs.io/en/latest/03_reference/testplan.html) for more details.
The additional features provided by the RISC-V Core Wrapper are verified at a chip level only (See the [Earlgrey Chip DV testplan](../../../top_earlgrey/dv/README.md).
As they are simple features chip level only verification suffices to meet our goals.
Similarly there is no specific verification for the TL-UL <-> Ibex memory protocol wrappers (provided by the separate [TLUL IP](../../tlul/README.md)).
These are exercised extensively by all chip-level testing that runs software on Ibex providing comprehensive verification.
## Coverage
Due to the simplicity of the additional `rv_core_ibex` features, the existence of self checking chip-level tests combined with code and expression coverage is sufficient to be confident of their verification without functional coverpoints.
The TL-UL <-> Ibex memory protocol contains minimal logic so again code and expression coverage will suffice with one exception.
The iside and dside Ibex interfaces can have up to 8 or 2 outstanding requests respectively, we need to ensure these scenarios are seen.
An SVA cover expression will be used to produce coverage for this.