diff options
-rw-r--r-- | model/riscv_addr_checks.sail | 7 | ||||
-rw-r--r-- | model/riscv_addr_checks_common.sail | 21 | ||||
-rw-r--r-- | model/riscv_mem.sail | 11 |
3 files changed, 36 insertions, 3 deletions
diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index 318d2a2..33a5060 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -53,3 +53,10 @@ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ex function ext_handle_data_check_error(err : ext_data_addr_error) -> unit = () + +/* Default implementations of these hooks permit all accesses. */ +function ext_check_phys_mem_read (access_type, paddr, size, aquire, release, reserved, read_meta) = + Ext_PhysAddr_OK () + +function ext_check_phys_mem_write(write_kind, paddr, size, data, metadata) = + Ext_PhysAddr_OK () diff --git a/model/riscv_addr_checks_common.sail b/model/riscv_addr_checks_common.sail index 945621d..2d1e526 100644 --- a/model/riscv_addr_checks_common.sail +++ b/model/riscv_addr_checks_common.sail @@ -20,3 +20,24 @@ union Ext_DataAddr_Check ('a : Type) = { Ext_DataAddr_OK : xlenbits, /* Address to use for the data access */ Ext_DataAddr_Error : 'a } + +union Ext_PhysAddr_Check = { + Ext_PhysAddr_OK : unit, + Ext_PhysAddr_Error : ExceptionType +} + +/*! + * Validate a read from physical memory. + * THIS(access_type, paddr, size, aquire, release, reserved, read_meta) should + * return Some(exception) to abort the read or None to allow it to proceed. The + * check is performed after PMP checks and does not apply to MMIO memory. + */ +val ext_check_phys_mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType (ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> Ext_PhysAddr_Check + +/*! + * Validate a write to physical memory. + * THIS(write_kind, paddr, size, data, metadata) should return Some(exception) + * to abort the write or None to allow it to proceed. The check is performed + * after PMP checks and does not apply to MMIO memory. + */ +val ext_check_phys_mem_write : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> Ext_PhysAddr_Check diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 3f90cf6..3ee5e66 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -52,8 +52,10 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType( if within_mmio_readable(paddr, width) 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 match t { + then match ext_check_phys_mem_read(t, paddr, width, aq, rl, res, meta) { + Ext_PhysAddr_OK() => phys_mem_read(t, paddr, width, aq, rl, res, meta), + Ext_PhysAddr_Error(e) => MemException(e) + } else match t { Execute() => MemException(E_Fetch_Access_Fault()), Read(Data) => MemException(E_Load_Access_Fault()), _ => MemException(E_SAMO_Access_Fault()) @@ -163,7 +165,10 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin 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) + then match ext_check_phys_mem_write (wk, paddr, width, data, meta) { + Ext_PhysAddr_OK() => phys_mem_write(wk, paddr, width, data, meta), + Ext_PhysAddr_Error(e) => MemException(e) + } else MemException(E_SAMO_Access_Fault()) /* PMP checks if enabled */ |