Add an extension point to allow validation of physical memory accesses.

This is required for implementing memory version support for CHERI.

1 files changed, 21 insertions, 0 deletions

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