csr_regfile: WARL legalize the dcsr write path (prv, v, cause)

[codeadpool]

• I have searched for similar pull requests
• 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.

DCSR write path stored several fields raw, this legalizes them on write. prv is clamped to supported privilege modes, v is forced to 0 without hypervisor extension and at RVH=1, when the mode being stored or restored is M: on the write when the written prv is M, and on dret when the restored privilege is M (M-mode is never virtualized), and cause is preserved. Without prv legalization a dret could set priv_lvl to an unimplemented encoding (2'b10/ PRIV_LVL_HS on an RVH=0 build), losing M-mode's PMP bypass. Found by formal property checking of csr_regfile. The property that priv_lvl is always one of M, S, U fails on current RTL and passes after the fix, the illegal dcsr.prv state that produced the cex becomes unreachable.

Fixes #3383, #1984, #1985

Verified formally on cv64a6_imafdc_sv39 (RVH=0) for prv/cause/reserved, and on cv64a6_imafdch_sv39 (RVH=1) for the dcsr.v clamps. the legalization is guarded by the same RVH/RVS/RVU params the rest of the CSR file uses. The mret path to the same M-with-V=1 state is a separate register, tracked in #3313.

[JeanRochCoulon]

When !CVA6Cfg.RVH, we cannot have dcsr_d.prv == riscv::PRIV_LVL_HS...

[codeadpool]

dcsr.prv can hold 2'b10 here, write is raw (dcsr_d = csr_wdata[31:0], dcsr_t.prv is a full 2-bit priv_lvl_t), so a debugger can set it and dret copies it into priv_lvl unlegalized. The formal check behind this PR witnesses this on RVH=0 (fails before the patch, passes after).

Agreed, CVA6Cfg.RVH guard is too narrow though. 2'b10 is never a valid operating priv_lvl in any config: HS mode is priv_lvl=S with V=0 not priv_lvl=2'b10, so the guard shouldn't be conditional. I'd mirrored mstatus.mpp handling at csr_regfile.sv:1382, it has the same !RVH form. i've generalized it to legalize prv against the supported set unconditionally and clamp anything else to M, so it also covers RVH=1 builds:

   if (dcsr_d.prv != riscv::PRIV_LVL_M &&
       !(CVA6Cfg.RVS && dcsr_d.prv == riscv::PRIV_LVL_S) &&
       !(CVA6Cfg.RVU && dcsr_d.prv == riscv::PRIV_LVL_U)) begin
     dcsr_d.prv = riscv::PRIV_LVL_M;
   end 

Pushed. My formal setup only exercises RVH=0, but this generalization is correct by construction for the hypervisor configs too.

[codeadpool]

Pushed 8f74af4, which zeroes DCSR reserved fields zero 1 (bit 14) and zero2 (bits 27:18). they were assigned raw from csr_wdata, so software could set them. this completes the reserved-field half of #1984 that the prv/v/cause change didn't cover.

property	v5.3.0 (2ef1c1b)	this pr (8f74af4)
priv_lvl in {M,S,U} after dret (#3383)	CEX	pass
DCSR reserved fields read 0 (#1984)	CEX	pass

In both cases the scenario covers (debug entry, dret in debug) still reach and only the defect witness covers become unreachable so defects are unreachable, not unexercised.
Logs and traces: https://github.com/codeadpool/cva6-priv-sva/tree/main/evidence/probe

[codeadpool]

I ran formal on this PR at head 58e79cf. Each property produces a CEX on the unpatched v5.3.0 baseline and passes here as an unbounded proof.

At cv64a6_imafdc_sv39 (RVH=0):

• dcsr.prv: proven WARL-legal, with priv_lvl after dret constrained to {M, S, U}.
• DCSR reserved fields (Virtualization mode only dcsr field v and other reserved fields are set #1984): zero1 (bit 14) and zero2 (bits 27:18) proven to read zero.
• dcsr.cause (Debug-mode entry reason dcsr field cause is writable by software #1985): proven preserved across an in-debug CSR write, so a debugger cannot overwrite the hardware-set cause.

At cv64a6_imafdch_sv39 (RVH=1):

• dcsr.v write legalization: with v cleared when the written, legalized prv is M, proven that an in-debug DCSR write cannot store {prv=M, v=1}.
• DRET legalization: with v cleared when DRET restores M-mode, proven that DRET never resumes M-mode with V=1, regardless of how DCSR acquired its value.

Each property fails without its corresponding clamp and proves with it.

Checkers and per property logs: https://github.com/codeadpool/cva6-priv-sva/tree/main/evidence/probe

One related path remains: M,V=1 is also reachable through mret when mstatus.mpv=1 and mstatus.mpp=M. that is open issue #3313, whose fix belongs in the mstatus/MRET path. This PR handles the DCSR/DRET paths; #3313 handles MRET