From 825a62595fb8b2a488bfa004beeef5020a975314 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Radim=20Kr=C4=8Dm=C3=A1=C5=99?= Date: Sat, 11 Jan 2025 10:46:16 +0100 Subject: [PATCH 1/3] insts_base: ignore architecture in SFENCE_VMA MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit architecture doesn't change the behavior, so there is no reason to complicate the code with it. The code is still suboptimal because of rhs duplication, so this should be rewritten if (when) Sail supports multiple matches like: User or (Supervisor if mstatus[TVM] == 0b1) => ... Machine or (Supervisor if mstatus[TVM] == 0b0) => ... (Separately mapping those four cases into two and matching on the two is also an option, but I'm not sure it would be clearer.) Signed-off-by: Radim Krčmář --- model/riscv_insts_base.sail | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 390b3a9d2..7cd920437 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -714,9 +714,9 @@ function clause execute SFENCE_VMA(rs1, rs2) = { let asid = if rs2 != zreg then Some(X(rs2)[asidlen - 1 .. 0]) else None(); match cur_privilege { User => { handle_illegal(); RETIRE_FAIL }, - Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus[TVM]) { - (_, 0b1) => { handle_illegal(); RETIRE_FAIL }, - (_, 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS }, + Supervisor => match mstatus[TVM] { + 0b1 => { handle_illegal(); RETIRE_FAIL }, + 0b0 => { flush_TLB(asid, addr); RETIRE_SUCCESS }, }, Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS } } From 9716f11f0765a09b23a8e74d3370b91a141b243f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Radim=20Kr=C4=8Dm=C3=A1=C5=99?= Date: Mon, 27 Jan 2025 22:56:04 +0100 Subject: [PATCH 2/3] sys_regs: remove SXL and UXL accessors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The SXL and UXL fields are WPRI when MXLEN=32, so we should not confuse the sail implementation by saying that SXL and UXL is 0b01 on RV32. Signed-off-by: Radim Krčmář --- model/riscv_sys_regs.sail | 30 +++++++++++------------------- model/riscv_vmem.sail | 2 +- 2 files changed, 12 insertions(+), 20 deletions(-) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 3a52f9a62..41bd58a9e 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -220,18 +220,6 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : then privLevel_of_bits(m[MPP]) else priv -function get_mstatus_SXL(m : Mstatus) -> arch_xlen = { - if xlen == 32 - then architecture(RV32) - else m[SXL] -} - -function get_mstatus_UXL(m : Mstatus) -> arch_xlen = { - if xlen == 32 - then architecture(RV32) - else m[UXL] -} - function get_mstatus_SD(m : Mstatus) -> bits(1) = { if xlen == 32 then m[SD_32] else m[SD_64] @@ -324,13 +312,17 @@ function clause write_CSR((0x310, value) if xlen == 32) = { mstatus = legalize_m /* architecture and extension checks */ function cur_architecture() -> Architecture = { - let a : arch_xlen = - match cur_privilege { - Machine => misa[MXL], - Supervisor => get_mstatus_SXL(mstatus), - User => get_mstatus_UXL(mstatus) - }; - architecture(a) + if xlen == 32 + then RV32 + else { + let a : arch_xlen = + match cur_privilege { + Machine => misa[MXL], + Supervisor => mstatus[SXL], + User => mstatus[UXL], + }; + architecture(a) + } } function in32BitMode() -> bool = { diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index 5011c3f7c..b829b8b0b 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -179,7 +179,7 @@ function satp_to_ppn(satp_val) = function translationMode(priv : Privilege) -> SATPMode = { if priv == Machine then Bare else { - let arch = architecture(get_mstatus_SXL(mstatus)); + let arch = if xlen == 32 then RV32 else architecture(mstatus[SXL]); let mbits : satp_mode = match arch { RV64 => { // Can't have an effective architecture of RV64 on RV32. From 27f6296dff86868c61ff20879d72b63c50610145 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Radim=20Kr=C4=8Dm=C3=A1=C5=99?= Date: Sat, 11 Jan 2025 10:41:53 +0100 Subject: [PATCH 3/3] sys_regs: compute mstatus and sstatus SD bit on CSR read MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SD bit is read-only and we don't have to store it anywhere, because its only purpose is to accelerate software after CSR reads. Remove SD from mstatus and add SD as the most significant bit in CSR reads * to avoid the need to increase mstatus width to bit(128) when implementing RV128, * to simplify support for dynamic XLEN (no need to move SD in mstatus), * to make the code nicer. Signed-off-by: Radim Krčmář --- model/riscv_fdext_regs.sail | 1 - model/riscv_sys_regs.sail | 51 ++++++++++--------------------------- model/riscv_vext_regs.sail | 1 - 3 files changed, 13 insertions(+), 40 deletions(-) diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 261175de1..f363ab736 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -88,7 +88,6 @@ register f31 : fregtype function dirty_fd_context() -> unit = { assert(sys_enable_fdext()); mstatus[FS] = extStatus_to_bits(Dirty); - mstatus = set_mstatus_SD(mstatus, 0b1); } function dirty_fd_context_if_present() -> unit = { diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 41bd58a9e..f4a211243 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -176,8 +176,6 @@ function have_privLevel(priv : priv_level) -> bool = } bitfield Mstatus : bits(64) = { - SD_64: 63, - //MDT : 42, //MPELP: 41, @@ -190,8 +188,6 @@ bitfield Mstatus : bits(64) = { SXL : 35 .. 34, UXL : 33 .. 32, - SD_32: 31, - //SDT : 24, //SPELP: 23, TSR : 22, @@ -220,15 +216,10 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : then privLevel_of_bits(m[MPP]) else priv -function get_mstatus_SD(m : Mstatus) -> bits(1) = { - if xlen == 32 then m[SD_32] - else m[SD_64] -} - -function set_mstatus_SD(m : Mstatus, v : bits(1)) -> Mstatus = { - if xlen == 32 - then [m with SD_32 = v] - else [m with SD_64 = v] +function status_dirty(s : Mstatus) -> bits(1) = { + bool_to_bits(extStatus_of_bits(s[FS]) == Dirty | + extStatus_of_bits(s[XS]) == Dirty | + extStatus_of_bits(s[VS]) == Dirty) } function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = { @@ -239,7 +230,9 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = { */ let v = Mk_Mstatus(v); - let o = [o with + [o with + /* SD is handled in CSR accessors */ + // MDT = v[MDT], // MPELP = v[MPELP], // MPV = v[MPV], @@ -273,16 +266,6 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = { SPIE = v[SPIE], MIE = v[MIE], SIE = v[SIE], - ]; - - // Set dirty bit to OR of other status bits. - let dirty = extStatus_of_bits(o[FS]) == Dirty | - extStatus_of_bits(o[XS]) == Dirty | - extStatus_of_bits(o[VS]) == Dirty; - - [o with - SD_64 = if xlen == 64 then bool_to_bits(dirty) else o[SD_64], - SD_32 = if xlen == 32 then bool_to_bits(dirty) else o[SD_32], ] } @@ -302,11 +285,11 @@ mapping clause csr_name_map = 0x300 <-> "mstatus" function clause is_CSR_defined(0x300) = true // mstatus function clause is_CSR_defined(0x310) = xlen == 32 // mstatush -function clause read_CSR(0x300) = mstatus.bits[xlen - 1 .. 0] +function clause read_CSR(0x300) = status_dirty(mstatus) @ mstatus.bits[xlen - 2 .. 0] function clause read_CSR(0x310 if xlen == 32) = mstatus.bits[63 .. 32] -function clause write_CSR((0x300, value) if xlen == 64) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits } -function clause write_CSR((0x300, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, mstatus.bits[63 .. 32] @ value); mstatus.bits[31 .. 0] } +function clause write_CSR((0x300, value) if xlen == 64) = { mstatus = legalize_mstatus(mstatus, value); status_dirty(mstatus) @ mstatus.bits[62 .. 0] } +function clause write_CSR((0x300, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, mstatus.bits[63 .. 32] @ value); status_dirty(mstatus) @ mstatus.bits[30 .. 0] } function clause write_CSR((0x310, value) if xlen == 32) = { mstatus = legalize_mstatus(mstatus, value @ mstatus.bits[31 .. 0]); mstatus.bits[63 .. 32] } /* architecture and extension checks */ @@ -700,10 +683,9 @@ function clause read_CSR(0xF15) = mconfigptr /* sstatus reveals a subset of mstatus */ bitfield Sstatus : bits(64) = { - SD_64 : 63, + /* SD is handled in CSR accessors */ UXL : 33 .. 32, - SD_32 : 31, // SDT : 24, // SPELP : 23, MXR : 19, @@ -721,9 +703,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { let s = Mk_Sstatus(zeros()); [s with - SD_64 = m[SD_64], UXL = m[UXL], - SD_32 = m[SD_32], //SDT = m[SDT], //SPELP = m[SPELP], MXR = m[MXR], @@ -738,12 +718,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { } function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { - let dirty = extStatus_of_bits(s[FS]) == Dirty | extStatus_of_bits(s[XS]) == Dirty | - extStatus_of_bits(s[VS]) == Dirty; - [m with - SD_64 = if xlen == 64 then bool_to_bits(dirty) else m[SD_64], - SD_32 = if xlen == 32 then bool_to_bits(dirty) else m[SD_32], UXL = s[UXL], //SDT = s[SDT], //SPELP = s[SPELP], @@ -764,8 +739,8 @@ function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = { mapping clause csr_name_map = 0x100 <-> "sstatus" function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus -function clause read_CSR(0x100) = lower_mstatus(mstatus).bits[xlen - 1 .. 0] -function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits[xlen - 1 .. 0] } +function clause read_CSR(0x100) = status_dirty(mstatus) @ lower_mstatus(mstatus).bits[xlen - 2 .. 0] +function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); status_dirty(mstatus) @ mstatus.bits[xlen - 2 .. 0] } bitfield Sinterrupts : xlenbits = { diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index e98a87013..15823df43 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -79,7 +79,6 @@ mapping vreg_name = { function dirty_v_context() -> unit = { assert(sys_enable_vext()); mstatus[VS] = extStatus_to_bits(Dirty); - mstatus = set_mstatus_SD(mstatus, 0b1); } function rV (r : regno) -> vregtype = {