Squashed commit of various patches from @scottj97:

    Rename var to make it clear it is physical and not virtual.

    There are a lot of variables in riscv_mem.sail and riscv_platform.sail named addr and it's not always clear if that is physical or virtual address. These changes rename those variables to paddr to reduce ambiguity.

2 files changed, 64 insertions, 64 deletions

diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 6d761c3..d02c49d 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -20,14 +20,14 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool
   unsigned(addr) % width == 0
 
 // 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), addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
+function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = {
   let result = (match (aq, rl, res) {
-    (false, false, false) => Some(read_ram(Read_plain, addr, width)),
-    (true, false, false)  => Some(read_ram(Read_RISCV_acquire, addr, width)),
-    (true, true, false)   => Some(read_ram(Read_RISCV_strong_acquire, addr, width)),
-    (false, false, true)  => Some(read_ram(Read_RISCV_reserved, addr, width)),
-    (true, false, true)   => Some(read_ram(Read_RISCV_reserved_acquire, addr, width)),
-    (true, true, true)    => Some(read_ram(Read_RISCV_reserved_strong_acquire, addr, width)),
+    (false, false, false) => Some(read_ram(Read_plain, paddr, width)),
+    (true, false, false)  => Some(read_ram(Read_RISCV_acquire, paddr, width)),
+    (true, true, false)   => Some(read_ram(Read_RISCV_strong_acquire, paddr, width)),
+    (false, false, true)  => Some(read_ram(Read_RISCV_reserved, paddr, width)),
+    (true, false, true)   => Some(read_ram(Read_RISCV_reserved_acquire, paddr, width)),
+    (true, true, true)    => Some(read_ram(Read_RISCV_reserved_strong_acquire, paddr, width)),
     (false, true, false)  => None(), /* should these be instead throwing error_not_implemented as below? */
     (false, true, true)   => None()
   }) : option(bits(8 * 'n));
@@ -36,26 +36,26 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext
     (Read(Data), None()) => MemException(E_Load_Access_Fault()),
     (_,          None()) => MemException(E_SAMO_Access_Fault()),
     (_,         Some(v)) => { if   get_config_print_mem()
-                              then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+                              then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v));
                               MemValue(v) }
   }
 }
 
 /* dispatches to MMIO regions or physical memory regions depending on physical memory map */
-function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
-  if   within_mmio_readable(addr, width)
-  then mmio_read(addr, width)
-  else if within_phys_mem(addr, width)
-  then phys_mem_read(t, addr, width, aq, rl, res)
+function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+  if   within_mmio_readable(paddr, width)
+  then mmio_read(paddr, width)
+  else if within_phys_mem(paddr, width)
+  then phys_mem_read(t, paddr, width, aq, rl, res)
   else MemException(E_Load_Access_Fault())
 
 /* PMP checks if enabled */
-function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
   if   (~ (plat_enable_pmp ()))
-  then checked_mem_read(t, addr, width, aq, rl, res)
+  then checked_mem_read(t, paddr, width, aq, rl, res)
   else {
-    match pmpCheck(addr, width, t, effectivePrivilege(mstatus, cur_privilege)) {
-      None()  => checked_mem_read(t, addr, width, aq, rl, res),
+    match pmpCheck(paddr, width, t, effectivePrivilege(mstatus, cur_privilege)) {
+      None()  => checked_mem_read(t, paddr, width, aq, rl, res),
       Some(e) => MemException(e)
     }
   }
@@ -86,16 +86,16 @@ $else
 val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
 $endif
 
-function mem_read (typ, addr, width, aq, rl, res) = {
+function mem_read (typ, paddr, width, aq, rl, res) = {
  let result : MemoryOpResult(bits(8 * 'n)) =
-  if (aq | res) & (~ (is_aligned_addr(addr, width)))
+  if (aq | res) & (~ (is_aligned_addr(paddr, width)))
   then MemException(E_Load_Addr_Align())
   else match (aq, rl, res) {
     (false, true,  false) => throw(Error_not_implemented("load.rl")),
     (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (_, _, _)             => pmp_mem_read(typ, addr, width, aq, rl, res)
+    (_, _, _)             => pmp_mem_read(typ, paddr, width, aq, rl, res)
   };
- rvfi_read(addr, width, result);
+ rvfi_read(paddr, width, result);
  result
 }
 
@@ -131,28 +131,28 @@ function rvfi_write (addr, width, value) = ()
 $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, addr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = {
-  rvfi_write(addr, width, data);
-  let result = MemValue(write_ram(wk, addr, width, data, meta));
+function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = {
+  rvfi_write(paddr, width, data);
+  let result = MemValue(write_ram(wk, paddr, width, data, meta));
   if   get_config_print_mem()
-  then print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  then print_mem("mem[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data));
   result
 }
 
 /* dispatches to MMIO regions or physical memory regions depending on physical memory map */
-function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) =
-  if   within_mmio_writable(addr, width)
-  then mmio_write(addr, width, data)
-  else if within_phys_mem(addr, width)
-  then phys_mem_write(wk, addr, width, data, meta)
+function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) =
+  if   within_mmio_writable(paddr, width)
+  then mmio_write(paddr, width, data)
+  else if within_phys_mem(paddr, width)
+  then phys_mem_write(wk, paddr, width, data, meta)
   else MemException(E_SAMO_Access_Fault())
 
 /* PMP checks if enabled */
-function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), ext_acc: ext_access_type, meta: mem_meta) -> MemoryOpResult(bool) =
+function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), ext_acc: ext_access_type, meta: mem_meta) -> MemoryOpResult(bool) =
   if   (~ (plat_enable_pmp ()))
-  then checked_mem_write(wk, addr, width, data, meta)
-  else match pmpCheck(addr, width, Write(ext_acc), effectivePrivilege(mstatus, cur_privilege)) {
-         None()  => checked_mem_write(wk, addr, width, data, meta),
+  then checked_mem_write(wk, paddr, width, data, meta)
+  else match pmpCheck(paddr, width, Write(ext_acc), effectivePrivilege(mstatus, cur_privilege)) {
+         None()  => checked_mem_write(wk, paddr, width, data, meta),
          Some(e) => MemException(e)
   }
 
@@ -164,17 +164,17 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, ad
  * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime.
  */
 val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
-function mem_write_value_meta (addr, width, value, ext_acc, meta, aq, rl, con) = {
-  rvfi_write(addr, width, value);
-  if (rl | con) & (~ (is_aligned_addr(addr, width)))
+function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = {
+  rvfi_write(paddr, width, value);
+  if (rl | con) & (~ (is_aligned_addr(paddr, width)))
   then MemException(E_SAMO_Addr_Align())
   else match (aq, rl, con) {
-    (false, false, false) => pmp_mem_write(Write_plain, addr, width, value, ext_acc, meta),
-    (false, true,  false) => pmp_mem_write(Write_RISCV_release, addr, width, value, ext_acc, meta),
-    (false, false, true)  => pmp_mem_write(Write_RISCV_conditional, addr, width, value, ext_acc, meta),
-    (false, true , true)  => pmp_mem_write(Write_RISCV_conditional_release, addr, width, value, ext_acc, meta),
-    (true,  true,  false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, ext_acc, meta),
-    (true,  true , true)  => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, ext_acc, meta),
+    (false, false, false) => pmp_mem_write(Write_plain, paddr, width, value, ext_acc, meta),
+    (false, true,  false) => pmp_mem_write(Write_RISCV_release, paddr, width, value, ext_acc, meta),
+    (false, false, true)  => pmp_mem_write(Write_RISCV_conditional, paddr, width, value, ext_acc, meta),
+    (false, true , true)  => pmp_mem_write(Write_RISCV_conditional_release, paddr, width, value, ext_acc, meta),
+    (true,  true,  false) => pmp_mem_write(Write_RISCV_strong_release, paddr, width, value, ext_acc, meta),
+    (true,  true , true)  => pmp_mem_write(Write_RISCV_conditional_strong_release, paddr, width, value, ext_acc, meta),
     // throw an illegal instruction here?
     (true,  false, false) => throw(Error_not_implemented("store.aq")),
     (true,  false, true)  => throw(Error_not_implemented("sc.aq"))
@@ -183,5 +183,5 @@ function mem_write_value_meta (addr, width, value, ext_acc, meta, aq, rl, con) =
 
 /* Memory write with a default metadata value. */
 val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
-function mem_write_value (addr, width, value, aq, rl, con) =
-  mem_write_value_meta(addr, width, value, default_write_acc, default_meta, aq, rl, con)
+function mem_write_value (paddr, width, value, aq, rl, con) =
+  mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con)
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 35d0960..7cc63cc 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -275,30 +275,30 @@ register htif_exit_code : bits(64)
  */
 
 val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
-function htif_load(addr, width) = {
+function htif_load(paddr, width) = {
   if   get_config_print_platform()
-  then print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost));
+  then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost));
   /* FIXME: For now, only allow the expected access widths. */
-  if      width == 8 & (addr == plat_htif_tohost())
+  if      width == 8 & (paddr == plat_htif_tohost())
   then    MemValue(sail_zero_extend(htif_tohost, 64))         /* FIXME: Redundant zero_extend currently required by Lem backend */
-  else if width == 4 & addr == plat_htif_tohost()
+  else if width == 4 & paddr == plat_htif_tohost()
   then    MemValue(sail_zero_extend(htif_tohost[31..0], 32))  /* FIXME: Redundant zero_extend currently required by Lem backend */
-  else if width == 4 & addr == plat_htif_tohost() + 4
+  else if width == 4 & paddr == plat_htif_tohost() + 4
   then    MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */
   else    MemException(E_Load_Access_Fault())
 }
 
 /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */
 val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg}
-function htif_store(addr, width, data) = {
+function htif_store(paddr, width, data) = {
   if   get_config_print_platform()
-  then print_platform("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  then print_platform("htif[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data));
   /* Store the written value so that we can ack it later. */
   if      width == 8
   then    { htif_tohost = EXTZ(data) }
-  else if width == 4 & addr == plat_htif_tohost()
+  else if width == 4 & paddr == plat_htif_tohost()
   then    { htif_tohost = vector_update_subrange(htif_tohost, 31, 0, data) }
-  else if width == 4 & addr == plat_htif_tohost() + 4
+  else if width == 4 & paddr == plat_htif_tohost() + 4
   then    { htif_tohost = vector_update_subrange(htif_tohost, 63, 32, data) }
   else    { htif_tohost = EXTZ(data) };
 
@@ -351,18 +351,18 @@ $else
 function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
 $endif
 
-function mmio_read forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
-  if   within_clint(addr, width)
-  then clint_load(addr, width)
-  else if within_htif_readable(addr, width) & (1 <= 'n)
-  then htif_load(addr, width)
+function mmio_read forall 'n, 0 < 'n <= max_mem_access . (paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
+  if   within_clint(paddr, width)
+  then clint_load(paddr, width)
+  else if within_htif_readable(paddr, width) & (1 <= 'n)
+  then htif_load(paddr, width)
   else MemException(E_Load_Access_Fault())
 
-function mmio_write forall 'n, 0 <'n <= max_mem_access . (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
-  if   within_clint(addr, width)
-  then clint_store(addr, width, data)
-  else if within_htif_writable(addr, width) & 'n <= 8
-  then htif_store(addr, width, data)
+function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
+  if   within_clint(paddr, width)
+  then clint_store(paddr, width, data)
+  else if within_htif_writable(paddr, width) & 'n <= 8
+  then htif_store(paddr, width, data)
   else MemException(E_SAMO_Access_Fault())
 
 /* Platform initialization and ticking. */