diff options
-rw-r--r-- | model/riscv_mem.sail | 44 |
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} |