diff options
| -rw-r--r-- | model/riscv_mem.sail | 90 | ||||
| -rw-r--r-- | model/riscv_platform.sail | 38 |
2 files changed, 64 insertions, 64 deletions
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 6d761c3..d02c49d 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -20,14 +20,14 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool unsigned(addr) % width == 0 // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = { +function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = { let result = (match (aq, rl, res) { - (false, false, false) => Some(read_ram(Read_plain, addr, width)), - (true, false, false) => Some(read_ram(Read_RISCV_acquire, addr, width)), - (true, true, false) => Some(read_ram(Read_RISCV_strong_acquire, addr, width)), - (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, false, false) => Some(read_ram(Read_plain, paddr, width)), + (true, false, false) => Some(read_ram(Read_RISCV_acquire, paddr, width)), + (true, true, false) => Some(read_ram(Read_RISCV_strong_acquire, paddr, width)), + (false, false, true) => Some(read_ram(Read_RISCV_reserved, paddr, width)), + (true, false, true) => Some(read_ram(Read_RISCV_reserved_acquire, paddr, width)), + (true, true, true) => Some(read_ram(Read_RISCV_reserved_strong_acquire, paddr, width)), (false, true, false) => None(), /* should these be instead throwing error_not_implemented as below? */ (false, true, true) => None() }) : option(bits(8 * 'n)); @@ -36,26 +36,26 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext (Read(Data), None()) => MemException(E_Load_Access_Fault()), (_, None()) => MemException(E_SAMO_Access_Fault()), (_, Some(v)) => { if get_config_print_mem() - then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v)); + then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v)); MemValue(v) } } } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = - if within_mmio_readable(addr, width) - then mmio_read(addr, width) - else if within_phys_mem(addr, width) - then phys_mem_read(t, addr, width, aq, rl, res) +function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = + if within_mmio_readable(paddr, width) + then mmio_read(paddr, width) + else if within_phys_mem(paddr, width) + then phys_mem_read(t, paddr, width, aq, rl, res) else MemException(E_Load_Access_Fault()) /* PMP checks if enabled */ -function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = +function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = if (~ (plat_enable_pmp ())) - then checked_mem_read(t, addr, width, aq, rl, res) + then checked_mem_read(t, paddr, width, aq, rl, res) else { - match pmpCheck(addr, width, t, effectivePrivilege(mstatus, cur_privilege)) { - None() => checked_mem_read(t, addr, width, aq, rl, res), + match pmpCheck(paddr, width, t, effectivePrivilege(mstatus, cur_privilege)) { + None() => checked_mem_read(t, paddr, width, aq, rl, res), Some(e) => MemException(e) } } @@ -86,16 +86,16 @@ $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, rreg, escape} $endif -function mem_read (typ, addr, width, aq, rl, res) = { +function mem_read (typ, paddr, width, aq, rl, res) = { let result : MemoryOpResult(bits(8 * 'n)) = - if (aq | res) & (~ (is_aligned_addr(addr, width))) + 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, addr, width, aq, rl, res) + (_, _, _) => pmp_mem_read(typ, paddr, width, aq, rl, res) }; - rvfi_read(addr, width, result); + rvfi_read(paddr, width, result); result } @@ -131,28 +131,28 @@ function rvfi_write (addr, width, value) = () $endif // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, addr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { - rvfi_write(addr, width, data); - let result = MemValue(write_ram(wk, addr, width, data, meta)); +function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { + rvfi_write(paddr, width, data); + let result = MemValue(write_ram(wk, paddr, width, data, meta)); if get_config_print_mem() - then print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); + then print_mem("mem[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data)); result } /* dispatches to MMIO regions or physical memory regions depending on physical memory map */ -function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> 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(wk, addr, width, data, meta) +function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), meta: mem_meta) -> MemoryOpResult(bool) = + if within_mmio_writable(paddr, width) + then mmio_write(paddr, width, data) + else if within_phys_mem(paddr, width) + then phys_mem_write(wk, paddr, width, data, meta) else MemException(E_SAMO_Access_Fault()) /* PMP checks if enabled */ -function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), ext_acc: ext_access_type, meta: mem_meta) -> MemoryOpResult(bool) = +function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), ext_acc: ext_access_type, meta: mem_meta) -> MemoryOpResult(bool) = if (~ (plat_enable_pmp ())) - then checked_mem_write(wk, addr, width, data, meta) - else match pmpCheck(addr, width, Write(ext_acc), effectivePrivilege(mstatus, cur_privilege)) { - None() => checked_mem_write(wk, addr, width, data, meta), + then checked_mem_write(wk, paddr, width, data, meta) + else match pmpCheck(paddr, width, Write(ext_acc), effectivePrivilege(mstatus, cur_privilege)) { + None() => checked_mem_write(wk, paddr, width, data, meta), Some(e) => MemException(e) } @@ -164,17 +164,17 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, ad * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */ val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} -function mem_write_value_meta (addr, width, value, ext_acc, meta, aq, rl, con) = { - rvfi_write(addr, width, value); - if (rl | con) & (~ (is_aligned_addr(addr, width))) +function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = { + rvfi_write(paddr, width, value); + if (rl | con) & (~ (is_aligned_addr(paddr, width))) then MemException(E_SAMO_Addr_Align()) else match (aq, rl, con) { - (false, false, false) => pmp_mem_write(Write_plain, addr, width, value, ext_acc, meta), - (false, true, false) => pmp_mem_write(Write_RISCV_release, addr, width, value, ext_acc, meta), - (false, false, true) => pmp_mem_write(Write_RISCV_conditional, addr, width, value, ext_acc, meta), - (false, true , true) => pmp_mem_write(Write_RISCV_conditional_release, addr, width, value, ext_acc, meta), - (true, true, false) => pmp_mem_write(Write_RISCV_strong_release, addr, width, value, ext_acc, meta), - (true, true , true) => pmp_mem_write(Write_RISCV_conditional_strong_release, addr, width, value, ext_acc, meta), + (false, false, false) => pmp_mem_write(Write_plain, paddr, width, value, ext_acc, meta), + (false, true, false) => pmp_mem_write(Write_RISCV_release, paddr, width, value, ext_acc, meta), + (false, false, true) => pmp_mem_write(Write_RISCV_conditional, paddr, width, value, ext_acc, meta), + (false, true , true) => pmp_mem_write(Write_RISCV_conditional_release, paddr, width, value, ext_acc, meta), + (true, true, false) => pmp_mem_write(Write_RISCV_strong_release, paddr, width, value, ext_acc, meta), + (true, true , true) => pmp_mem_write(Write_RISCV_conditional_strong_release, paddr, width, value, ext_acc, meta), // throw an illegal instruction here? (true, false, false) => throw(Error_not_implemented("store.aq")), (true, false, true) => throw(Error_not_implemented("sc.aq")) @@ -183,5 +183,5 @@ function mem_write_value_meta (addr, width, value, ext_acc, meta, aq, rl, con) = /* Memory write with a default metadata value. */ val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (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) = - mem_write_value_meta(addr, width, value, default_write_acc, default_meta, aq, rl, con) +function mem_write_value (paddr, width, value, aq, rl, con) = + mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con) diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 35d0960..7cc63cc 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -275,30 +275,30 @@ register htif_exit_code : bits(64) */ val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} -function htif_load(addr, width) = { +function htif_load(paddr, width) = { if get_config_print_platform() - then print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost)); + then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ - if width == 8 & (addr == plat_htif_tohost()) + if width == 8 & (paddr == plat_htif_tohost()) then MemValue(sail_zero_extend(htif_tohost, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ - else if width == 4 & addr == plat_htif_tohost() + else if width == 4 & paddr == plat_htif_tohost() then MemValue(sail_zero_extend(htif_tohost[31..0], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ - else if width == 4 & addr == plat_htif_tohost() + 4 + else if width == 4 & paddr == plat_htif_tohost() + 4 then MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ else MemException(E_Load_Access_Fault()) } /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */ val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg} -function htif_store(addr, width, data) = { +function htif_store(paddr, width, data) = { if get_config_print_platform() - then print_platform("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); + then print_platform("htif[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data)); /* Store the written value so that we can ack it later. */ if width == 8 then { htif_tohost = EXTZ(data) } - else if width == 4 & addr == plat_htif_tohost() + else if width == 4 & paddr == plat_htif_tohost() then { htif_tohost = vector_update_subrange(htif_tohost, 31, 0, data) } - else if width == 4 & addr == plat_htif_tohost() + 4 + else if width == 4 & paddr == plat_htif_tohost() + 4 then { htif_tohost = vector_update_subrange(htif_tohost, 63, 32, data) } else { htif_tohost = EXTZ(data) }; @@ -351,18 +351,18 @@ $else function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false $endif -function mmio_read forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = - if within_clint(addr, width) - then clint_load(addr, width) - else if within_htif_readable(addr, width) & (1 <= 'n) - then htif_load(addr, width) +function mmio_read forall 'n, 0 < 'n <= max_mem_access . (paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = + if within_clint(paddr, width) + then clint_load(paddr, width) + else if within_htif_readable(paddr, width) & (1 <= 'n) + then htif_load(paddr, width) else MemException(E_Load_Access_Fault()) -function mmio_write forall 'n, 0 <'n <= max_mem_access . (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = - if within_clint(addr, width) - then clint_store(addr, width, data) - else if within_htif_writable(addr, width) & 'n <= 8 - then htif_store(addr, width, data) +function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = + if within_clint(paddr, width) + then clint_store(paddr, width, data) + else if within_htif_writable(paddr, width) & 'n <= 8 + then htif_store(paddr, width, data) else MemException(E_SAMO_Access_Fault()) /* Platform initialization and ticking. */ |