Some of the possible combination in the if statement line 1241 of cv32e40p_controller were not covered during all the simulation non-regressions.
After analysis we suspected that those scenario were in fact unreachable.
Siemens Questa OneSpin Static formal tool was used to prove that those three scenario were unreachable. For each scenario, row 4, 5 and 10, a dedicated assertion was written, respectively named assert_unreachable_ctrl_1241_row_4, assert_unreachable_ctrl_1241_row_5 and assert_unreachable_ctrl_1241_row_10
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 those 3 scenario holes in v2.
Component
Component:RTL
Issue description
Some of the possible combination in the if statement line 1241 of cv32e40p_controller were not covered during all the simulation non-regressions.
After analysis we suspected that those scenario were in fact unreachable. Siemens Questa OneSpin Static formal tool was used to prove that those three scenario were unreachable. For each scenario, row 4, 5 and 10, a dedicated assertion was written, respectively named assert_unreachable_ctrl_1241_row_4, assert_unreachable_ctrl_1241_row_5 and assert_unreachable_ctrl_1241_row_10
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 those 3 scenario holes in v2.