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
966 stars 423 forks source link

RTL Code Coverage Hole in cv32e40p_controller module lines 1187 and 1210 #1011

Open YoannPruvost opened 5 months ago

YoannPruvost commented 5 months ago

Component

Component:RTL

Issue description

There are to "if, else if" statement line 1187 and 1210 of cv32e40p_controller where the "All False" condition were not covered during all the simulation

After analysis we suspected that those scenario were in fact unreachable. Siemens Questa OneSpin Static formal tool was used to prove that those two scenario were unreachable. For each statement, line 1187 and 1210, a dedicated assertion was written, respectively named assert_all_true_ctrl_1187_1189_and_1191 and assert_all_true_ctrl_1210_and_1212

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 update those lines 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 those 2 branches holes in v2.

1187-1 1187-2

1210-1 1210-2