2 files changed, 25 insertions, 6 deletions
diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 31ec09c4..be926f6a 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -13,31 +13,37 @@ bool plat_enable_misaligned_access(unit u)
 
 mach_bits plat_ram_base(unit u)
 {
+  fprintf(stderr, "plat_ram_base: -> %0" PRIx64 "\n", rv_ram_base);
   return rv_ram_base;
 }
 
 mach_bits plat_ram_size(unit u)
 {
+  fprintf(stderr, "plat_ram_size: -> %0" PRIx64 "\n", rv_ram_size);
   return rv_rom_base;
 }
 
 mach_bits plat_rom_base(unit u)
 {
+  fprintf(stderr, "plat_rom_base: -> %0" PRIx64 "\n", rv_rom_base);
   return rv_rom_base;
 }
 
 mach_bits plat_rom_size(unit u)
 {
+  fprintf(stderr, "plat_rom_size: -> %0" PRIx64 "\n", rv_rom_size);
   return rv_rom_size;
 }
 
 mach_bits plat_clint_base(unit u)
 {
+  fprintf(stderr, "plat_clint_base: -> %0" PRIx64 "\n", rv_clint_base);
   return rv_clint_base;
 }
 
 mach_bits plat_clint_size(unit u)
 {
+  fprintf(stderr, "plat_clint_size: -> %0" PRIx64 "\n", rv_clint_size);
   return rv_clint_size;
 }
 
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 80f546b8..c4af9c79 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -42,15 +42,28 @@ function phys_mem_segments() =
 
 /* Physical memory map predicates */
 
-function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool = {
+  let ram_base = plat_ram_base ();
+  let rom_base = plat_rom_base ();
+  let ram_size = plat_ram_size ();
+  let rom_size = plat_rom_size ();
+
   /* todo: iterate over segment list */
-  if (  plat_ram_base() <=_u addr
-      & (addr + sizeof('n)) <=_u (plat_ram_base() + plat_ram_size ()))
+  if (  ram_base <=_u addr
+      & (addr + sizeof('n)) <=_u (ram_base + ram_size))
        then true
-  else if (  plat_rom_base() <=_u addr
-           & (addr + sizeof('n)) <=_u (plat_rom_base() + plat_rom_size()))
+  else if (  rom_base <=_u addr
+           & (addr + sizeof('n)) <=_u (rom_base + rom_size))
        then true
-  else false
+  else {
+    print("within_phys_mem: " ^ BitStr(addr) ^ " not within phys-mem:");
+    print("  plat_rom_base: " ^ BitStr(rom_base));
+    print("  plat_rom_size: " ^ BitStr(rom_size));
+    print("  plat_ram_base: " ^ BitStr(ram_base));
+    print("  plat_ram_size: " ^ BitStr(ram_size));
+    false
+  }
+}
 
 function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
     plat_clint_base() <=_u addr