From aef99830347c6ffd825145a4fb0561f81f7f7bf0 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Tue, 9 Apr 2024 14:47:35 +0200 Subject: [PATCH 1/4] Updated incorrect table names. Signed-off-by: Pascal Gouedo --- docs/source/instruction_set_extensions.rst | 30 +++++++++++----------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/docs/source/instruction_set_extensions.rst b/docs/source/instruction_set_extensions.rst index b669e2836..15513c974 100644 --- a/docs/source/instruction_set_extensions.rst +++ b/docs/source/instruction_set_extensions.rst @@ -1019,7 +1019,7 @@ Immediate Branching Encoding ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ .. table:: Immediate Branching encoding - :name: General ALU operations encoding + :name: Immediate Branching encoding :widths: 13 14 8 6 8 12 12 11 16 :class: no-scrollbar-table @@ -1046,8 +1046,8 @@ The custom multiply-accumulate extensions are only supported if ``COREV_PULP`` = 16-Bit x 16-Bit Multiplication operations ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -.. table:: 16-Bit Multiplication operations - :name: 16-Bit Multiplication operations +.. table:: 16-Bit x 16-Bit Multiplication operations + :name: 16-Bit x 16-Bit Multiplication operations :widths: 30 70 :class: no-scrollbar-table @@ -1099,8 +1099,8 @@ The custom multiply-accumulate extensions are only supported if ``COREV_PULP`` = 16-Bit x 16-Bit Multiplication pseudo-instructions ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -.. table:: 16-Bit Multiplication pseudo-instructions - :name: 16-Bit Multiplication pseudo-instructions +.. table:: 16-Bit x 16-Bit Multiplication pseudo-instructions + :name: 16-Bit x 16-Bit Multiplication pseudo-instructions :widths: 23 27 50 :class: no-scrollbar-table @@ -1127,8 +1127,8 @@ The custom multiply-accumulate extensions are only supported if ``COREV_PULP`` = 16-Bit x 16-Bit Multiply-Accumulate operations ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -.. table:: 16-Bit Multiply-Accumulate operations - :name: 16-Bit Multiply-Accumulate operations +.. table:: 16-Bit x 16-Bit Multiply-Accumulate operations + :name: 16-Bit x 16-Bit Multiply-Accumulate operations :widths: 30 70 :class: no-scrollbar-table @@ -1179,8 +1179,8 @@ The custom multiply-accumulate extensions are only supported if ``COREV_PULP`` = 32-Bit x 32-Bit Multiply-Accumulate operations ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -.. table:: 32-Bit Multiply-Accumulate operations - :name: 32-Bit Multiply-Accumulate operations +.. table:: 32-Bit x 32-Bit Multiply-Accumulate operations + :name: 32-Bit x 32-Bit Multiply-Accumulate operations :widths: 30 70 :class: no-scrollbar-table @@ -1195,8 +1195,8 @@ The custom multiply-accumulate extensions are only supported if ``COREV_PULP`` = Encoding ^^^^^^^^ -.. table:: 16-Bit Multiplication operations - :name: 16-Bit Multiplication operations +.. table:: 16-Bit x 16-Bit Multiplication encoding + :name: 16-Bit x 16-Bit Multiplication encoding :widths: 5 16 6 6 9 6 11 39 :class: no-scrollbar-table @@ -1222,8 +1222,8 @@ Encoding | 11 | Luimm5[4:0] | src2 | src1 | 100 | dest | 101 1011 | **cv.mulhhsRN rD, rs1, rs2, Is3** | +--------+---------------+---------+---------+------------+--------+------------+------------------------------------+ -.. table:: 16-Bit Multiply-Accumulate operations - :name: 16-Bit Multiply-Accumulate operations +.. table:: 16-Bit x 16-Bit Multiply-Accumulate encoding + :name: 16-Bit x 16-Bit Multiply-Accumulate encoding :widths: 5 16 6 6 9 6 11 39 :class: no-scrollbar-table @@ -1249,8 +1249,8 @@ Encoding | 11 | Luimm5[4:0] | src2 | src1 | 110 | dest | 101 1011 | **cv.machhsRN rD, rs1, rs2, Is3** | +--------+---------------+---------+---------+------------+--------+------------+------------------------------------+ -.. table:: 32-Bit Multiply-Accumulate operations - :name: 32-Bit Multiply-Accumulate operations +.. table:: 32-Bit x 32-Bit Multiply-Accumulate encoding + :name: 32-Bit x 32-Bit Multiply-Accumulate encoding :widths: 21 6 6 9 6 11 39 :class: no-scrollbar-table From f2cd0b4def31b257e3facf010f3f5111cb9365bd Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Tue, 9 Apr 2024 14:48:19 +0200 Subject: [PATCH 2/4] Added missing paragraph carriage return. Signed-off-by: Pascal Gouedo --- docs/source/pipeline.rst | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/source/pipeline.rst b/docs/source/pipeline.rst index 971a0a9e1..8cbf907e9 100644 --- a/docs/source/pipeline.rst +++ b/docs/source/pipeline.rst @@ -47,6 +47,7 @@ Execute (EX) * There is a multi-cycle MULH in EX. * There is a Misaligned LOAD/STORE in EX. * There is a Post-Increment LOAD/STORE in EX. + In those 3 exceptions, EX will not be stalled, FPU result (and flags) are memorized and will be written back in the register file (and FPU CSR) as soon as there is no conflict anymore. Writeback (WB) From 5aa98cb3f225c876a779134ab01585f7ad03e361 Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Tue, 9 Apr 2024 17:13:42 +0200 Subject: [PATCH 3/4] Forbid floating figures. Signed-off-by: Pascal Gouedo --- docs/source/conf.py | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/source/conf.py b/docs/source/conf.py index 53badd35b..803228d89 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -164,6 +164,7 @@ # Latex figure (float) alignment # # 'figure_align': 'htbp', + 'figure_align': 'H', } # Grouping the document tree into LaTeX files. List of tuples From d6d94f461e957f5d4dab1b3fc053a1a1acd4db2c Mon Sep 17 00:00:00 2001 From: Pascal Gouedo Date: Tue, 9 Apr 2024 17:14:22 +0200 Subject: [PATCH 4/4] Updated Verification section. Signed-off-by: Pascal Gouedo --- docs/source/verification.rst | 241 ++++++++++++++++++----------------- 1 file changed, 121 insertions(+), 120 deletions(-) diff --git a/docs/source/verification.rst b/docs/source/verification.rst index afc645886..56d71a834 100644 --- a/docs/source/verification.rst +++ b/docs/source/verification.rst @@ -1,19 +1,19 @@ .. - Copyright (c) 2023 OpenHW Group - - Licensed under the Solderpad Hardware Licence, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. + 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/ + https://solderpad.org/licenses/SHL-2.1/ - Unless required by applicable law or agreed to in writing, software + 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. - - SPDX-License-Identifier: Apache-2.0 WITH SHL-2.0 .. _verification: @@ -29,8 +29,8 @@ 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 `_. +`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 @@ -97,45 +97,106 @@ 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 - that it took a team of professonal verification engineers more than 9 months + that it took a team of professional verification engineers more than 9 months to find all these issues. +.. raw:: latex + + \newpage + v2.0.0 verification ------------------- -The table below lists the 9 configurations with ``cv32e40p_top`` parameters values verified in the scope of CV32E40Pv2 project using both Formal-based and Simulation-based methodologies. +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 :align: center + :widths: 23 11 11 11 11 11 11 11 :class: no-scrollbar-table - +--------------------+-----------------------------------+ - | **Top Parameters** | **Verified Configurations** | - +====================+===+===+===+===+===+===+===+===+===+ - | COREV_PULP | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | - +--------------------+---+---+---+---+---+---+---+---+---+ - | COREV_CLUSTER | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | - +--------------------+---+---+---+---+---+---+---+---+---+ - | FPU | 0 | 1 | 1 | 1 | 1 | 1 | 1 | 0 | 1 | - +--------------------+---+---+---+---+---+---+---+---+---+ - | ZFINX | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 0 | 1 | - +--------------------+---+---+---+---+---+---+---+---+---+ - | FPU_ADDMUL_LAT | 0 | 0 | 1 | 2 | 0 | 1 | 2 | 0 | 2 | - +--------------------+---+---+---+---+---+---+---+---+---+ - | FPU_OTHERS_LAT | 0 | 0 | 1 | 2 | 0 | 1 | 2 | 0 | 2 | - +--------------------+---+---+---+---+---+---+---+---+---+ - -A total of resp. 30 and xx RTL issues were identified by resp. Formal Verification and Simulation methodologies, all have been resolved. + +--------------------+-------------------------------------------------------------------------+ + | | **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 -A breakdown of the RTL issues is as follows: + ImperasDV framework + +CV32E40Pv2 achieved RTL Freeze (released with cv32e40p_v2.0.0 version) mid-April 2024, meaning that is has been fully verified as per its +`Verification Plan `_. +Final functional, code and test coverage reports can be found here: `CV32E40P v2.0.0 Report `_. + +It is to be mentioned that CV32E40Pv2 has successfully executed `RISCOF (RISC-V COmpatibility Framework) `_ for RV32IMCF extensions. +Report can be found `here `_. + +Formal verification +^^^^^^^^^^^^^^^^^^^ + +To accelerate the verification of more than 300 XPULP instructions, Formal Verification methodology has been used with Siemens EDA Onespin 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 more than 430 assertions and 29 CSRs descriptions. +Those assertions have been applied on the 7 different configurations listed in :ref:`Verified configurations` table. + +RTL code coverage is generated using Siemens EDA Onespin Quantify tool which uses RTL mutation to check assertions quality and can produce standard UCDB database that can be merged with simulation one afterwards. + +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 v2.0.0 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 v2.0.0 was the adoption of a standardized tracer 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 +^^^^^^^^^^^^^^^ -.. table:: How RTL Issues Were Found in v2.0.0 - :name: How RTL Issues Were Found in v2.0.0 +30 issues were identified by Formal Verification and 10 by Simulation methodologies, all have been resolved. + +Here is the breakdown of all the issues: + +.. table:: How Issues Were Found in v2.0.0 + :name: How Issues Were Found in v2.0.0 :widths: 27 9 64 :class: no-scrollbar-table @@ -144,12 +205,12 @@ A breakdown of the RTL issues is as follows: +=====================+===========+===============================================================+ | Formal Verification | 30 | All related to features enabled by ``COREV_PULP`` or ``FPU``. | +---------------------+-----------+---------------------------------------------------------------+ - | Simulation | | | + | Simulation | 10 | | +---------------------+-----------+---------------------------------------------------------------+ - | Lint | | | + | Lint | 2 | | +---------------------+-----------+---------------------------------------------------------------+ -A classification of the Formal Verification issues by type and their description are listed in the two following tables: +A classification of the Formal Verification issues by type and their description are listed in the following tables: .. table:: Breakdown of Issues found by Formal Verification in v2.0.0 :name: Breakdown of Issues found by Formal Verification in v2.0.0 @@ -186,7 +247,7 @@ A classification of the Formal Verification issues by type and their description | 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 method used to identify them is informative: +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 v2.0.0 :name: Breakdown of Issues found by Simulation in v2.0.0 @@ -194,92 +255,32 @@ A classification of the simulation issues by method used to identify them is inf :class: no-scrollbar-table +------------------------------+-----------+----------------------------------------------------------------------------------------+ - | **Simulation Method** | **Count** | **Note** | + | **Type** | **Count** | **Note** | +==============================+===========+========================================================================================+ - | Directed, self-checking test | | Many test supplied by Design team and a couple from the Open Source Community at large | - +------------------------------+-----------+----------------------------------------------------------------------------------------+ - | RVFI/RVVI | | Issues directly attributed to comparison against Reference Model | - +------------------------------+-----------+----------------------------------------------------------------------------------------+ - | Constrained-Random | | Test generated by corev-dv (extension of riscv-dv) | + | RTL bugs | 10 | See classification below | +------------------------------+-----------+----------------------------------------------------------------------------------------+ - -A classification of the Simulation issues themselves: - -.. table:: Simulation Issue Classification in v2.0.0 - :name: Simulation Issue Classification in v2.0.0 - :widths: 27 9 64 +.. table:: Simulation Issues Classification in v2.0.0 + :name: Simulation Issues Classification in v2.0.0 + :widths: 38 9 53 :class: no-scrollbar-table - +------------------------------+-----------+----------------------------------------------------------------------------------------+ - | **Issue Type** | **Count** | **Note** | - +==============================+===========+========================================================================================+ - | RTL Functional bug | | | - +------------------------------+-----------+----------------------------------------------------------------------------------------+ - | | | | - +------------------------------+-----------+----------------------------------------------------------------------------------------+ - -Formal verification -^^^^^^^^^^^^^^^^^^^ - -To accelerate the verification of more than 300 Xpulp instructions, Formal Verification methodology has been used with Siemens EDA Onespin tools 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 more than 430 assertions and 29 CSRs descriptions. -Those assertions have been applied on the 9 different configurations listed in :ref:`Verified configurations` table. - -RTL code coverage is generated using Siemens EDA Onespin Quantify tool which uses RTL mutation to check assertions quality and can produce standard UCDB database that can be merged with simulation one afterwards. - -WIP... - -.. ADD PLANS AND REPORTS LINKS - -.. Formal Verification assertions and RTL code coverage reports can be found `here `_. - -.. TO DEVELOP ... - -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 v2.0.0 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 v2.0.0 was the adoption of a standardized tracer 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. - -Additionaly to V1 Verification plans, `Verification Plan `_ contains a `new section `_ related to F and XPULP verification. - -WIP... - -.. ADD REPORTS LINKS - -.. TO DEVELOP ... - -Reports -^^^^^^^ - -WIP... - -.. ADD BUG LIST LINK AND TABLE LIKE ABOVE - -.. ADD MERGED RTL CODE COVERAGE GENERATED REPORTS LINK - + +--------------------------------+-----------+---------------------------------------------------------------------------------------+ + | **Issue Type** | **Count** | **Note** | + +================================+===========+=======================================================================================+ + | Multi-cycle F instructions | 5 | Data forward violation between XPULP instructions and muticycle F instructions. | + +--------------------------------+-----------+---------------------------------------------------------------------------------------+ + | Hardware Loops | 3 | Incorrect behavior when count programmed with 0 value. | + | | | | + | | | lpendX CSR updated by a cancelled instruction. | + | | | | + | | | lpcountX not updated after a pipeline flush due to a CSR access. | + +--------------------------------+-----------+---------------------------------------------------------------------------------------+ + | Deadlock | 1 | Bug resolution for multicycle F instructions created a deadlock when conflicting | + | | | Register File write between ALU and FPU. | + +--------------------------------+-----------+---------------------------------------------------------------------------------------+ + | MSTATUS.FS incorrect value | 1 | FS was not updated following any Floating Point Load instruction. | + +--------------------------------+-----------+---------------------------------------------------------------------------------------+ Tracer ------ @@ -292,7 +293,7 @@ Output file ^^^^^^^^^^^ All traced instructions are written to a log file. -The log file is named ``trace_core_.log``, with ```` being the 32 digit hart ID of the core being traced. +The log file is named ``trace_core.log``. Trace output format ^^^^^^^^^^^^^^^^^^^ @@ -309,7 +310,7 @@ The trace output is in tab-separated columns. - 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). -6. **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), the loaded and stored data are given. +6. **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.