Remove code duplication in mem_readmem_meta_merge

1 files changed, 17 insertions, 27 deletions

diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 25065ab..e34a8f4 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -91,38 +91,28 @@ $endif
 
 /* NOTE: The rreg effect is due to MMIO. */
 $ifdef RVFI_DII
-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 {wreg, rmem, rmemt, rreg, escape}
-val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
+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 {wreg, rmem, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
 $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, rmemt, rreg, escape}
-val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
+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, rmemt, rreg, escape}
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
 $endif
 
-function mem_read (typ, paddr, width, aq, rl, res) = {
- let result : MemoryOpResult(bits(8 * 'n)) =
-  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")),
-    (_, _, _)             => MemoryOpResult_drop_meta(pmp_mem_read(typ, paddr, width, aq, rl, res, false))
-  };
- rvfi_read(paddr, width, result);
- result
+function mem_read_meta (typ, paddr, width, aq, rl, res, meta) = {
+  let result : MemoryOpResult((bits(8 * 'n), mem_meta)) =
+    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, paddr, width, aq, rl, res, meta)
+    };
+  rvfi_read(paddr, width, MemoryOpResult_drop_meta(result));
+  result
 }
 
-function mem_read_meta (typ, addr, width, aq, rl, res) = {
- let result : MemoryOpResult((bits(8 * 'n), mem_meta)) =
-  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")),
-    (_, _, _)             => pmp_mem_read(typ, addr, width, aq, rl, res, true)
-  };
- rvfi_read(addr, width, MemoryOpResult_drop_meta(result));
- result
-}
+function mem_read (typ, paddr, width, aq, rl, res) =
+  MemoryOpResult_drop_meta(mem_read_meta(typ, paddr, width, aq, rl, res, false))
 
 val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}