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 5 How RTL Issues Were Found

“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 6 Breakdown of Issues found by Simulation

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 7 Issue Classification

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 professonal verification engineers more than 9 months to find all these issues.

v2.0.0 verification

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.

WIP…

Formal verification

To accelerate the verification of more than 300 Xpulp instructions, Formal Verification methodology has been used with Siemens EDA Onespin tools and their RISC-V ISA 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. This has been applied on 5 different core configurations (controlled via SystemVerilog parameters).

WIP…

Reports

WIP…

Tracer

TODO: To re-work with ImperasDV tracer.

The module cv32e40p_tracer 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_TRACE_EXECUTION.

Output file

All traced instructions are written to a log file. The log file is named trace_core_<HARTID>.log, with <HARTID> being the 32 digit hart ID of the core being traced.

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 address and the loaded and stored data are given.

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:0x00008000 x8=0x00007fff
 136    64 0000015a 8c65     c.and   x8,x9       x8:0x00007fff x9:0x00000000 x8=0x00000000
 142    67 0000015c c622     c.swsp  x8,12(x2)   x2:0x00002000 x8:0x00000000 PA:0x0000200c