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

@@ -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(),

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

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) = ()

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) = {

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

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)
     }
   }

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

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