diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-04-24 17:56:32 -0700 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-04-24 17:58:26 -0700 |
commit | 3442aba5aa6545e76e066a199be45809784d495a (patch) | |
tree | 902e43defc518f9ec7004e288ab1c23165f60d88 /model/riscv_mem.sail | |
parent | ca5788f07ad099c3891a193d4d3d95ea71863961 (diff) | |
download | sail-riscv-3442aba5aa6545e76e066a199be45809784d495a.zip sail-riscv-3442aba5aa6545e76e066a199be45809784d495a.tar.gz sail-riscv-3442aba5aa6545e76e066a199be45809784d495a.tar.bz2 |
Add extended model from cheri-merge.
Diffstat (limited to 'model/riscv_mem.sail')
-rw-r--r-- | model/riscv_mem.sail | 38 |
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) } } |