There is 1 branch condition not covered on line 675 of cv32e40p_controller during all the simulation non-regressions:
No case when ID not ready for single stepped instruction
After a lot of talks and brainstorming, it was suspected that thisAllFalse uncovered branch could be unreachable case.
SLEC app of Cadence JasperGold was used to prove that there is no difference on CV32E40P top level output signals between original RTL code and a modified one where lines 675 and 703 are totally removed.
As the tool is not able to generate a scenario/counter-example by driving any kind of sequential sequence on CV32E40P top level input signals showing a different behavior on output signals between the original RTL and the modified one, the conclusion is that AllFalse uncovered branches are really unreachable.
To reproduce/analyze it, slec run could be launched between original RTL code and a modified one by going in cv32e40p/scripts/slec and by launching following command:
./run.sh -t cadence -p sec
As it was too late to remove 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 this branch hole in v2.
Component
Component:RTL
Issue description
There is 1 branch condition not covered on line 675 of cv32e40p_controller during all the simulation non-regressions: No case when ID not ready for single stepped instruction
After a lot of talks and brainstorming, it was suspected that thisAllFalse uncovered branch could be unreachable case. SLEC app of Cadence JasperGold was used to prove that there is no difference on CV32E40P top level output signals between original RTL code and a modified one where lines 675 and 703 are totally removed. As the tool is not able to generate a scenario/counter-example by driving any kind of sequential sequence on CV32E40P top level input signals showing a different behavior on output signals between the original RTL and the modified one, the conclusion is that AllFalse uncovered branches are really unreachable.
To reproduce/analyze it, slec run could be launched between original RTL code and a modified one by going in cv32e40p/scripts/slec and by launching following command: ./run.sh -t cadence -p sec
As it was too late to remove 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 this branch hole in v2.