The condition for if statement line 287 of fpnew_divsqrt_th_32 was not covered during all the simulation non-regressions.
After analysis we suspected that this scenario was in fact unreachable.
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_divsqrt_th_288.
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.
Component
Component:RTL
Issue Description
The condition for if statement line 287 of fpnew_divsqrt_th_32 was not covered during all the simulation non-regressions.
After analysis we suspected that this scenario was in fact unreachable. 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_divsqrt_th_288.
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.