From db63dacb9636aeb9317f922d9fd30327acb3b2f1 Mon Sep 17 00:00:00 2001 From: MuhammadHammad001 Date: Wed, 19 Feb 2025 13:27:42 +0500 Subject: [PATCH 1/4] Big endianness support added --- model/prelude.sail | 3 +++ model/riscv_mem.sail | 29 ++++++++++++++++++++++++----- model/riscv_sys_regs.sail | 7 +++++-- 3 files changed, 32 insertions(+), 7 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index 2b878591c..f7627b1e2 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -236,3 +236,6 @@ type max_mem_access : Int = 4096 // Type used for memory access widths. Zero byte accesses are not allowed. type mem_access_width = range(1, max_mem_access) + +// Function to reverse endianness. +val reverse_endianness = pure {c: " reverse_endianness"} : forall 'n . (bits('n * 8)) -> bits('n * 8) \ No newline at end of file diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 1493747a7..6fd4ae40a 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -63,6 +63,15 @@ function write_kind_of_flags (aq : bool, rl : bool, con : bool) -> write_kind = (true, false, true) => throw(Error_not_implemented("sc.aq")) } +val check_endianess: unit -> bool +function check_endianess() = { + match cur_privilege { + Machine => bits_to_bool(mstatus[MBE]), + Supervisor => bits_to_bool(mstatus[SBE]), + User => bits_to_bool(mstatus[UBE]), + } +} + // only used for actual memory regions, to avoid MMIO effects function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : physaddr, width : int('n), aq : bool, rl: bool, res : bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = { let result = (match read_kind_of_flags(aq, rl, res) { @@ -73,9 +82,15 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext (Execute(), None()) => Err(E_Fetch_Access_Fault()), (Read(Data), None()) => Err(E_Load_Access_Fault()), (_, None()) => Err(E_SAMO_Access_Fault()), - (_, Some(v, m)) => { if get_config_print_mem() - then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(physaddr_bits(paddr)) ^ "] -> " ^ BitStr(v)); - Ok(v, m) } + (_, Some(v, m)) => { + let temp_var: bits('n * 8) = match (t, check_endianess()) { + (Execute(), _) => (v), + (_, true) => reverse_endianness(v), + (_, false) => (v), + }; + if get_config_print_mem() + then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(physaddr_bits(paddr)) ^ "] -> " ^ BitStr(temp_var)); + Ok(temp_var, m) } } } @@ -196,9 +211,13 @@ $endif // only used for actual memory regions, to avoid MMIO effects function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : physaddr, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { - let result = write_ram(wk, paddr, width, data, meta); + let temp_var: bits('n * 8) = match (check_endianess()) { + false => data, + true => reverse_endianness(data), + }; + let result = write_ram(wk, paddr, width, temp_var, meta); if get_config_print_mem() - then print_mem("mem[" ^ BitStr(physaddr_bits(paddr)) ^ "] <- " ^ BitStr(data)); + then print_mem("mem[" ^ BitStr(physaddr_bits(paddr)) ^ "] <- " ^ BitStr(temp_var)); Ok(result) } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 1a7e6233e..2f11fd822 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -207,6 +207,7 @@ bitfield Mstatus : bits(64) = { SPP : 8, MPIE : 7, + UBE : 6, SPIE : 5, MIE : 3, @@ -244,8 +245,8 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = { // MPV = v[MPV], // GVA = v[GVA], /* We don't currently support changing MBE and SBE. */ - // MBE = v[MBE], - // SBE = v[SBE], + MBE = v[MBE], + SBE = v[SBE], /* We don't support dynamic changes to SXL and UXL. */ // SXL = if xlen == 64 then v[SXL] else o[SXL], // UXL = if xlen == 64 then v[UXL] else o[UXL], @@ -269,6 +270,7 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = { SPP = if extensionEnabled(Ext_S) then v[SPP] else 0b0, VS = v[VS], MPIE = v[MPIE], + UBE = v[UBE], SPIE = v[SPIE], MIE = v[MIE], SIE = v[SIE], @@ -294,6 +296,7 @@ register mstatus : Mstatus = { } mapping clause csr_name_map = 0x300 <-> "mstatus" +mapping clause csr_name_map = 0x310 <-> "mstatush" function clause is_CSR_defined(0x300) = true // mstatus function clause is_CSR_defined(0x310) = xlen == 32 // mstatush From b7a06e3811a91ef07f1ad26bc6d285ebe3868c11 Mon Sep 17 00:00:00 2001 From: MuhammadHammad001 Date: Wed, 19 Feb 2025 17:10:26 +0500 Subject: [PATCH 2/4] Add conditions on sbe, ube --- model/prelude.sail | 2 +- model/riscv_mem.sail | 10 +++++----- model/riscv_sys_control.sail | 3 +++ model/riscv_sys_regs.sail | 4 ++-- 4 files changed, 11 insertions(+), 8 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index f7627b1e2..8386c23ac 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -238,4 +238,4 @@ type max_mem_access : Int = 4096 type mem_access_width = range(1, max_mem_access) // Function to reverse endianness. -val reverse_endianness = pure {c: " reverse_endianness"} : forall 'n . (bits('n * 8)) -> bits('n * 8) \ No newline at end of file +val reverse_endianness = pure {c: " reverse_endianness"} : forall 'n . (bits('n * 8)) -> bits('n * 8) diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 6fd4ae40a..d60dc3e0c 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -63,9 +63,9 @@ function write_kind_of_flags (aq : bool, rl : bool, con : bool) -> write_kind = (true, false, true) => throw(Error_not_implemented("sc.aq")) } -val check_endianess: unit -> bool -function check_endianess() = { - match cur_privilege { +val check_endianess: (AccessType(ext_access_type)) -> bool +function check_endianess(typ) = { + match effectivePrivilege(typ, mstatus, cur_privilege) { Machine => bits_to_bool(mstatus[MBE]), Supervisor => bits_to_bool(mstatus[SBE]), User => bits_to_bool(mstatus[UBE]), @@ -83,7 +83,7 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext (Read(Data), None()) => Err(E_Load_Access_Fault()), (_, None()) => Err(E_SAMO_Access_Fault()), (_, Some(v, m)) => { - let temp_var: bits('n * 8) = match (t, check_endianess()) { + let temp_var: bits('n * 8) = match (t, check_endianess(t)) { (Execute(), _) => (v), (_, true) => reverse_endianness(v), (_, false) => (v), @@ -211,7 +211,7 @@ $endif // only used for actual memory regions, to avoid MMIO effects function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : physaddr, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { - let temp_var: bits('n * 8) = match (check_endianess()) { + let temp_var: bits('n * 8) = match (check_endianess(Write())) { false => data, true => reverse_endianness(data), }; diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ead87d08c..f7708eca0 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -339,6 +339,9 @@ function reset_sys() -> unit = { mstatus[MIE] = 0b0; mstatus[MPRV] = 0b0; + // If little-endian memory accesses are supported, the mstatus/mstatush field MBE is reset to 0. + mstatus[MBE] = 0b0; + // "If little-endian memory accesses are supported, the mstatus/mstatush field // MBE is reset to 0." // TODO: The handling of mstatush is a bit awkward currently, but the model diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 2f11fd822..624edc926 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -246,7 +246,7 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = { // GVA = v[GVA], /* We don't currently support changing MBE and SBE. */ MBE = v[MBE], - SBE = v[SBE], + SBE = if extensionEnabled(Ext_S) then v[SBE] else 0b0, /* We don't support dynamic changes to SXL and UXL. */ // SXL = if xlen == 64 then v[SXL] else o[SXL], // UXL = if xlen == 64 then v[UXL] else o[UXL], @@ -270,7 +270,7 @@ function legalize_mstatus(o : Mstatus, v : bits(64)) -> Mstatus = { SPP = if extensionEnabled(Ext_S) then v[SPP] else 0b0, VS = v[VS], MPIE = v[MPIE], - UBE = v[UBE], + UBE = if extensionEnabled(Ext_U) then v[UBE] else 0b0, SPIE = v[SPIE], MIE = v[MIE], SIE = v[SIE], From 3930145cdd353e3f1cd72f83a52d5aff6dcb8b69 Mon Sep 17 00:00:00 2001 From: MuhammadHammad001 Date: Thu, 20 Feb 2025 12:38:28 +0500 Subject: [PATCH 3/4] add ube field in sstatus --- model/riscv_sys_control.sail | 8 +------- model/riscv_sys_regs.sail | 3 +++ 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index f7708eca0..d8a753003 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -339,15 +339,9 @@ function reset_sys() -> unit = { mstatus[MIE] = 0b0; mstatus[MPRV] = 0b0; - // If little-endian memory accesses are supported, the mstatus/mstatush field MBE is reset to 0. - mstatus[MBE] = 0b0; - // "If little-endian memory accesses are supported, the mstatus/mstatush field // MBE is reset to 0." - // TODO: The handling of mstatush is a bit awkward currently, but the model - // currently only supports little endian so MBE is always 0. - // See https://github.com/riscv/sail-riscv/issues/639 - // mstatus[MBE] = 0b0; + mstatus[MBE] = 0b0; // "The misa register is reset to enable the maximal set of supported extensions" reset_misa(); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 624edc926..467398c5a 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -706,6 +706,7 @@ bitfield Sstatus : bits(64) = { FS : 14 .. 13, VS : 10 .. 9, SPP : 8, + UBE : 6, SPIE : 5, SIE : 1, } @@ -725,6 +726,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { FS = m[FS], VS = m[VS], SPP = m[SPP], + UBE = m[UBE], SPIE = m[SPIE], SIE = m[SIE], ] @@ -745,6 +747,7 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { FS = s[FS], VS = s[VS], SPP = s[SPP], + UBE = s[UBE], SPIE = s[SPIE], SIE = s[SIE], ] From 89d26641a07d91abbb460325566613cc4804b0fe Mon Sep 17 00:00:00 2001 From: MuhammadHammad001 Date: Fri, 21 Feb 2025 13:21:07 +0500 Subject: [PATCH 4/4] Rename big endianness check function --- model/riscv_mem.sail | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index d60dc3e0c..688bd850d 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -63,8 +63,7 @@ function write_kind_of_flags (aq : bool, rl : bool, con : bool) -> write_kind = (true, false, true) => throw(Error_not_implemented("sc.aq")) } -val check_endianess: (AccessType(ext_access_type)) -> bool -function check_endianess(typ) = { +function is_big_endian(typ : AccessType(ext_access_type)) -> bool = { match effectivePrivilege(typ, mstatus, cur_privilege) { Machine => bits_to_bool(mstatus[MBE]), Supervisor => bits_to_bool(mstatus[SBE]), @@ -83,7 +82,7 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext (Read(Data), None()) => Err(E_Load_Access_Fault()), (_, None()) => Err(E_SAMO_Access_Fault()), (_, Some(v, m)) => { - let temp_var: bits('n * 8) = match (t, check_endianess(t)) { + let temp_var: bits('n * 8) = match (t, is_big_endian(t)) { (Execute(), _) => (v), (_, true) => reverse_endianness(v), (_, false) => (v), @@ -211,7 +210,7 @@ $endif // only used for actual memory regions, to avoid MMIO effects function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : physaddr, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { - let temp_var: bits('n * 8) = match (check_endianess(Write())) { + let temp_var: bits('n * 8) = match (is_big_endian(Write())) { false => data, true => reverse_endianness(data), };