Add formal assertion for controller line 850 (#1010)

[avinashkollu-git]

This PR adds one assertion for issue #1010.

What it says
Lines 850 and 852-887 of cv32e40p_controller.sv can never run. The assertion checks that the controller is never in
DECODE_HWLOOP while single-step is on and the core is not in debug mode.

Why it is true
Single-step can only be turned on by dret or by a CSR write. Both send the controller back to DECODE. In DECODE
the core stops for the single step before it can enter DECODE_HWLOOP.

How I checked it
I do not have Questa, so I used open-source tools (Yosys and SymbiYosys). I used the same assumptions as
scripts/formal: no scan, the OBI rules on both buses, and no writes to the hardware-loop CSRs.

• Proven for COREV_PULP=1, FPU=0 (clock gate treated as always on). It also holds without the hardware-loop CSR assumption.
• COREV_PULP=0: the code does not exist, so the assertion is always true.
• FPU=1, and the full clock-gate model: the proof did not finish in two hours. No failure was found, but it is not proven.
• The check is not empty: the tool can reach DECODE_HWLOOP, and it can reach single-step outside debug mode.
• If I break the RTL so a CSR write turns on single-step without the pipeline flush, the assertion fails. So it can catch a real bug.
• The new lines pass Verilator lint inside the full formal setup.

Please note
The controller bind connects clk_i and rst_ni, which do not exist in cv32e40p_controller. PR #1072 fixes this.
Without it, the controller assertions, including this one, have no working clock.

Full report: https://github.com/Rivoryxa-Technologies/core-v-investigation-reports/blob/main/reports/rtl-triage-cv32e40p-1010.pdf