From fb68dcdc4a94bcb9484f639b4bad522d37cdd676 Mon Sep 17 00:00:00 2001 From: KotorinMinami <98281165+KotorinMinami@users.noreply.github.com> Date: Thu, 19 Dec 2024 18:29:21 +0800 Subject: [PATCH] Make physical addresses 34-bit for RV32 Change physical addresses to be 34-bits on RV32. Sv32 allows 34-bit physical addresses. When no virtual memory is supported or the Bare translation mode is used, the 34-bit addresses are just zero extended from the 32-bit virtual address. > When the value of satp.MODE is Bare, the 32-bit virtual address is translated (unmodified) into a 32-bit physical address, and then that physical address is zero-extended into a 34-bit machine-level physical address. The underlying Sail memory system only supports 32 or 64-bit addresses, so now we zero-extend to 64-bit in all cases. Note, Sv32 can be used on RV64 if SXLEN=32. The model does not support SXLEN != XLEN yet but this code may need modifying if support is added. --- model/prelude_mem.sail | 21 ++++++++++++--------- model/prelude_mem_addrtype.sail | 7 +++++-- model/prelude_mem_metadata.sail | 4 ++-- model/riscv_platform.sail | 28 ++++++++++++++-------------- model/riscv_sys_control.sail | 4 ++-- model/riscv_vmem.sail | 14 +++++--------- model/riscv_xlen32.sail | 2 ++ model/riscv_xlen64.sail | 2 ++ 8 files changed, 44 insertions(+), 38 deletions(-) diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 17813b93e..53bf8a83a 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -58,15 +58,18 @@ struct RISCV_strong_access = { /* The Sail concurrency interface lets us have a physical address type with additional information, provided we can supply a function that - converts it into a bitvector. Since we are just using xlenbits as a - physical address, we need the identity function for xlenbits. */ -val xlenbits_identity : xlenbits -> xlenbits + converts it into a bitvector. When in RV32 mode, physaddrbits is + bits(34), which needs to be zero-extended to bits(64) for + sail_mem_write/read interface. This conversion is necessary because + the memory interface only supports 32-bit or 64-bit physical + addresses regardless of the actual physical address width. */ +val physaddrbits_zero_extend : physaddrbits -> bits(64) -function xlenbits_identity xs = xs +function physaddrbits_zero_extend xs = zero_extend(xs) instantiation sail_mem_write with - 'pa = xlenbits, - pa_bits = xlenbits_identity, + 'pa = physaddrbits, + pa_bits = physaddrbits_zero_extend, /* We don't have a relaxed-memory translation model for RISC-V, so we just use unit as a dummy type. */ 'translation_summary = unit, @@ -93,7 +96,7 @@ type max_mem_access : Int = 4096 val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, int('n), bits(8 * 'n), mem_meta) -> bool function write_ram(wk, physaddr(addr), width, data, meta) = { - let request : Mem_write_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { + let request : Mem_write_request('n, 64, physaddrbits, unit, RISCV_strong_access) = struct { access_kind = match wk { Write_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }), Write_RISCV_release => AK_explicit(struct { variety = AV_plain, strength = AS_rel_or_acq }), @@ -129,12 +132,12 @@ val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access. (write_kind, physaddr, i function write_ram_ea(wk, physaddr(addr), width) = () instantiation sail_mem_read with - pa_bits = xlenbits_identity + pa_bits = physaddrbits_zero_extend val read_ram : forall 'n, 0 < 'n <= max_mem_access. (read_kind, physaddr, int('n), bool) -> (bits(8 * 'n), mem_meta) function read_ram(rk, physaddr(addr), width, read_meta) = { let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta; - let request : Mem_read_request('n, 64, xlenbits, unit, RISCV_strong_access) = struct { + let request : Mem_read_request('n, 64, physaddrbits, unit, RISCV_strong_access) = struct { access_kind = match rk { Read_plain => AK_explicit(struct { variety = AV_plain, strength = AS_normal }), Read_ifetch => AK_ifetch(), diff --git a/model/prelude_mem_addrtype.sail b/model/prelude_mem_addrtype.sail index c1b325d3e..d9efb551d 100644 --- a/model/prelude_mem_addrtype.sail +++ b/model/prelude_mem_addrtype.sail @@ -9,10 +9,13 @@ /* Note: virtaddr includes physical addresses when address translation is disabled. * It is used where the address would be virtual if address translation is active. */ +type physaddrbits = bits(physaddrbits_len) -newtype physaddr = physaddr : xlenbits +let physaddrbits_len = sizeof(physaddrbits_len) + +newtype physaddr = physaddr : physaddrbits newtype virtaddr = virtaddr : xlenbits -function physaddr_bits(physaddr(paddr) : physaddr) -> xlenbits = paddr +function physaddr_bits(physaddr(paddr) : physaddr) -> physaddrbits = paddr function virtaddr_bits(virtaddr(vaddr) : virtaddr) -> xlenbits = vaddr diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail index b8dd81b32..9a80a760f 100644 --- a/model/prelude_mem_metadata.sail +++ b/model/prelude_mem_metadata.sail @@ -14,8 +14,8 @@ type mem_meta = unit let default_meta : mem_meta = () -val __WriteRAM_Meta : forall 'n. (xlenbits, int('n), mem_meta) -> unit +val __WriteRAM_Meta : forall 'n. (physaddrbits, int('n), mem_meta) -> unit function __WriteRAM_Meta(addr, width, meta) = () -val __ReadRAM_Meta : forall 'n. (xlenbits, int('n)) -> mem_meta +val __ReadRAM_Meta : forall 'n. (physaddrbits, int('n)) -> mem_meta function __ReadRAM_Meta(addr, width) = () diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index c7bbaf16b..e6d601f53 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -30,8 +30,8 @@ val elf_entry = pure { val plat_cache_block_size_exp = pure {c: "plat_cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12) /* Main memory */ -val plat_ram_base = pure {c: "plat_ram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits -val plat_ram_size = pure {c: "plat_ram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits +val plat_ram_base = pure {c: "plat_ram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> physaddrbits +val plat_ram_size = pure {c: "plat_ram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> physaddrbits /* whether the MMU should update dirty bits in PTEs */ val plat_enable_dirty_update = pure {interpreter: "Platform.enable_dirty_update", @@ -51,19 +51,19 @@ val plat_mtval_has_illegal_inst_bits = pure {interpreter: "Platform.mtval_has_il lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool /* ROM holding reset vector and device-tree DTB */ -val plat_rom_base = pure {interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits -val plat_rom_size = pure {interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits +val plat_rom_base = pure {interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> physaddrbits +val plat_rom_size = pure {interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> physaddrbits /* Location of clock-interface, which should match with the spec in the DTB */ -val plat_clint_base = pure {interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits -val plat_clint_size = pure {interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits +val plat_clint_base = pure {interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> physaddrbits +val plat_clint_size = pure {interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> physaddrbits /* Location of HTIF ports */ -val plat_htif_tohost = pure {c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits -function plat_htif_tohost () = to_bits(xlen, elf_tohost ()) +val plat_htif_tohost = pure {c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> physaddrbits +function plat_htif_tohost () = to_bits(physaddrbits_len, elf_tohost ()) // todo: fromhost -val phys_mem_segments : unit -> list((xlenbits, xlenbits)) +val phys_mem_segments : unit -> list((physaddrbits, physaddrbits)) function phys_mem_segments() = (plat_rom_base (), plat_rom_size ()) :: (plat_ram_base (), plat_ram_size ()) :: @@ -143,11 +143,11 @@ register stimecmp : bits(64) * bffc mtime hi */ -let MSIP_BASE : xlenbits = zero_extend(0x00000) -let MTIMECMP_BASE : xlenbits = zero_extend(0x04000) -let MTIMECMP_BASE_HI : xlenbits = zero_extend(0x04004) -let MTIME_BASE : xlenbits = zero_extend(0x0bff8) -let MTIME_BASE_HI : xlenbits = zero_extend(0x0bffc) +let MSIP_BASE : physaddrbits = zero_extend(0x00000) +let MTIMECMP_BASE : physaddrbits = zero_extend(0x04000) +let MTIMECMP_BASE_HI : physaddrbits = zero_extend(0x04004) +let MTIME_BASE : physaddrbits = zero_extend(0x0bff8) +let MTIME_BASE_HI : physaddrbits = zero_extend(0x0bffc) val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), physaddr, int('n)) -> MemoryOpResult(bits(8 * 'n)) function clint_load(t, physaddr(addr), width) = { diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 28731f6be..a8c755724 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -90,8 +90,8 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = val speculate_conditional = impure {interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool -val load_reservation = impure {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit -val match_reservation = pure {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool +val load_reservation = impure {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : physaddrbits -> unit +val match_reservation = pure {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : physaddrbits -> bool val cancel_reservation = impure {interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit /* Exception delegation: given an exception and the privilege at which diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index 64fe15696..91155e23b 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -97,11 +97,7 @@ function pt_walk(sv_params, let pte_offset = vpn_j << sv_params.log_pte_size_bytes; let pte_addr = pt_base + pte_offset; - // In Sv32, physical addrs are actually 34 bits, not XLEN(=32) bits. - // Below, 'pte_phys_addr' is XLEN bits because it's an arg to - // 'mem_read_priv()' [riscv_mem.sail] where it's declared as xlenbits. - // That def and this use need to be fixed together (TODO) - let pte_phys_addr : physaddr = physaddr(pte_addr[(xlen - 1) .. 0]); + let pte_phys_addr : physaddr = physaddr(pte_addr[(physaddrbits_len - 1) .. 0]); // Read this-level PTE from mem let mem_result = mem_read_priv(Read(Data), // AccessType @@ -320,7 +316,7 @@ function translate_TLB_hit(sv_params : SV_Params, // Writeback the PTE (which has new A/D bits) let n_ent = {ent with pte=pte'}; write_TLB(tlb_index, n_ent); - let pte_phys_addr = physaddr(ent.pteAddr[(xlen - 1) .. 0]); + let pte_phys_addr = physaddr(ent.pteAddr[(physaddrbits_len - 1) .. 0]); match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => (), @@ -366,7 +362,7 @@ function translate_TLB_miss(sv_params : SV_Params, TR_Failure(PTW_PTE_Update(), ext_ptw) else { // Writeback the PTE (which has new A/D bits) - let pte_phys_addr = physaddr(pteAddr[(xlen - 1) .. 0]); + let pte_phys_addr = physaddr(pteAddr[(physaddrbits_len - 1) .. 0]); match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => { @@ -418,7 +414,7 @@ function translateAddr(vAddr : virtaddr, let effPriv : Privilege = effectivePrivilege(ac, mstatus, cur_privilege); let mode : SATPMode = translationMode(effPriv); let (valid_va, sv_params) : (bool, SV_Params) = match mode { - Sbare => return TR_Address(physaddr(virtaddr_bits(vAddr)), init_ext_ptw), + Sbare => return TR_Address(physaddr(zero_extend(virtaddr_bits(vAddr))), init_ext_ptw), Sv32 => (true, sv32_params), Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params), Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params), @@ -439,7 +435,7 @@ function translateAddr(vAddr : virtaddr, init_ext_ptw); // Fixup result PA or exception match tr_result1 { - TR_Address(pa, ext_ptw) => TR_Address(physaddr(truncate(pa, xlen)), ext_ptw), + TR_Address(pa, ext_ptw) => TR_Address(physaddr(truncate(pa, physaddrbits_len)), ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } } diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail index 926f20f74..7b2680c59 100644 --- a/model/riscv_xlen32.sail +++ b/model/riscv_xlen32.sail @@ -10,3 +10,5 @@ // This is done using the smallest/most logarithmic possible value since Sail's // type system works well for multiply and 2^ but not divide and log2. type log2_xlen_bytes : Int = 2 + +type physaddrbits_len : Int = 34 diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail index 9878c7ffa..54db542c4 100644 --- a/model/riscv_xlen64.sail +++ b/model/riscv_xlen64.sail @@ -10,3 +10,5 @@ // This is done using the smallest/most logarithmic possible value since Sail's // type system works well for multiply and 2^ but not divide and log2. type log2_xlen_bytes : Int = 3 + +type physaddrbits_len : Int = 64