diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/riscv_mem.sail | 18 | ||||
| -rw-r--r-- | riscv/riscv_step.sail | 4 |
2 files changed, 11 insertions, 11 deletions
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 2d59a891..2bcc9797 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -16,12 +16,12 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo MemValue(v) } } -function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */ if t == Data & within_mmio_readable(addr, width) then mmio_read(addr, width) else if within_phys_mem(addr, width) - then phys_mem_read(t, addr, width, false, false, false) + then phys_mem_read(t, addr, width, aq, rl, res) else MemException(E_Load_Access_Fault) /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ @@ -33,12 +33,12 @@ val MEMr_reserved : forall 'n, 'n > 0. (xlenbits, atom('n)) -> Me val MEMr_reserved_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} val MEMr_reserved_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -function MEMr (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_acquire (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_strong_acquire (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_reserved (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_reserved_acquire (addr, width) = checked_mem_read(Data, addr, width) -function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width) +function MEMr (addr, width) = checked_mem_read(Data, addr, width, false, false, false) +function MEMr_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, false) +function MEMr_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, false) +function MEMr_reserved (addr, width) = checked_mem_read(Data, addr, width, false, false, true) +function MEMr_reserved_acquire (addr, width) = checked_mem_read(Data, addr, width, true, false, true) +function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, true) /* NOTE: The rreg effect is due to MMIO. */ val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape} @@ -47,7 +47,7 @@ function mem_read (addr, width, aq, rl, res) = { if (aq | res) & (~ (is_aligned_addr(addr, width))) then MemException(E_Load_Addr_Align) else match (aq, rl, res) { - (false, false, false) => checked_mem_read(Data, addr, width), + (false, false, false) => checked_mem_read(Data, addr, width, false, false, false), (true, false, false) => MEMr_acquire(addr, width), (false, false, true) => MEMr_reserved(addr, width), (true, false, true) => MEMr_reserved_acquire(addr, width), diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail index 8e5a0090..f9675115 100644 --- a/riscv/riscv_step.sail +++ b/riscv/riscv_step.sail @@ -21,7 +21,7 @@ function fetch() -> FetchResult = * well as to generate precise fault addresses in any fetch * exceptions. */ - match checked_mem_read(Instruction, ppclo, 2) { + match checked_mem_read(Instruction, ppclo, 2, false, false, false) { MemException(e) => F_Error(E_Fetch_Access_Fault, PC), MemValue(ilo) => { if isRVC(ilo) then F_RVC(ilo) @@ -30,7 +30,7 @@ function fetch() -> FetchResult = match translateAddr(PChi, Execute, Instruction) { TR_Failure(e) => F_Error(e, PChi), TR_Address(ppchi) => { - match checked_mem_read(Instruction, ppchi, 2) { + match checked_mem_read(Instruction, ppchi, 2, false, false, false) { MemException(e) => F_Error(E_Fetch_Access_Fault, PChi), MemValue(ihi) => F_Base(append(ihi, ilo)) } |