Add extended model from cheri-merge.

1 files changed, 26 insertions, 12 deletions

diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index a3b34d5..a1bc1d5 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -94,27 +94,27 @@ function mem_write_ea (addr, width, aq, rl, con) = {
 }
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data : bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = {
+function phys_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta, aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = {
   let result = (match (aq, rl, con) {
-    (false, false, false) => MemValue(__write_mem(Write_plain, sizeof(xlen), addr, width, data)),
-    (false, true,  false) => MemValue(__write_mem(Write_RISCV_release ,sizeof(xlen), addr, width, data)),
-    (false, false, true)  => MemValue(__write_mem(Write_RISCV_conditional, sizeof(xlen), addr, width, data)),
-    (false, true , true)  => MemValue(__write_mem(Write_RISCV_conditional_release, sizeof(xlen), addr, width, data)),
+    (false, false, false) => MemValue(write_ram(Write_plain, addr, width, data, meta)),
+    (false, true,  false) => MemValue(write_ram(Write_RISCV_release, addr, width, data, meta)),
+    (false, false, true)  => MemValue(write_ram(Write_RISCV_conditional, addr, width, data, meta)),
+    (false, true , true)  => MemValue(write_ram(Write_RISCV_conditional_release, addr, width, data, meta)),
     (true,  false, false) => throw(Error_not_implemented("store.aq")),
-    (true,  true,  false) => MemValue(__write_mem(Write_RISCV_strong_release, sizeof(xlen), addr, width, data)),
+    (true,  true,  false) => MemValue(write_ram(Write_RISCV_strong_release, addr, width, data, meta)),
     (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (true,  true , true)  => MemValue(__write_mem(Write_RISCV_conditional_strong_release, sizeof(xlen), addr, width, data))
+    (true,  true , true)  => MemValue(write_ram(Write_RISCV_conditional_strong_release, addr, width, data, meta))
   }) : MemoryOpResult(bool);
   print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   result
 }
 
 // dispatches to MMIO regions or physical memory regions depending on physical memory map
-function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) =
+function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta, aq : bool, rl : bool, con : bool) -> 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(addr, width, data, aq, rl, con)
+  then phys_mem_write(addr, width, data, meta, aq, rl, con)
   else MemException(E_SAMO_Access_Fault)
 
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
@@ -133,9 +133,9 @@ val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit
 function rvfi_write (addr, width, value) = ()
 $endif
 
+/* Memory write with a default metadata value */
 /* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */
-val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, rreg, wreg, escape}
-
+val mem_write_value : forall 'n, 'n > 0. (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) = {
   rvfi_write(addr, width, value);
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
@@ -143,6 +143,20 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   else match (aq, rl, con) {
     (true,  false, false) => throw(Error_not_implemented("store.aq")),
     (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (_, _, _)             => checked_mem_write(addr, width, value, aq, rl, con)
+    (_, _, _)             => checked_mem_write(addr, width, value, default_meta, aq, rl, con)
+  }
+}
+
+/* Memory write with an explicit metadata value */
+/* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */
+val mem_write_value_meta : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function mem_write_value_meta (addr, width, value, meta, aq, rl, con) = {
+  rvfi_write(addr, width, value);
+  if (rl | con) & (~ (is_aligned_addr(addr, width)))
+  then MemException(E_SAMO_Addr_Align)
+  else match (aq, rl, con) {
+    (true,  false, false) => throw(Error_not_implemented("store.aq")),
+    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
+    (_, _, _)             => checked_mem_write(addr, width, value, meta, aq, rl, con)
   }
 }