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 8 How RTL Issues Were Found in v1.0.0

“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 9 Breakdown of Issues found by Simulation in v1.0.0

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 10 Issue Classification in v1.0.0

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.

v2.0.0 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 11 Verified configurations

	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 2 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:

{
  "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 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

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 12 How Issues Were Found in v2.0.0

“Found By”	Count	Note
Formal Verification	30	All related to features enabled by COREV_PULP or FPU.
Simulation	10
Lint	2

A classification of the Formal Verification issues by type and their description are listed in the following tables:

Table 13 Breakdown of Issues found by Formal Verification in v2.0.0

Type	Count	Note
User Manual	12	Instructions description leading to mis-interpretation
RTL bugs	18	See classification below

Table 14 Formal Verification Issues Classification in v2.0.0

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 respective F instructions (when FPU_ADDMUL_LAT or 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 15 Breakdown of Issues found by Simulation in v2.0.0

Type	Count	Note
RTL bugs	10	See classification below

Table 16 Simulation Issues Classification in v2.0.0

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

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. 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).

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.

Time Cycle PC       Instr    Decoded instruction Register and memory contents
 130    61 00000150 4481     c.li    x9,0        x9=0x00000000
 132    62 00000152 00008437 lui     x8,0x8      x8=0x00008000
 134    63 00000156 fff40413 addi    x8,x8,-1    x8=0x00007fff  x8:0x00008000
 136    64 0000015a 8c65     c.and   x8,x9       x8=0x00000000  x8:0x00007fff  x9:0x00000000
 142    67 0000015c c622     c.swsp  x8,12(x2)   x2:0x00002000  x8:0x00000000 PA:0x0000200c