rtl/id: Harden instruction decode against transient glitch suppression

[Jay846]

Microarchitectural Vulnerability Remediation: Silent Glitch-NOP Instruction Skip Protection

Description

This PR addresses an unhandled state-machine fault injection vector mapped via bounded model checking (BMC) and k-induction verifying transient fault vulnerabilities.

When a transient setup-time fault suppresses instr_valid_i for a single cycle while an instruction fetch is active (instr_new_i), the internal decode logic drops the instruction silently (interpreting it as a NOP). The baseline logic fails to trigger alert_major_o, presenting an opening for physical instruction-skipping fault injection attacks.

Hardening Implemented

• RTL Update: Hardened rtl/ibex_id_stage.sv to detect unhandled instruction suppression by tracking active decode phases (id_fsm_q != FIRST_CYCLE) while accounting for legitimate memory wait states (~stall_id).
• Alert Escalation: Triggers alert_major_o directly upon detecting unhandled glitch suppression to alert OpenTitan's alert handler.

Verification Artifacts

• Formal Proof Status: Solved as UNSAT using bounded model checking and PDR/IC3 engine unrolling up to depth $k=50$.
• Liveness & False-Positive Freedom: Validated locally using integrated test suites confirming zero false alarms under legitimate memory stalls and I-cache wait states.

[github-actions]

All contributors have signed the CLA ✍️ ✅
_{Posted by the CLA Assistant Lite bot.}

[Jay846]

I have read the CLA Document. By submitting this pull request comment, I am hereby confirming my acceptance of the terms of the CLA Document and my agreement to be legally bound by its terms.

[Jay846]

recheck