Define exception handler delegation.

2 files changed, 38 insertions, 0 deletions

diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 4807e31c..7ed9d977 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -455,6 +455,22 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
   & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite)
   & check_TVM_SATP(csr, p)
 
+/* exception delegation: given an exception and the privilege at which
+ * it occured, returns the privilege at which it should be handled.
+ */
+function exception_delegatee(e : ExceptionType, p : Privilege) ->
+  Privilege = {
+  let idx   = exceptionType_to_nat(e);
+  let super = medeleg.bits()[idx];
+  let user  = sedeleg.bits()[idx];
+  let deleg = if      misa.N() == true & user  then User
+              else if misa.S() == true & super then Supervisor
+              else Machine;
+  /* Ensure there is no transition to a less-privileged mode. */
+  if   privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
+  then p else deleg
+}
+
 /* instruction control flow */
 
 struct sync_exception = {
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index d42af3df..2d184042 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -143,6 +143,28 @@ function exceptionType_to_bits(e) = {
   }
 }
 
+val cast exceptionType_to_nat : ExceptionType -> range(0, 15)
+function exceptionType_to_nat(e) = {
+  match (e) {
+    E_Fetch_Addr_Align => 0,
+    E_Fetch_Access_Fault => 1,
+    E_Illegal_Instr => 2,
+    E_Breakpoint => 3,
+    E_Load_Addr_Align => 4,
+    E_Load_Access_Fault => 5,
+    E_SAMO_Addr_Align => 6,
+    E_SAMO_Access_Fault => 7,
+    E_U_EnvCall => 8,
+    E_S_EnvCall => 9,
+    E_Reserved_10 => 10,
+    E_M_EnvCall => 11,
+    E_Fetch_Page_Fault => 12,
+    E_Load_Page_Fault => 13,
+    E_Reserved_14 => 14,
+    E_SAMO_Page_Fault => 15
+  }
+}
+
 enum InterruptType = {
   I_U_Software,
   I_S_Software,