csr_regfile: zero mtval/stval on interrupt traps (fix GPLEN-1 bit select)

[codeadpool]

…ect)

• [ x] I have searched for similar pull requests
• [ x] I am a human engaging in an interpersonal interaction. During this interaction, my words are my own and are not generated. If relevant, I provide links to my sources.

Two related bugs leave the interrupted instruction's encoding in mtval/stval after an interrupt, where the privileged spec requires zero.

1. The M-mode mtval zeroing term uses ex_i.cause[GPLEN-1] where every sibling use ex_i.cause[XLEN-1]; GPLEN-1 is zero for all valid architectural causes. so the interrupt term never fired.
2. The zeroing arm is gated by ZERO_TVAL i.e., 0 in default builds, so interrupt tval was not zeroed even with the above GPLEN -> XLEN fixed. This corrects the bit-select and zeroes tval for interrupts unconditionally at mtval, stval, vstval sites, leaving the ZERO_TVAL gated exception behavior unchanged. Found by formal property checking of csr_regfile.

Fixes #3379

The hypervisor htinst path has a similar ZERO_TVAL gated interrupt term, but it is only active on RVH builds. This config is RVH=0, so that path is not exercised by the formal check and is left out of this PR. htval is unchanged its GPLEN slice is guest physical length not a cause bit select, so its not affected.

[JeanRochCoulon]

By reviewing this PR, we can wonder whether code could be simplified.
ZERO_TVAL seems to be defined to support Spike Tandem. @AyoubJalali do you confirm we need this trick ?

Extracted from ariane_pkg.sv:

@ASintzoff

[AyoubJalali]

By reviewing this PR, we can wonder whether code could be simplified. ZERO_TVAL seems to be defined to support Spike Tandem. @AyoubJalali do you confirm we need this trick ?

Extracted from ariane_pkg.sv:

@ASintzoff

LGTM

[codeadpool]

@JeanRochCoulon this pr leaves ZERO_TVAL doing exactly what it did before. the only change is the interrupt check now sits outside the guard. with ZERO_TVAL=0 that reduces to just cause[XLEN-1], so interrupts zero tval in every build. that's the part spec requires, tandem or not. the exception cause list is still gated exactly as before, so if you decide the trick isn't necessary, dropping it only affects that list and interrupts stay correct.
on simplification: mtval/stval/vstval all have the same shape now, with interrupt case pulled out of the tandem gated one. can restructure if you'd prefer.

ran this branch against unmodified csr_regfile:

v5.3.0 (2ef1c1b)	this pr (3250ed4)
CEX	Pass

logs and traces: https://github.com/codeadpool/cva6-priv-sva/tree/main/evidence/mstatus

limitation: htinst/mtinst have their interrupt condition inside the ZERO_TVAL guard, so on a RVH build an interrupt can still leave them non-zero. that's outside the config i verified (RVH=0), so i kept it out of this PR, happy to open a separate issue for it.

[codeadpool]

the previous table was bmc only (depth 12), re-ran with an unbounded proof, and this pr changes three sites and i'd only checked mtval.

property	v5.3.0 (2ef1c1b)	this pr (3250ed4)
interrupt trap to M => mtval == 0	CEX	proven (k-induction)
interrupt trap to S => stval == 0	CEX	proven (k-induction)

the antecedent covers (M/S interrupt with nonzero tval) still reach on the fixed rtl, and both witness covers are the exact negation of a proven assertion, so they're unreachable by proof rather than by bounded search.

still uncovered: vstval (needs RVH=1, outside the config i verify) plus the htinst/mtinst limitation noted above.

logs and traces: https://github.com/codeadpool/cva6-priv-sva/tree/main/evidence/mstatus

[github-actions]

❌ failed run, report available here.

[cainria]

Hi! Any news about this PR ?

[codeadpool]

Hi im waiting for feedback from the code owner to see if any adjustments are needed on my side. I’ll update the PR accordingly once I hear back