Update the os-boot patch.

1 files changed, 39 insertions, 32 deletions

diff --git a/os-boot/os-boot-patch.diff b/os-boot/os-boot-patch.diff
index 03d0c30..f4f1a52 100644
--- a/os-boot/os-boot-patch.diff
+++ b/os-boot/os-boot-patch.diff
@@ -1,42 +1,49 @@
-diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
-index 8e483f8..8c68192 100644
---- a/model/prelude_mem.sail
-+++ b/model/prelude_mem.sail
-@@ -29,8 +29,8 @@ function __RISCV_write (addr, width, data, aq, rl, con) =
-     (false, true,  true)  => __WriteRAM_conditional_release(sizeof(xlen), width, EXTZ(0x0), addr, data),
-     (true,  true,  false) => __WriteRAM_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data),
-     (true,  true,  true)  => __WriteRAM_conditional_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data),
--    (true,  false, false) => false,
--    (true,  false, true)  => false
-+    (true,  false, false) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data),//false
-+    (true,  false, true)  => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data) //false
-   }
- 
- val __TraceMemoryWrite : forall 'n 'm.
 diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
-index 3549e80..1d77e6b 100644
+index 256d6de4..45640229 100644
 --- a/model/riscv_mem.sail
 +++ b/model/riscv_mem.sail
-@@ -88,9 +88,9 @@ function mem_write_ea (addr, width, aq, rl, con) = {
-     (false, true,  false) => MemValue(MEMea_release(addr, width)),
-     (false, false, true)  => MemValue(MEMea_conditional(addr, width)),
-     (false, true , true)  => MemValue(MEMea_conditional_release(addr, width)),
+@@ -28,8 +28,8 @@ function phys_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, widt
+     (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, true, false)  => None(), /* should these be instead throwing error_not_implemented as below? */
+-    (false, true, true)   => None()
++    (false, true, false)  => Some(read_ram(Read_plain, addr, width)),
++    (false, true, true)   => Some(read_ram(Read_plain, addr, width))
+   }) : option(bits(8 * 'n));
+   match (t, result) {
+     (Execute, None()) => MemException(E_Fetch_Access_Fault),
+@@ -91,8 +91,8 @@ function mem_read (typ, addr, width, aq, rl, res) = {
+   if (aq | res) & (~ (is_aligned_addr(addr, 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")),
++    (false, true,  false) => pmp_mem_read(typ, addr, width, aq, rl, res),
++    (false, true,  true)  => pmp_mem_read(typ, addr, width, aq, rl, res),
+     (_, _, _)             => pmp_mem_read(typ, addr, width, aq, rl, res)
+   };
+  rvfi_read(addr, width, result);
+@@ -109,9 +109,9 @@ function mem_write_ea (addr, width, aq, rl, con) = {
+     (false, true,  false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)),
+     (false, false, true)  => MemValue(write_ram_ea(Write_RISCV_conditional, addr, width)),
+     (false, true , true)  => MemValue(write_ram_ea(Write_RISCV_conditional_release, addr, width)),
 -    (true,  false, false) => throw(Error_not_implemented("store.aq")),
-+    (true,  false, false) => MemValue(MEMea(addr, width)),//throw(Error_not_implemented("store.aq")),
-     (true,  true,  false) => MemValue(MEMea_strong_release(addr, width)),
++    (true,  false, false) => MemValue(write_ram_ea(Write_plain, addr, width)),
+     (true,  true,  false) => MemValue(write_ram_ea(Write_RISCV_strong_release, addr, width)),
 -    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-+    (true,  false, true)  => MemValue(MEMea(addr, width)),//throw(Error_not_implemented("sc.aq")),
-     (true,  true , true)  => MemValue(MEMea_conditional_strong_release(addr, width))
++    (true,  false, true)  => MemValue(write_ram_ea(Write_plain, addr, width)),
+     (true,  true , true)  => MemValue(write_ram_ea(Write_RISCV_conditional_strong_release, addr, width))
    }
  }
-@@ -133,8 +133,8 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
-   if (rl | con) & (~ (is_aligned_addr(addr, width)))
-   then MemException(E_SAMO_Addr_Align)
-   else match (aq, rl, con) {
+@@ -176,8 +176,8 @@ function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = {
+     (true,  true,  false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, meta),
+     (true,  true , true)  => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, meta),
+     // throw an illegal instruction here?
 -    (true,  false, false) => throw(Error_not_implemented("store.aq")),
--    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-+    (true,  false, false) => checked_mem_write(addr, width, value, aq, rl, con),//throw(Error_not_implemented("store.aq")),
-+    (true,  false, true)  => checked_mem_write(addr, width, value, aq, rl, con),//throw(Error_not_implemented("sc.aq")),
-     (_, _, _)             => checked_mem_write(addr, width, value, aq, rl, con)
+-    (true,  false, true)  => throw(Error_not_implemented("sc.aq"))
++    (true,  false, false) => pmp_mem_write(Write_plain, addr, width, value, meta),
++    (true,  false, true)  => pmp_mem_write(Write_plain, addr, width, value, meta)
    }
  }
+