search

openhwgroup / cv32e40p

CV32E40P is an in-order 4-stage RISC-V RV32IMFCXpulp CPU based on RI5CY from PULP-Platform
https://docs.openhwgroup.org/projects/cv32e40p-user-manual/en/latest
Other
928 stars 410 forks source link

RTL Code Coverage Hole in cv32e40p_EX_stage module line 237 and 241 #1023

Open YoannPruvost opened 2 months ago

YoannPruvost commented 2 months ago

Component

Component:RTL

Issue Description

One of the possible combination in the if statements line 237 and 241 of cv32e40p_EX_stage was not covered during all the simulation non-regressions for 0 cycle latency and 2 cycle latency on the FPU.

After analysis we suspected that this scenario was in fact unreachable as in those configurations all FPU instructions are either single_cycle or multi_cycle (ie more than 1 cycle)

Siemens Questa Static formal tool was used to prove that this scenario was unreachable. For this scenario a dedicated assertion was written, named assert_unreachable_ex_237.

All information necessary to reproduce and analyze our work with formal can be found in the ReadMe in the cv32e40p/scripts/formal folder

As it was too late to implement a fix in the RTL due to long RISC-V ISA Formal Verification runs and requiring to update all waivers files as well, it has been decided to waive this scenario hole in v2.

237-241 237-241-2

MikeOpenHWGroup commented 2 months ago

Hi @YoannPruvost, can you provide some addition insight into this code coverage hole?