.. Copyright 2024 OpenHW Group and Dolphin Design SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1 Licensed under the Solderpad Hardware License v 2.1 (the "License"); you may not use this file except in compliance with the License, or, at your option, the Apache License version 2.0. You may obtain a copy of the License at https://solderpad.org/licenses/SHL-2.1/ Unless required by applicable law or agreed to in writing, any work distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. .. _verification: Verification ============ The verification environment (testbenches, testcases, etc.) for the CV32E40P core can be found at `core-v-verif `_. It is recommended to start by reviewing the `CORE-V Verification Strategy `_. 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 `_. 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 RTL Freeze, a total of 47 RTL issues and 38 User Manual issues were identified and resolved [1]_. A breakdown of the RTL issues is as follows: .. table:: How RTL Issues Were Found in v1.0.0 :name: How RTL Issues Were Found in v1.0.0 :widths: 27 9 64 :class: no-scrollbar-table +---------------------+-----------+----------------------------------------------------+ | **"Found By"** | **Count** | **Note** | +=====================+===========+====================================================+ | Simulation | 18 | See classification below | +---------------------+-----------+----------------------------------------------------+ | Inspection | 13 | Human review of the RTL | +---------------------+-----------+----------------------------------------------------+ | Formal Verification | 13 | This includes both Designer and Verifier use of FV | +---------------------+-----------+----------------------------------------------------+ | Lint | 2 | | +---------------------+-----------+----------------------------------------------------+ | Unknown | 1 | | +---------------------+-----------+----------------------------------------------------+ A classification of the simulation issues by method used to identify them is informative: .. table:: Breakdown of Issues found by Simulation in v1.0.0 :name: Breakdown of Issues found by Simulation in v1.0.0 :widths: 27 9 64 :class: no-scrollbar-table +------------------------------+-----------+----------------------------------------------------------------------------------------+ | **Simulation Method** | **Count** | **Note** | +==============================+===========+========================================================================================+ | Directed, self-checking test | 10 | Many test supplied by Design team and a couple from the Open Source Community at large | +------------------------------+-----------+----------------------------------------------------------------------------------------+ | Step & Compare | 6 | Issues directly attributed to S&C against ISS | +------------------------------+-----------+----------------------------------------------------------------------------------------+ | Constrained-Random | 2 | Test generated by corev-dv (extension of riscv-dv) | +------------------------------+-----------+----------------------------------------------------------------------------------------+ A classification of the issues themselves: .. table:: Issue Classification in v1.0.0 :name: Issue Classification in v1.0.0 :widths: 27 9 64 :class: no-scrollbar-table +------------------------------+-----------+----------------------------------------------------------------------------------------+ | **Issue Type** | **Count** | **Note** | +==============================+===========+========================================================================================+ | RTL Functional | 40 | A bug! | +------------------------------+-----------+----------------------------------------------------------------------------------------+ | RTL coding style | 4 | Linter issues, removing TODOs, removing \`ifdefs, etc. | +------------------------------+-----------+----------------------------------------------------------------------------------------+ | Non-RTL functional | 1 | Issue related to behavioral tracer (not part of the core) | +------------------------------+-----------+----------------------------------------------------------------------------------------+ | Unreproducible | 1 | | +------------------------------+-----------+----------------------------------------------------------------------------------------+ | Invalid | 1 | | +------------------------------+-----------+----------------------------------------------------------------------------------------+ 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 that it took a team of professional verification engineers more than 9 months to find all these issues. .. raw:: latex \newpage v1.8.3 verification ------------------- The table below lists the 7 configurations with ``cv32e40p_top`` parameters values verified in the scope of CV32E40Pv2 project using both Formal-based and Simulation-based methodologies. .. table:: Verified configurations :name: Verified configurations :widths: 23 11 11 11 11 11 11 11 :class: no-scrollbar-table +--------------------+-------------------------------------------------------------------------+ | | **Verified Configurations (CFG_"config name")** | +====================+=======+==========+==========+==========+==========+==========+==========+ | **Top Parameters** | **P** | **P_F0** | **P_F1** | **P_F2** | **P_Z0** | **P_Z1** | **P_Z2** | +--------------------+-------+----------+----------+----------+----------+----------+----------+ | COREV_PULP | 1 | 1 | 1 | 1 | 1 | 1 | 1 | +--------------------+-------+----------+----------+----------+----------+----------+----------+ | COREV_CLUSTER | 0 | 0 | 0 | 0 | 0 | 0 | 0 | +--------------------+-------+----------+----------+----------+----------+----------+----------+ | FPU | 0 | 1 | 1 | 1 | 1 | 1 | 1 | +--------------------+-------+----------+----------+----------+----------+----------+----------+ | ZFINX | 0 | 0 | 0 | 0 | 1 | 1 | 1 | +--------------------+-------+----------+----------+----------+----------+----------+----------+ | FPU_ADDMUL_LAT | 0 | 0 | 1 | 2 | 0 | 1 | 2 | +--------------------+-------+----------+----------+----------+----------+----------+----------+ | FPU_OTHERS_LAT | 0 | 0 | 1 | 2 | 0 | 1 | 2 | +--------------------+-------+----------+----------+----------+----------+----------+----------+ Verification environment is described in `CORE-V Verification Strategy `_ and used the so-called `Step-and-Compare 2.0 `_ methodology. It is using an Imperas® model connected in the test-bench through an RVVI interface as shown by following figure: .. figure:: ../images/ImperasDV_diagram_May_2023-reduced.jpg :name: ImperasDV framework :align: center 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 `_ 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 `_. All issues (User Manual or RTL) mentioned below can be found at `CV32E40Pv2 Design Issues Summary `_. RISC-V ISA Formal verification ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ To accelerate the verification of more than 300 XPULP instructions, RISC-V ISA Formal Verification methodology has been used with Siemens Questa Processor tool and its RISC-V ISA Processor Verification app. The XPULP instructions pseudo-code description using Sail language have been added to the RISC-V ISA app to successfully formally verify all the CV32E40P instructions, including the previously verified standard IMC together with the new F, Zfinx and XPULP extensions and all additional custom CSRs. Example: .. code-block:: text { "name": "CV.SDOTUP.B", "disassembly": "cv.sdotup.b {rd},{rs1},{rs2}", "decoding": "1001100 rs2 rs1 001 rd/rs3 1111011", "restrictions": "", "execution": "X(rd) = X(rs3) + EXTZ(mul(X(rs1)[7..0],X(rs2)[7..0])) + EXTZ(mul(X(rs1)[15..8],X(rs2)[15..8])) + EXTZ(mul(X(rs1)[23..16],X(rs2)[23..16])) + EXTZ(mul(X(rs1)[31..24],X(rs2)[31..24]))" }, Those SAIL instructions description are then used to automatically generate assertions and CSRs descriptions that are grouped by classes. Additionally to those instructions and CSR assertions there are some of them to check specific features (e.g. OBI interfaces protocol, legal CSRs reset values..). So globally it is resulting in 198 assertions to be checked on the 7 different configurations listed in :ref:`Verified configurations` table. 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 `_. Simulation verification ^^^^^^^^^^^^^^^^^^^^^^^ core-v-verif verification environment for v1.0.0 was using a *step&compare* methodology with an instruction set simulator (ISS) from Imperas Software as the reference model. This strategy was successful, but inefficient because the *step&compare* logic in the testbench must compensate for the cycle-time effects of events that are asynchronous to the instruction stream such as interrupts, debug resets plus bus errors and random delays on instruction fetch and load/store memory buses. For verification of v1.8.3 release of the CV32E40P core, the step-and-compare and the ISS have been replaced by a true reference model (RM) called ImperasDV. In addition, the Imperas Reference Model has been extended to support the v2 XPULP instructions specification. Another innovation for v1.8.3 was the adoption of a standardized interface to the DUT and RM, based on the open-source RISC-V Verification Interface (RVVI). The use of well documented, standardized interfaces greatly simplifies the integration of the DUT with the RM. 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 `_. 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. Here is the breakdown of all the issues: .. table:: How Issues Were Found in v1.8.3 :name: How Issues Were Found in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table +--------------------------------+-----------+---------------------------------------------------------------+ | **"Found By"** | **Count** | **Note** | +================================+===========+===============================================================+ | RISC-V ISA Formal Verification | 30 | All related to features enabled by ``COREV_PULP`` or ``FPU``. | +--------------------------------+-----------+---------------------------------------------------------------+ | Simulation | 20 | Details below | +--------------------------------+-----------+---------------------------------------------------------------+ | Lint/RTL Code review | 4 | | +--------------------------------+-----------+---------------------------------------------------------------+ A classification of the RISC-V ISA Formal Verification issues by type and their description are listed in the following tables: .. table:: Breakdown of Issues found by RISC-V ISA Formal Verification in v1.8.3 :name: Breakdown of Issues found by RISC-V ISA Formal Verification in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table +------------------------------+-----------+----------------------------------------------------------------------------------------+ | **Type** | **Count** | **Note** | +==============================+===========+========================================================================================+ | User Manual | 12 | Instructions description leading to mis-interpretation | +------------------------------+-----------+----------------------------------------------------------------------------------------+ | RTL bugs | 18 | Details below | +------------------------------+-----------+----------------------------------------------------------------------------------------+ .. table:: RISC-V ISA Formal Verification Issues Classification in v1.8.3 :name: RISC-V ISA Formal Verification Issues Classification in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table +--------------------------------+-----------+---------------------------------------------------------------------------------------+ | **Issue Type** | **Count** | **Note** | +================================+===========+=======================================================================================+ | Illegal instructions exception | 5 | F and XPULP instructions corner cases or CSR accesses not flagged as Illegal | | | | instructions exception. | +--------------------------------+-----------+---------------------------------------------------------------------------------------+ | Multi-cycle F instructions | 8 | FDIV, FSQRT or all F instructions when FPU_ADDMUL_LAT/FPU_OTHERS_LAT = 2 are executed | | | | in the background and the pipeline can continue to execute other instructions | | | | as long as there is no Read-After-Write or Write-After-Write dependency. | | | | When the multi-cycle F instructions are finally writing back their result in the | | | | Register File, this register update can corrupt on-going instructions behaviour or | | | | result. This is the case for Misaligned Loads, Post-Incremented Load/Stores, MULH, | | | | JALR or cv.add*NR/cv.sub*NR. | +--------------------------------+-----------+---------------------------------------------------------------------------------------+ | F instructions result or flags | 5 | F result or flags computations is incorrect with respect to IEEE 754-2008 standard. | +--------------------------------+-----------+---------------------------------------------------------------------------------------+ A classification of the Simulation issues by type and their description are listed in the following tables: .. table:: Breakdown of Issues found by Simulation in v1.8.3 :name: Breakdown of Issues found by Simulation in v1.8.3 :widths: 27 9 64 :class: no-scrollbar-table +------------------------------+-----------+----------------------------------------------------------------------------------------+ | **Type** | **Count** | **Note** | +==============================+===========+========================================================================================+ | RTL bugs | 20 | See classification below | +------------------------------+-----------+----------------------------------------------------------------------------------------+ .. table:: Simulation Issues Classification in v1.8.3 :name: Simulation Issues Classification in v1.8.3 :widths: 38 9 53 :class: no-scrollbar-table +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | **Issue Type** | **Count** | **Note** | +==========================================+===========+=======================================================================================+ | Multi-cycle F instructions | 5 | Data forward violation between muticycle F instructions and XPULP instructions. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Hardware Loops | 4 | Conflict between CSR write and cv.lp* instructions. | | | | | | | | Incorrect behavior when count programmed with 0 value. | | | | | | | | lpcountX not decremented to 0 at the end of HWloop execution. | | | | | | | | lpcountX not updated after a pipeline flush due to a CSR access. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Illegal instructions exception | 3 | Illegal immediates values | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Incorrect Register file control | 1 | When ZFINX = 1 | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | MIMPID incorrect value | 1 | Value depending of FPU, COREV_PULP and COREV_CLUSTER paremeters. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Deadlock | 1 | Bug resolution for multicycle F instructions created a deadlock when conflicting | | | | Register File write between FPU and ALU. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | MSTATUS.FS incorrect value | 1 | FS was not updated following any Floating Point Load instruction. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Unnecessary multiple Register File write | 1 | Removed redundant Register File writes. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | Missing or unreacheable case defaults | 2 | Found with RTL Code coverage holes analysis. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ | FPU unnecessary clock enable | 1 | Finer grain clock gating generation. | +------------------------------------------+-----------+---------------------------------------------------------------------------------------+ Tracer ------ The module ``cv32e40p_rvfi_trace`` can be used to create a log of the executed instructions. It is a behavioral, non-synthesizable, module instantiated in the example testbench that is provided for the ``cv32e40p_top``. It can be enabled during simulation by defining **CV32E40P_RVFI_TRACE_EXECUTION**. Output file ^^^^^^^^^^^ All traced instructions are written to a log file. The log file is named ``trace_core.log``. Trace output format ^^^^^^^^^^^^^^^^^^^ The trace output is in tab-separated columns. 1. **Time**: The current simulation time. 2. **Cycle**: The number of cycles since the last reset. 3. **PC**: The program counter 4. **Instr**: The executed instruction (base 16). 32 bit wide instructions (8 hex digits) are uncompressed instructions, 16 bit wide instructions (4 hex digits) are compressed instructions. 5. **Ctx**: When an illegal instruction is cancelled, this field shows (C) information together with the instruction which caused cancellation. 6. **Decoded instruction**: The decoded (disassembled) instruction in a format equal to what objdump produces when calling it like ``objdump -Mnumeric -Mno-aliases -D``. - Unsigned numbers are given in hex (prefixed with ``0x``), signed numbers are given as decimal numbers. - Numeric register names are used (e.g. ``x1``). - Symbolic CSR names are used. - Jump/branch targets are given as absolute address if possible (PC + immediate). 7. **Register and memory contents**: For all accessed registers, the value before and after the instruction execution is given. Writes to registers are indicated as ``registername=value``, reads as ``registername:value``. For memory accesses, the physical address (PA) of the loaded or stored data is reported as well. 8. **Stop cycle Stop time**: For long multi-cycle instructions like Floating-Point Division or Square-root, these columns are indicating when the result and the flags are returned by the FPU. .. code-block:: text Time Cycle PC Instr Ctx Decoded instruction Register and memory contents Stop cycle Stop time 130.000 ns 61 00000150 4481 c.li x9,0 x9=0x00000000 132.000 ns 62 00000152 00008437 lui x8,0x8 x8=0x00008000 134.000 ns 63 00000156 fff40413 addi x8,x8,-1 x8=0x00007fff x8:0x00008000 136.000 ns 64 0000015a 18e50353 fdiv.s f6, f10, f14 f6=59463c68 f10:990dcef4 f14:8016e429 67 142.000 ns 138.000 ns 65 0000015c 8c65 c.and x8,x9 x8=0x00000000 x8:0x00007fff x9:0x00000000 142.000 ns 67 0000015e c622 c.swsp x8,12(x2) x2:0x00002000 x8:0x00000000 PA:0x0000200c 144.000 ns 68 00000160 36067a73 (C) csrrci x0, 0x00000000, 0x360 152.000 ns 72 00033200 0800006f jal x0, 128