Redesign the physical address check extension point to more closely resemble the other address check extension points.ext_check_phys_mem_alt

This adds a parameterisable exception type and a customisable handler function, although the handler still has to return a RISC-V exception type.

3 files changed, 30 insertions, 25 deletions

diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail
index 33a5060..3d3957d 100644
--- a/model/riscv_addr_checks.sail
+++ b/model/riscv_addr_checks.sail
@@ -54,9 +54,30 @@ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ex
 function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
   ()
 
+
+type ext_phys_addr_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 (ext_phys_addr_error)
+
+/*!
+ * 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 (ext_phys_addr_error)
+
 /* 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 ()
+  Ext_PhysAddr_OK (paddr)
 
 function ext_check_phys_mem_write(write_kind, paddr, size, data, metadata) =
-  Ext_PhysAddr_OK ()
+  Ext_PhysAddr_OK (paddr)
+
+function ext_handle_phys_check_error(err : ext_phys_addr_error) -> ExceptionType =
+  err
diff --git a/model/riscv_addr_checks_common.sail b/model/riscv_addr_checks_common.sail
index 2d1e526..1d1c3e8 100644
--- a/model/riscv_addr_checks_common.sail
+++ b/model/riscv_addr_checks_common.sail
@@ -21,23 +21,7 @@ union Ext_DataAddr_Check ('a : Type) = {
   Ext_DataAddr_Error : 'a
 }
 
-union Ext_PhysAddr_Check = {
-  Ext_PhysAddr_OK : unit,
-  Ext_PhysAddr_Error : ExceptionType
+union Ext_PhysAddr_Check ('a : Type) = {
+  Ext_PhysAddr_OK : xlenbits,
+  Ext_PhysAddr_Error : 'a
 }
-
-/*!
- * 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 3ee5e66..0318335 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -53,8 +53,8 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
   then MemoryOpResult_add_meta(mmio_read(t, paddr, width), default_meta)
   else if within_phys_mem(paddr, width)
   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)
+    Ext_PhysAddr_OK(pa)   => phys_mem_read(t, pa, width, aq, rl, res, meta),
+    Ext_PhysAddr_Error(e) => MemException(ext_handle_phys_check_error(e))
   } else match t {
     Execute()  => MemException(E_Fetch_Access_Fault()),
     Read(Data) => MemException(E_Load_Access_Fault()),
@@ -166,8 +166,8 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
   then mmio_write(paddr, width, data)
   else if within_phys_mem(paddr, width)
   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)
+    Ext_PhysAddr_OK(pa) => phys_mem_write(wk, pa, width, data, meta),
+    Ext_PhysAddr_Error(e)  => MemException(ext_handle_phys_check_error(e))
   }  
   else MemException(E_SAMO_Access_Fault())