From 5010f08299f091234f8a3eb4e03c2499e03ef251 Mon Sep 17 00:00:00 2001 From: ahadali5000 Date: Fri, 2 Jun 2023 20:06:51 +0500 Subject: [PATCH] If C cannot be disabled, all changes to misa must be suppressed --- model/riscv_sys_regs.sail | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index ecc7735b7..fbd7130ab 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -156,21 +156,28 @@ 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()) - } + then { + let v = Mk_Misa(v); + /* Suppress disabling C & keep misa unchanged if nextPC would become misaligned or an extension vetoes */ + if 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_writable_misa()) then m else update_C(m, v.C()); + /* Suppress updates to F/D if they are read-only or would become an illegal combination */ + if not(sys_enable_writable_misa()) + then m + else if (v.D() == 0b1 & v.F() == 0b0) + then { + if m.F() == 0b1 + then update_D(update_F(m, 0b0), 0b0) + else m + } + else update_D(update_F(m, v.F()), v.D()) + } + } else m }