diff --git a/docs/source/verification.rst b/docs/source/verification.rst index 34b33b09e..ceed0b5f3 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 @@ -146,12 +146,12 @@ 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 `_. +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 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -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.