diff --git a/docs/source/verification.rst b/docs/source/verification.rst index 944c00105..34b33b09e 100644 --- a/docs/source/verification.rst +++ b/docs/source/verification.rst @@ -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 `_. -Final functional, code and test coverage reports can be found `here `_. +Final functional, code and test coverage reports can be found `here `_. 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 @@ -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 `_. +Additional details are available as part of the `CV32E40P v1.0.0 Report `_. .. [1] It is a testament on the quality of the work done by the PULP platform team @@ -145,13 +145,13 @@ Verification environment is described in `CORE-V Verification Strategy `_ and `RISC-V ISA Formal Verification Plan `_. -Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports `_. +`Simulation Verification Plan `_ and `RISC-V ISA Formal Verification Plan `_. +Summary and all reports links (RTL code, functional, tests) can be found here: `CV32E40P v1.8.3 Verification Summary and Reports `_. It is to be mentioned that CV32E40Pv2 has successfully executed `RISCOF (RISC-V COmpatibility Framework) `_ for RV32IMCF extensions. -The official RISCOF reports can be found `here `_. +The official RISCOF reports can be found `here `_. -All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. +All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. RISC-V ISA Formal verification ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -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 `_. +A document explaining the RISC-V ISA Formal Verication methodology using Siemens Questa Processor tool can be found `here `_. Simulation verification ^^^^^^^^^^^^^^^^^^^^^^^ @@ -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 `_. +Properties status can be found in `CV32E40P v1.8.3 Report `_. 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.