diff options
-rw-r--r-- | model/riscv_mem.sail | 8 | ||||
-rw-r--r-- | model/riscv_platform.sail | 32 |
2 files changed, 28 insertions, 12 deletions
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 3fd6f31..25065ab 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -50,10 +50,14 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext /* 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), paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = if within_mmio_readable(paddr, width) - then MemoryOpResult_add_meta(mmio_read(paddr, width), default_meta) + then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta) else if within_phys_mem(paddr, width) then phys_mem_read(t, paddr, width, aq, rl, res, meta) - else MemException(E_Load_Access_Fault()) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } /* PMP checks if enabled */ 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, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) = diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 7cc63cc..7e07cf1 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -142,8 +142,8 @@ let MTIMECMP_BASE_HI : xlenbits = EXTZ(0x04004) let MTIME_BASE : xlenbits = EXTZ(0x0bff8) let MTIME_BASE_HI : xlenbits = EXTZ(0x0bffc) -val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} -function clint_load(addr, width) = { +val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function clint_load(t, addr, width) = { let addr = addr - plat_clint_base (); /* FIXME: For now, only allow exact aligned access. */ if addr == MSIP_BASE & ('n == 8 | 'n == 4) @@ -194,7 +194,11 @@ function clint_load(addr, width) = { else { if get_config_print_platform() then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>"); - MemException(E_Load_Access_Fault()) + match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } } } @@ -274,8 +278,8 @@ register htif_exit_code : bits(64) * dispatched the address. */ -val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} -function htif_load(paddr, width) = { +val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function htif_load(t, paddr, width) = { if get_config_print_platform() then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ @@ -285,7 +289,11 @@ function htif_load(paddr, width) = { then MemValue(sail_zero_extend(htif_tohost[31..0], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ 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()) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } } /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */ @@ -351,12 +359,16 @@ $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 . (paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = +function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(paddr, width) - then clint_load(paddr, width) + then clint_load(t, paddr, width) else if within_htif_readable(paddr, width) & (1 <= 'n) - then htif_load(paddr, width) - else MemException(E_Load_Access_Fault()) + then htif_load(t, paddr, width) + else match t { + Execute() => MemException(E_Fetch_Access_Fault()), + Read(Data) => MemException(E_Load_Access_Fault()), + _ => MemException(E_SAMO_Access_Fault()) + } 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) |