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

This is required for implementing memory version support for CHERI.

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 5efe8e3..c5fcde9 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -63,8 +63,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())
@@ -189,7 +191,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 */