If C cannot be disabled, all changes to misa must be suppressed

model/riscv_sys_regs.sail

@@ -156,22 +156,19 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "
  unsetting C. If it returns true the write will have no effect. */
 val ext_veto_disable_C : unit -> bool effect {rreg}
 
-/* We currently only support dynamic changes for the C extension. */
 function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
- if sys_enable_writable_misa ()
- then { /* Handle modifications to C. */
- let v = Mk_Misa(v);
- /* Suppress changing C if nextPC would become misaligned or an extension vetoes or C was disabled at boot (i.e. not supported). */
- let m =
- if (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | not(sys_enable_rvc())
- then m
- else update_C(m, v.C());
- /* Handle updates for F/D. */
- if not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
- then m
- else update_D(update_F(m, v.F()), v.D())
- }
- else m
+ let v = Mk_Misa(v);
+ /* If MISA is not writable then suppress updates to misa & disabling C if nextPC would become misaligned or an extension vetoes */
+ if not(sys_enable_writable_misa()) | (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C()))
+ then m
+ else {
+ /* Suppress updates to C if C is read-only */
+ let m = if not(sys_enable_rvc()) then m else update_C(m, v.C());
+ /* Handle updates for F/D. */
+ if not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
+ then m
+ else update_D(update_F(m, v.F()), v.D())
+ }
 }
 
 /* helpers to check support for various extensions. */