Skip to content

Commit

Permalink
All links updated to cv32e40p_v1.8.3 tag for the 3 target repos (core…
Browse files Browse the repository at this point in the history
…-v-docs, cv32e40p, core-v-verif).

Signed-off-by: Pascal Gouedo <pascal.gouedo@dolphin.fr>
  • Loading branch information
Pascal Gouedo committed Jul 11, 2024
1 parent c998590 commit c0823cf
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions docs/source/verification.rst
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ v1.0.0 verification

In early 2021 the CV32E40P achieved Functional RTL Freeze (released with cv32e40p_v1.0.0 version), meaning that is has been fully verified as per its
`Verification Plan <https://github.com/openhwgroup/core-v-verif/blob/cb2cc35fe27e0961ea21864f62e6104c238d25cd/cv32e40p/docs/VerifPlans/README.md#cv32e40p-v1-verification-plans>`_.
Final functional, code and test coverage reports can be found `here <https://github.com/openhwgroup/programs/tree/master/Project-Descriptions-and-Plans/CV32E40Pv1/Milestone-data/Reports>`_.
Final functional, code and test coverage reports can be found `here <https://github.com/openhwgroup/core-v-docs/tree/master/Project-Descriptions-and-Plans/CV32E40Pv1/Milestone-data/Reports>`_.

The unofficial start date for the CV32E40P verification effort is 2020-02-27,
which is the date the core-v-verif environment "went live". Between then and
Expand Down Expand Up @@ -97,7 +97,7 @@ A classification of the issues themselves:
| Invalid | 1 | |
+------------------------------+-----------+----------------------------------------------------------------------------------------+

Additional details are available as part of the `CV32E40P v1.0.0 Report <https://github.com/openhwgroup/programs/tree/b72d726665b31b3df5befc5f672b745f814ea709/Project-Descriptions-and-Plans/CV32E40Pv1/Milestone-data/RTL_Freeze_v1.0.0>`_.
Additional details are available as part of the `CV32E40P v1.0.0 Report <https://github.com/openhwgroup/core-v-docs/tree/b72d726665b31b3df5befc5f672b745f814ea709/Project-Descriptions-and-Plans/CV32E40Pv1/Milestone-data/RTL_Freeze_v1.0.0>`_.

.. [1]
It is a testament on the quality of the work done by the PULP platform team
Expand Down Expand Up @@ -145,13 +145,13 @@ Verification environment is described in `CORE-V Verification Strategy <https://
ImperasDV framework

CV32E40Pv2 achieved RTL Freeze (released with cv32e40p_v1.8.3 version) end of June 2024, meaning that is has been fully verified as per its
`Simulation Verification Plan <https://github.com/openhwgroup/core-v-verif/tree/cv32e40p/dev/cv32e40p/docs/VerifPlans/README.md>`_ and `RISC-V ISA Formal Verification Plan <https://github.com/openhwgroup/core-v-verif/tree/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx>`_.
Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports <https://github.com/openhwgroup/programs/blob/master/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3//index.html>`_.
`Simulation Verification Plan <https://github.com/openhwgroup/core-v-verif/blob/cv32e40p_v1.8.3/cv32e40p/docs/VerifPlans/README.md>`_ and `RISC-V ISA Formal Verification Plan <https://github.com/openhwgroup/core-v-verif/blob/cv32e40p_v1.8.3/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_Formal_VerificationPlans.xlsx>`_.
Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports <https://github.com/openhwgroup/core-v-docs/blob/cv32e40p_v1.8.3/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3/index.html>`_.

It is to be mentioned that CV32E40Pv2 has successfully executed `RISCOF (RISC-V COmpatibility Framework) <https://riscof.readthedocs.io/en/stable>`_ for RV32IMCF extensions.
The official RISCOF reports can be found `here <https://github.com/openhwgroup/programs/tree/master/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3/Reports/RISCOF>`_.
The official RISCOF reports can be found `here <https://github.com/openhwgroup/core-v-docs/tree/cv32e40p_v1.8.3/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3/Reports/RISCOF>`_.

All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary <https://github.com/openhwgroup/programs/blob/master/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3/CV32E40Pv2_Design_Issue_Summary.xlsx>`_.
All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary <https://github.com/openhwgroup/core-v-docs/blob/cv32e40p_v1.8.3/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3/CV32E40Pv2_Design_Issue_Summary.xlsx>`_.

RISC-V ISA Formal verification
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Expand Down Expand Up @@ -180,7 +180,7 @@ So globally it is resulting in 198 assertions to be checked on the 7 different c

RTL code coverage is generated using Siemens Questa Processor Quantify tool which uses RTL mutation to check assertions quality and can produce standard UCDB database that can be merged with simulation ones afterwards.

A document explaining the RISC-V ISA Formal Verication methodology using Siemens Questa Processor tool can be found `here <https://github.com/openhwgroup/core-v-verif/tree/cv32e40p/dev/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_RISCV_vPlan_v1.1.pdf>`_.
A document explaining the RISC-V ISA Formal Verication methodology using Siemens Questa Processor tool can be found `here <https://github.com/openhwgroup/core-v-verif/blob/cv32e40p_v1.8.3/cv32e40p/docs/VerifPlans/RISC-V_ISA_Formal/CV32E40Pv2_RISCV_vPlan_v1.1.pdf>`_.

Simulation verification
^^^^^^^^^^^^^^^^^^^^^^^
Expand All @@ -196,7 +196,7 @@ Results summary

RISC-V ISA Formal Verification has been successfully launched on intermediate RTL versions of the 7 different configurations.
On v1.8.3 RTL tag, only PULP (CFG_P) and PULP with FPU (CFG_P_F0) configurations were fully proven, nearly all properties being unbounded hold, some being bounded hold with a high number of cycles.
Properties status can be found in `CV32E40P v1.8.3 Report <https://github.com/openhwgroup/programs/tree/master/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3/Reports/RISC-V_ISA_Formal/Property_Status-v1_8_3.xlsx>`_.
Properties status can be found in `CV32E40P v1.8.3 Report <https://github.com/openhwgroup/core-v-docs/blob/cv32e40p_v1.8.3/Project-Descriptions-and-Plans/CV32E40Pv2/Milestone-data/RTL_v1.8.3/Reports/RISC-V_ISA_Formal/Property_Status-v1_8_3.xlsx>`_.

30 issues were identified by Formal Verification, 20 by Simulation methodologies and 4 by Lint/RTL code review, all have been resolved except 1 about Lint warnings.

Expand Down

0 comments on commit c0823cf

Please sign in to comment.