Make a custom exception code available for extensions, and remove the E_CHERI code. Enable extensions for PTE checks and PTW errors, and propagate those into exception codes.

14 files changed, 317 insertions, 241 deletions

diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index d615691..f2f88b7 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -13,7 +13,7 @@ function fetch() -> FetchResult =
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
       if   (use_pc[0] != 0b0 | (use_pc[1] != 0b0 & (~ (haveRVC()))))
-      then F_Error(E_Fetch_Addr_Align, PC)
+      then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e)     => F_Error(e, PC),
         TR_Address(ppclo) => {
@@ -22,7 +22,7 @@ function fetch() -> FetchResult =
            * exceptions.
            */
           match mem_read(Execute(), ppclo, 2, false, false, false) {
-            MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
+            MemException(e) => F_Error(E_Fetch_Access_Fault(), PC),
             MemValue(ilo)   => {
               if   isRVC(ilo)
               then F_RVC(ilo)
@@ -36,7 +36,7 @@ function fetch() -> FetchResult =
                       TR_Failure(e)     => F_Error(e, PC_hi),
                       TR_Address(ppchi) => {
                         match mem_read(Execute(), ppchi, 2, false, false, false) {
-                          MemException(e) => F_Error(E_Fetch_Access_Fault, PC_hi),
+                          MemException(e) => F_Error(E_Fetch_Access_Fault(), PC_hi),
                           MemValue(ihi)   => F_Base(append(ihi, ilo))
                         }
                       }
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index a9d6be7..5ed1b6d 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -61,7 +61,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
          * - Andrew Waterman, isa-dev, 10 Jul 2018.
          */
         if (~ (aligned))
-        then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
+        then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
         else match translateAddr(vaddr, Read(Data)) {
                TR_Failure(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
                TR_Address(addr) =>
@@ -117,7 +117,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
               DOUBLE => vaddr[2..0] == 0b000
             };
           if (~ (aligned))
-          then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL }
+          then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
           else {
             if match_reservation(vaddr) == false then {
               /* cannot happen in rmem */
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 10f3117..bdd60ce 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -61,7 +61,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
       /* Perform standard alignment check */
       if   target[1] & (~ (haveRVC()))
       then {
-        handle_mem_exception(target, E_Fetch_Addr_Align);
+        handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
       } else {
         X(rd) = get_next_pc();
@@ -124,7 +124,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
       },
       Ext_ControlAddr_OK(target) => {
         if target[1] & (~ (haveRVC())) then {
-          handle_mem_exception(target, E_Fetch_Addr_Align);
+          handle_mem_exception(target, E_Fetch_Addr_Align());
           RETIRE_FAIL;
         } else {
           set_next_pc(target);
@@ -322,7 +322,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
-      then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL }
+      then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
       else match translateAddr(vaddr, Read(Data)) {
         TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
         TR_Address(addr) =>
@@ -377,7 +377,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
-      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); RETIRE_FAIL }
+      then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
       else match translateAddr(vaddr, Write(Data)) {
         TR_Failure(e)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
         TR_Address(addr) => {
@@ -695,9 +695,9 @@ mapping clause encdec = ECALL()
 function clause execute ECALL() = {
   let t : sync_exception =
     struct { trap = match (cur_privilege) {
-                      User       => E_U_EnvCall,
-                      Supervisor => E_S_EnvCall,
-                      Machine    => E_M_EnvCall
+                      User       => E_U_EnvCall(),
+                      Supervisor => E_S_EnvCall(),
+                      Machine    => E_M_EnvCall()
                     },
              excinfo = (None() : option(xlenbits)),
              ext     = None() };
@@ -750,7 +750,7 @@ mapping clause encdec = EBREAK()
   <-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute EBREAK() = {
-  handle_mem_exception(PC, E_Breakpoint);
+  handle_mem_exception(PC, E_Breakpoint());
   RETIRE_FAIL
 }
 
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index 5b37c78..1af2910 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -18,7 +18,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
       let  target = [addr with 0 = bitzero];  /* clear addr[0] */
       if   target[1] & (~ (haveRVC()))
       then {
-        handle_mem_exception(target, E_Fetch_Addr_Align);
+        handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
       } else {
         X(rd) = get_next_pc();
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index b62caf8..6d761c3 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -32,9 +32,9 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext
     (false, true, true)   => None()
   }) : option(bits(8 * 'n));
   match (t, result) {
-    (Execute(),  None()) => MemException(E_Fetch_Access_Fault),
-    (Read(Data), None()) => MemException(E_Load_Access_Fault),
-    (_,          None()) => MemException(E_SAMO_Access_Fault),
+    (Execute(),  None()) => MemException(E_Fetch_Access_Fault()),
+    (Read(Data), None()) => MemException(E_Load_Access_Fault()),
+    (_,          None()) => MemException(E_SAMO_Access_Fault()),
     (_,         Some(v)) => { if   get_config_print_mem()
                               then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
                               MemValue(v) }
@@ -47,7 +47,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
   then mmio_read(addr, width)
   else if within_phys_mem(addr, width)
   then phys_mem_read(t, addr, width, aq, rl, res)
-  else MemException(E_Load_Access_Fault)
+  else MemException(E_Load_Access_Fault())
 
 /* PMP checks if enabled */
 function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
@@ -89,7 +89,7 @@ $endif
 function mem_read (typ, addr, width, aq, rl, res) = {
  let result : MemoryOpResult(bits(8 * 'n)) =
   if (aq | res) & (~ (is_aligned_addr(addr, width)))
-  then MemException(E_Load_Addr_Align)
+  then MemException(E_Load_Addr_Align())
   else match (aq, rl, res) {
     (false, true,  false) => throw(Error_not_implemented("load.rl")),
     (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
@@ -103,7 +103,7 @@ val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bo
 
 function mem_write_ea (addr, width, aq, rl, con) = {
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
-  then MemException(E_SAMO_Addr_Align)
+  then MemException(E_SAMO_Addr_Align())
   else match (aq, rl, con) {
     (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)),
     (false, true,  false) => MemValue(write_ram_ea(Write_RISCV_release, addr, width)),
@@ -145,7 +145,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
   then mmio_write(addr, width, data)
   else if within_phys_mem(addr, width)
   then phys_mem_write(wk, addr, width, data, meta)
-  else MemException(E_SAMO_Access_Fault)
+  else MemException(E_SAMO_Access_Fault())
 
 /* PMP checks if enabled */
 function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, addr : xlenbits, width : atom('n), data: bits(8 * 'n), ext_acc: ext_access_type, meta: mem_meta) -> MemoryOpResult(bool) =
@@ -167,7 +167,7 @@ val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom
 function mem_write_value_meta (addr, width, value, ext_acc, meta, aq, rl, con) = {
   rvfi_write(addr, width, value);
   if (rl | con) & (~ (is_aligned_addr(addr, width)))
-  then MemException(E_SAMO_Addr_Align)
+  then MemException(E_SAMO_Addr_Align())
   else match (aq, rl, con) {
     (false, false, false) => pmp_mem_write(Write_plain, addr, width, value, ext_acc, meta),
     (false, true,  false) => pmp_mem_write(Write_RISCV_release, addr, width, value, ext_acc, meta),
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 52511a9..dac7490 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -194,7 +194,7 @@ function clint_load(addr, width) = {
   else {
     if   get_config_print_platform()
     then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
-    MemException(E_Load_Access_Fault)
+    MemException(E_Load_Access_Fault())
   }
 }
 
@@ -240,7 +240,7 @@ function clint_store(addr, width, data) = {
   } else {
     if   get_config_print_platform()
     then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)");
-    MemException(E_SAMO_Access_Fault)
+    MemException(E_SAMO_Access_Fault())
   }
 }
 
@@ -285,7 +285,7 @@ function htif_load(addr, width) = {
   then    MemValue(sail_zero_extend(htif_tohost[31..0], 32))  /* FIXME: Redundant zero_extend currently required by Lem backend */
   else if width == 4 & addr == plat_htif_tohost() + 4
   then    MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */
-  else    MemException(E_Load_Access_Fault)
+  else    MemException(E_Load_Access_Fault())
 }
 
 /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */
@@ -356,14 +356,14 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width
   then clint_load(addr, width)
   else if within_htif_readable(addr, width) & (1 <= 'n)
   then htif_load(addr, width)
-  else MemException(E_Load_Access_Fault)
+  else MemException(E_Load_Access_Fault())
 
 function mmio_write forall 'n, 0 <'n <= max_mem_access . (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) =
   if   within_clint(addr, width)
   then clint_store(addr, width, data)
   else if within_htif_writable(addr, width) & 'n <= 8
   then htif_store(addr, width, data)
-  else MemException(E_SAMO_Access_Fault)
+  else MemException(E_SAMO_Access_Fault())
 
 /* Platform initialization and ticking. */
 
@@ -383,7 +383,7 @@ function handle_illegal() -> unit = {
   let info = if plat_mtval_has_illegal_inst_bits ()
              then Some(instbits)
              else None();
-  let t : sync_exception = struct { trap    = E_Illegal_Instr,
+  let t : sync_exception = struct { trap    = E_Illegal_Instr(),
                                     excinfo = info,
                                     ext     = None() };
   set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC))
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index c1de35c..117de6d 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -158,10 +158,10 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
   if   check
   then None()
   else match acc {
-    Read(Data)      => Some(E_Load_Access_Fault),
-    Write(Data)     => Some(E_SAMO_Access_Fault),
-    ReadWrite(Data) => Some(E_SAMO_Access_Fault),
-    Execute()       => Some(E_Fetch_Access_Fault)
+    Read(Data)      => Some(E_Load_Access_Fault()),
+    Write(Data)     => Some(E_SAMO_Access_Fault()),
+    ReadWrite(Data) => Some(E_SAMO_Access_Fault()),
+    Execute()       => Some(E_Fetch_Access_Fault())
   }
 }
 
diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
index 87a9f08..22a023e 100644
--- a/model/riscv_pte.sail
+++ b/model/riscv_pte.sail
@@ -28,17 +28,26 @@ function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
   a.V() == false | (a.W() == true & a.R() == false)
 }
 
-function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte) -> bool = {
+union PTE_Check = {
+  PTE_Check_Success : unit,
+  PTE_Check_Failure : unit,
+  PTE_Check_Ext     : ext_pte_error
+}
+
+function to_pte_check(b : bool) -> PTE_Check =
+  if b then PTE_Check_Success() else PTE_Check_Failure(())
+
+function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte) -> PTE_Check = {
   match (ac, priv) {
-    (Read(Data),      User)       => p.U() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Write(Data),     User)       => p.U() == true & p.W() == true,
-    (ReadWrite(Data), User)       => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Execute(),       User)       => p.U() == true & p.X() == true,
-
-    (Read(Data),      Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)),
-    (Write(Data),     Supervisor) => (p.U() == false | do_sum) & p.W() == true,
-    (ReadWrite(Data), Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Execute(),       Supervisor) => p.U() == false & p.X() == true,
+    (Read(Data),      User)       => to_pte_check(p.U() == true & (p.R() == true | (p.X() == true & mxr))),
+    (Write(Data),     User)       => to_pte_check(p.U() == true & p.W() == true),
+    (ReadWrite(Data), User)       => to_pte_check(p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr))),
+    (Execute(),       User)       => to_pte_check(p.U() == true & p.X() == true),
+
+    (Read(Data),      Supervisor) => to_pte_check((p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr))),
+    (Write(Data),     Supervisor) => to_pte_check((p.U() == false | do_sum) & p.W() == true),
+    (ReadWrite(Data), Supervisor) => to_pte_check((p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr))),
+    (Execute(),       Supervisor) => to_pte_check(p.U() == false & p.X() == true),
 
     (_,               Machine)    => internal_error("m-mode mem perm check")
   }
diff --git a/model/riscv_ptw.sail b/model/riscv_ptw.sail
index e2056b4..1675593 100644
--- a/model/riscv_ptw.sail
+++ b/model/riscv_ptw.sail
@@ -1,19 +1,23 @@
 /* failure modes for address-translation/page-table-walks */
-enum PTW_Error = {
-  PTW_Access,       /* physical memory access error for a PTE */
-  PTW_Invalid_PTE,
-  PTW_No_Permission,
-  PTW_Misaligned,   /* misaligned superpage */
-  PTW_PTE_Update    /* PTE update needed but not enabled */
+
+union PTW_Error = {
+  PTW_Access        : unit,          /* physical memory access error for a PTE */
+  PTW_Invalid_PTE   : unit,
+  PTW_No_Permission : unit,
+  PTW_Misaligned    : unit,          /* misaligned superpage */
+  PTW_PTE_Update    : unit,          /* PTE update needed but not enabled */
+  PTW_Ext_Error     : ext_ptw_error  /* parameterized for errors from extensions */
 }
+
 val ptw_error_to_str : PTW_Error -> string
 function ptw_error_to_str(e) =
   match (e) {
-    PTW_Access        => "mem-access-error",
-    PTW_Invalid_PTE   => "invalid-pte",
-    PTW_No_Permission => "no-permission",
-    PTW_Misaligned    => "misaligned-superpage",
-    PTW_PTE_Update    => "pte-update-needed"
+    PTW_Access()         => "mem-access-error",
+    PTW_Invalid_PTE()    => "invalid-pte",
+    PTW_No_Permission()  => "no-permission",
+    PTW_Misaligned()     => "misaligned-superpage",
+    PTW_PTE_Update()     => "pte-update-needed",
+    PTW_Ext_Error(e)     => "extension-error"
   }
 
 overload to_str = {ptw_error_to_str}
@@ -22,14 +26,15 @@ overload to_str = {ptw_error_to_str}
 function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = {
   let e : ExceptionType =
   match (a, f) {
-    (ReadWrite(Data), PTW_Access) => E_SAMO_Access_Fault,
-    (ReadWrite(Data), _)          => E_SAMO_Page_Fault,
-    (Read(Data), PTW_Access)      => E_Load_Access_Fault,
-    (Read(Data), _)               => E_Load_Page_Fault,
-    (Write(Data), PTW_Access)     => E_SAMO_Access_Fault,
-    (Write(Data), _)              => E_SAMO_Page_Fault,
-    (Execute(), PTW_Access)       => E_Fetch_Access_Fault,
-    (Execute(), _)                => E_Fetch_Page_Fault
+    (_, PTW_Ext_Error(e))           => E_Extension(ext_translate_exception(e)),
+    (ReadWrite(Data), PTW_Access()) => E_SAMO_Access_Fault(),
+    (ReadWrite(Data), _)            => E_SAMO_Page_Fault(),
+    (Read(Data), PTW_Access())      => E_Load_Access_Fault(),
+    (Read(Data), _)                 => E_Load_Page_Fault(),
+    (Write(Data), PTW_Access())     => E_SAMO_Access_Fault(),
+    (Write(Data), _)                => E_SAMO_Page_Fault(),
+    (Execute(), PTW_Access())       => E_Fetch_Access_Fault(),
+    (Execute(), _)                  => E_Fetch_Page_Fault()
   } in {
 /*  print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
     e
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index e0a1f45..f61674c 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -138,74 +138,99 @@ function interruptType_to_bits (i) =
 
 /* architectural exception definitions */
 
-enum ExceptionType = {
- E_Fetch_Addr_Align,
- E_Fetch_Access_Fault,
- E_Illegal_Instr,
- E_Breakpoint,
- E_Load_Addr_Align,
- E_Load_Access_Fault,
- E_SAMO_Addr_Align,
- E_SAMO_Access_Fault,
- E_U_EnvCall,
- E_S_EnvCall,
- E_Reserved_10,
- E_M_EnvCall,
- E_Fetch_Page_Fault,
- E_Load_Page_Fault,
- E_Reserved_14,
- E_SAMO_Page_Fault,
+union ExceptionType = {
+ E_Fetch_Addr_Align   : unit,
+ E_Fetch_Access_Fault : unit,
+ E_Illegal_Instr      : unit,
+ E_Breakpoint         : unit,
+ E_Load_Addr_Align    : unit,
+ E_Load_Access_Fault  : unit,
+ E_SAMO_Addr_Align    : unit,
+ E_SAMO_Access_Fault  : unit,
+ E_U_EnvCall          : unit,
+ E_S_EnvCall          : unit,
+ E_Reserved_10        : unit,
+ E_M_EnvCall          : unit,
+ E_Fetch_Page_Fault   : unit,
+ E_Load_Page_Fault    : unit,
+ E_Reserved_14        : unit,
+ E_SAMO_Page_Fault    : unit,
 
  /* extensions */
- E_CHERI
+ E_Extension          : ext_exc_type
 }
 
 val cast exceptionType_to_bits : ExceptionType -> exc_code
 function exceptionType_to_bits(e) =
   match (e) {
-    E_Fetch_Addr_Align   => 0x00,
-    E_Fetch_Access_Fault => 0x01,
-    E_Illegal_Instr      => 0x02,
-    E_Breakpoint         => 0x03,
-    E_Load_Addr_Align    => 0x04,
-    E_Load_Access_Fault  => 0x05,
-    E_SAMO_Addr_Align    => 0x06,
-    E_SAMO_Access_Fault  => 0x07,
-    E_U_EnvCall          => 0x08,
-    E_S_EnvCall          => 0x09,
-    E_Reserved_10        => 0x0a,
-    E_M_EnvCall          => 0x0b,
-    E_Fetch_Page_Fault   => 0x0c,
-    E_Load_Page_Fault    => 0x0d,
-    E_Reserved_14        => 0x0e,
-    E_SAMO_Page_Fault    => 0x0f,
+    E_Fetch_Addr_Align()   => 0x00,
+    E_Fetch_Access_Fault() => 0x01,
+    E_Illegal_Instr()      => 0x02,
+    E_Breakpoint()         => 0x03,
+    E_Load_Addr_Align()    => 0x04,
+    E_Load_Access_Fault()  => 0x05,
+    E_SAMO_Addr_Align()    => 0x06,
+    E_SAMO_Access_Fault()  => 0x07,
+    E_U_EnvCall()          => 0x08,
+    E_S_EnvCall()          => 0x09,
+    E_Reserved_10()        => 0x0a,
+    E_M_EnvCall()          => 0x0b,
+    E_Fetch_Page_Fault()   => 0x0c,
+    E_Load_Page_Fault()    => 0x0d,
+    E_Reserved_14()        => 0x0e,
+    E_SAMO_Page_Fault()    => 0x0f,
 
     /* extensions */
-    E_CHERI              => 0x20    /* FIXME: this is reserved for a future standard */
+    E_Extension(e)         => 0x18    /* First code for a custom extension */
+  }
+
+val num_of_ExceptionType : ExceptionType -> {'n, (0 <= 'n < xlen). int('n)}
+function num_of_ExceptionType(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,
+
+    /* extensions */
+    E_Extension(e)         => 24    /* First code for a custom extension */
+
   }
 
 val exceptionType_to_str : ExceptionType -> string
 function exceptionType_to_str(e) =
   match (e) {
-    E_Fetch_Addr_Align   => "misaligned-fetch",
-    E_Fetch_Access_Fault => "fetch-access-fault",
-    E_Illegal_Instr      => "illegal-instruction",
-    E_Breakpoint         => "breakpoint",
-    E_Load_Addr_Align    => "misaligned-load",
-    E_Load_Access_Fault  => "load-access-fault",
-    E_SAMO_Addr_Align    => "misaliged-store/amo",
-    E_SAMO_Access_Fault  => "store/amo-access-fault",
-    E_U_EnvCall          => "u-call",
-    E_S_EnvCall          => "s-call",
-    E_Reserved_10        => "reserved-0",
-    E_M_EnvCall          => "m-call",
-    E_Fetch_Page_Fault   => "fetch-page-fault",
-    E_Load_Page_Fault    => "load-page-fault",
-    E_Reserved_14        => "reserved-1",
-    E_SAMO_Page_Fault    => "store/amo-page-fault",
+    E_Fetch_Addr_Align()   => "misaligned-fetch",
+    E_Fetch_Access_Fault() => "fetch-access-fault",
+    E_Illegal_Instr()      => "illegal-instruction",
+    E_Breakpoint()         => "breakpoint",
+    E_Load_Addr_Align()    => "misaligned-load",
+    E_Load_Access_Fault()  => "load-access-fault",
+    E_SAMO_Addr_Align()    => "misaliged-store/amo",
+    E_SAMO_Access_Fault()  => "store/amo-access-fault",
+    E_U_EnvCall()          => "u-call",
+    E_S_EnvCall()          => "s-call",
+    E_Reserved_10()        => "reserved-0",
+    E_M_EnvCall()          => "m-call",
+    E_Fetch_Page_Fault()   => "fetch-page-fault",
+    E_Load_Page_Fault()    => "load-page-fault",
+    E_Reserved_14()        => "reserved-1",
+    E_SAMO_Page_Fault()    => "store/amo-page-fault",
 
     /* extensions */
-    E_CHERI              => "CHERI"
+    E_Extension()          => "extension-exception"
   }
 
 overload to_str = {exceptionType_to_str}
diff --git a/model/riscv_types_ext.sail b/model/riscv_types_ext.sail
new file mode 100644
index 0000000..dfb23fe
--- /dev/null
+++ b/model/riscv_types_ext.sail
@@ -0,0 +1,18 @@
+/* No extensions for PTE checks */
+type ext_pte_error = unit
+
+/* No extensions for page-table-walk errors */
+
+type ext_ptw_error = unit
+
+/* No exception extensions */
+
+type ext_exc_type = unit
+
+/* Default translation of PTE checks into PTW errors */
+function ext_ptw_error_of_pte_error (e : ext_pte_error) -> ext_ptw_error =
+  ()
+
+/* Default translation of PTW errors into exception annotations */
+function ext_translate_exception(e : ext_ptw_error) -> ext_exc_type =
+  e
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index fe4ae3e..cd92a2c 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -19,7 +19,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
             ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
             ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr))
             ^ ": invalid pte address"); */
-      PTW_Failure(PTW_Access)
+      PTW_Failure(PTW_Access())
     },
     MemValue(v) => {
       let pte = Mk_SV32_PTE(v);
@@ -34,42 +34,47 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
             ^ " pte=" ^ BitStr(v)); */
       if isInvalidPTE(pbits, ext_pte) then {
 /*      print("walk32: invalid pte"); */
-        PTW_Failure(PTW_Invalid_PTE)
+        PTW_Failure(PTW_Invalid_PTE())
       } else {
         if isPTEPtr(pbits, ext_pte) then {
           if level == 0 then {
             /* last-level PTE contains a pointer instead of a leaf */
 /*          print("walk32: last-level pte contains a ptr"); */
-            PTW_Failure(PTW_Invalid_PTE)
+            PTW_Failure(PTW_Invalid_PTE())
           } else {
             /* walk down the pointer to the next level */
             walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global)
           }
         } else { /* leaf PTE */
-          if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte)) then {
-/*          print("walk32: pte permission check failure"); */
-            PTW_Failure(PTW_No_Permission)
-          } else {
-            if level > 0 then { /* superpage */
-              /* fixme hack: to get a mask of appropriate size */
-              let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV32_LEVEL_BITS) - 1;
-              if (pte.PPNi() & mask) != EXTZ(0b0) then {
-                /* misaligned superpage mapping */
-/*              print("walk32: misaligned superpage mapping"); */
-                PTW_Failure(PTW_Misaligned)
+          match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte) {
+            PTE_Check_Failure() => {
+/*            print("walk32: pte permission check failure"); */
+              PTW_Failure(PTW_No_Permission()) },
+            PTE_Check_Ext(e)    => {
+/*            print("walk32: pte extension check failure"); */
+              PTW_Failure(PTW_Ext_Error(ext_ptw_error_of_pte_error(e))) },
+            PTE_Check_Success() => {
+              if level > 0 then { /* superpage */
+                /* fixme hack: to get a mask of appropriate size */
+                let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV32_LEVEL_BITS) - 1;
+                if (pte.PPNi() & mask) != EXTZ(0b0) then {
+                  /* misaligned superpage mapping */
+/*                print("walk32: misaligned superpage mapping"); */
+                  PTW_Failure(PTW_Misaligned())
+                } else {
+                  /* add the appropriate bits of the VPN to the superpage PPN */
+                  let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
+/*                let res = append(ppn, va.PgOfs());
+                  print("walk32: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
+                        ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
+                  PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
+                }
               } else {
-                /* add the appropriate bits of the VPN to the superpage PPN */
-                let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
-/*              let res = append(ppn, va.PgOfs());
-                print("walk32: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
-                      ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
-                PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
+                /* normal leaf PTE */
+/*              let res = append(pte.PPNi(), va.PgOfs());
+                print("walk32: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
+                PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
               }
-            } else {
-              /* normal leaf PTE */
-/*            let res = append(pte.PPNi(), va.PgOfs());
-              print("walk32: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
-              PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
             }
           }
         }
@@ -120,29 +125,31 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
       let  pte = Mk_SV32_PTE(ent.pte);
       let  ext_pte : extPte = zeros(); // no reserved bits for extensions
       let  pteBits = Mk_PTE_Bits(pte.BITS());
-      if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte))
-      then TR_Failure(PTW_No_Permission)
-      else {
-        match update_PTE_Bits(pteBits, ac, ext_pte) {
-          None()      => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
-          Some(pbits, ext) => {
-            if ~ (plat_enable_dirty_update ())
-            then {
-              /* pte needs dirty/accessed update but that is not enabled */
-              TR_Failure(PTW_PTE_Update)
-            } else {
-              /* update PTE entry and TLB */
-              n_pte = update_BITS(pte, pbits.bits());
-	      /* ext is unused since there are no reserved bits for extensions */
-              n_ent : TLB32_Entry = ent;
-              n_ent.pte = n_pte.bits();
-              write_TLB32(idx, n_ent);
-              /* update page table */
-              match mem_write_value(to_phys_addr(EXTZ(ent.pteAddr)), 4, n_pte.bits(), false, false, false) {
-                MemValue(_)     => (),
-                MemException(e) => internal_error("invalid physical address in TLB")
-              };
-              TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
+      match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte) {
+        PTE_Check_Failure() => TR_Failure(PTW_No_Permission()),
+        PTE_Check_Ext(e)    => TR_Failure(PTW_Ext_Error(ext_ptw_error_of_pte_error(e))),
+        PTE_Check_Success() => {
+          match update_PTE_Bits(pteBits, ac, ext_pte) {
+            None()      => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
+            Some(pbits, ext) => {
+              if ~ (plat_enable_dirty_update ())
+              then {
+                /* pte needs dirty/accessed update but that is not enabled */
+                TR_Failure(PTW_PTE_Update())
+              } else {
+                /* update PTE entry and TLB */
+                n_pte = update_BITS(pte, pbits.bits());
+                /* ext is unused since there are no reserved bits for extensions */
+                n_ent : TLB32_Entry = ent;
+                n_ent.pte = n_pte.bits();
+                write_TLB32(idx, n_ent);
+                /* update page table */
+                match mem_write_value(to_phys_addr(EXTZ(ent.pteAddr)), 4, n_pte.bits(), false, false, false) {
+                  MemValue(_)     => (),
+                  MemException(e) => internal_error("invalid physical address in TLB")
+                };
+                TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
+              }
             }
           }
         }
@@ -161,10 +168,10 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
               if ~ (plat_enable_dirty_update ())
               then {
                 /* pte needs dirty/accessed update but that is not enabled */
-                TR_Failure(PTW_PTE_Update)
+                TR_Failure(PTW_PTE_Update())
               } else {
                 w_pte : SV32_PTE = update_BITS(pte, pbits.bits());
-		/* ext is unused since there are no reserved bits for extensions */
+                /* ext is unused since there are no reserved bits for extensions */
                 match mem_write_value(to_phys_addr(pteAddr), 4, w_pte.bits(), false, false, false) {
                   MemValue(_) => {
                     add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
@@ -172,7 +179,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
                   },
                   MemException(e) => {
                     /* pte is not in valid memory */
-                    TR_Failure(PTW_Access)
+                    TR_Failure(PTW_Access())
                   }
                 }
               }
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index 2ae2b4c..ba7ebee 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -13,7 +13,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
             ^ " pt_ofs=" ^ BitStr(pt_ofs)
             ^ " pte_addr=" ^ BitStr(pte_addr)
             ^ ": invalid pte address"); */
-      PTW_Failure(PTW_Access)
+      PTW_Failure(PTW_Access())
     },
     MemValue(v) => {
       let pte = Mk_SV39_PTE(v);
@@ -28,42 +28,47 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
             ^ " pte=" ^ BitStr(v)); */
       if isInvalidPTE(pbits, ext_pte) then {
 /*      print("walk39: invalid pte"); */
-        PTW_Failure(PTW_Invalid_PTE)
+        PTW_Failure(PTW_Invalid_PTE())
       } else {
         if isPTEPtr(pbits, ext_pte) then {
           if level == 0 then {
             /* last-level PTE contains a pointer instead of a leaf */
 /*          print("walk39: last-level pte contains a ptr"); */
-            PTW_Failure(PTW_Invalid_PTE)
+            PTW_Failure(PTW_Invalid_PTE())
           } else {
             /* walk down the pointer to the next level */
             walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global)
           }
         } else { /* leaf PTE */
-          if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte)) then {
-/*          print("walk39: pte permission check failure"); */
-            PTW_Failure(PTW_No_Permission)
-          } else {
-            if level > 0 then { /* superpage */
-              /* fixme hack: to get a mask of appropriate size */
-              let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1;
-              if (pte.PPNi() & mask) != EXTZ(0b0) then {
-                /* misaligned superpage mapping */
-/*              print("walk39: misaligned superpage mapping"); */
-                PTW_Failure(PTW_Misaligned)
+          match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte) {
+	    PTE_Check_Failure() => {
+/*            print("walk39: pte permission check failure"); */
+              PTW_Failure(PTW_No_Permission()) },
+            PTE_Check_Ext(e) => {
+/*            print("walk39: pte extension check failure"); */
+              PTW_Failure(PTW_Ext_Error(ext_ptw_error_of_pte_error(e))) },
+            PTE_Check_Success()  => {
+              if level > 0 then { /* superpage */
+                /* fixme hack: to get a mask of appropriate size */
+                let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1;
+                if (pte.PPNi() & mask) != EXTZ(0b0) then {
+                  /* misaligned superpage mapping */
+/*                print("walk39: misaligned superpage mapping"); */
+                  PTW_Failure(PTW_Misaligned())
+                } else {
+                  /* add the appropriate bits of the VPN to the superpage PPN */
+                  let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
+/*                let res = append(ppn, va.PgOfs());
+                  print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
+                        ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
+                  PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
+                }
               } else {
-                /* add the appropriate bits of the VPN to the superpage PPN */
-                let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
-/*              let res = append(ppn, va.PgOfs());
-                print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
-                      ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
-                PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
+                /* normal leaf PTE */
+/*              let res = append(pte.PPNi(), va.PgOfs());
+                print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
+                PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
               }
-            } else {
-              /* normal leaf PTE */
-/*            let res = append(pte.PPNi(), va.PgOfs());
-              print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
-              PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
             }
           }
         }
@@ -114,29 +119,31 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
       let  pte = Mk_SV39_PTE(ent.pte);
       let  ext_pte = pte.Ext();
       let  pteBits = Mk_PTE_Bits(pte.BITS());
-      if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte))
-      then TR_Failure(PTW_No_Permission)
-      else {
-        match update_PTE_Bits(pteBits, ac, ext_pte) {
-          None()      => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
-          Some(pbits, ext) => {
-            if ~ (plat_enable_dirty_update ())
-            then {
-              /* pte needs dirty/accessed update but that is not enabled */
-              TR_Failure(PTW_PTE_Update)
-            } else {
-              /* update PTE entry and TLB */
-              n_pte = update_BITS(pte, pbits.bits());
-	      n_pte = update_Ext(n_pte, ext);
-              n_ent : TLB39_Entry = ent;
-              n_ent.pte = n_pte.bits();
-              write_TLB39(idx, n_ent);
-              /* update page table */
-              match mem_write_value(EXTZ(ent.pteAddr), 8, n_pte.bits(), false, false, false) {
-                MemValue(_)     => (),
-                MemException(e) => internal_error("invalid physical address in TLB")
-              };
-              TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
+      match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte) {
+        PTE_Check_Failure()  => TR_Failure(PTW_No_Permission()),
+        PTE_Check_Ext(e)     => TR_Failure(PTW_Ext_Error(ext_ptw_error_of_pte_error(e))),
+        PTE_Check_Success()  => {
+          match update_PTE_Bits(pteBits, ac, ext_pte) {
+            None()           => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
+            Some(pbits, ext) => {
+              if ~ (plat_enable_dirty_update ())
+              then {
+                /* pte needs dirty/accessed update but that is not enabled */
+                TR_Failure(PTW_PTE_Update())
+              } else {
+                /* update PTE entry and TLB */
+                n_pte = update_BITS(pte, pbits.bits());
+                n_pte = update_Ext(n_pte, ext);
+                n_ent : TLB39_Entry = ent;
+                n_ent.pte = n_pte.bits();
+                write_TLB39(idx, n_ent);
+                /* update page table */
+                match mem_write_value(EXTZ(ent.pteAddr), 8, n_pte.bits(), false, false, false) {
+                  MemValue(_)     => (),
+                  MemException(e) => internal_error("invalid physical address in TLB")
+                };
+                TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask))
+              }
             }
           }
         }
@@ -155,7 +162,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
               if ~ (plat_enable_dirty_update ())
               then {
                 /* pte needs dirty/accessed update but that is not enabled */
-                TR_Failure(PTW_PTE_Update)
+                TR_Failure(PTW_PTE_Update())
               } else {
                 w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
 		w_pte : SV39_PTE = update_Ext(w_pte, ext);
@@ -166,7 +173,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
                   },
                   MemException(e) => {
                     /* pte is not in valid memory */
-                    TR_Failure(PTW_Access)
+                    TR_Failure(PTW_Access())
                   }
                 }
               }
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index 0fe6545..8fc9cf0 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -13,7 +13,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
             ^ " pt_ofs=" ^ BitStr(pt_ofs)
             ^ " pte_addr=" ^ BitStr(pte_addr)
             ^ ": invalid pte address"); */
-      PTW_Failure(PTW_Access)
+      PTW_Failure(PTW_Access())
     },
     MemValue(v) => {
       let pte = Mk_SV48_PTE(v);
@@ -28,42 +28,47 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
             ^ " pte=" ^ BitStr(v)); */
       if isInvalidPTE(pbits, ext_pte) then {
 /*      print("walk48: invalid pte"); */
-        PTW_Failure(PTW_Invalid_PTE)
+        PTW_Failure(PTW_Invalid_PTE())
       } else {
         if isPTEPtr(pbits, ext_pte) then {
           if level == 0 then {
             /* last-level PTE contains a pointer instead of a leaf */
 /*          print("walk48: last-level pte contains a ptr"); */
-            PTW_Failure(PTW_Invalid_PTE)
+            PTW_Failure(PTW_Invalid_PTE())
           } else {
             /* walk down the pointer to the next level */
             walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global)
           }
         } else { /* leaf PTE */
-          if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte)) then {
-/*          print("walk48: pte permission check failure"); */
-            PTW_Failure(PTW_No_Permission)
-          } else {
-            if level > 0 then { /* superpage */
-              /* fixme hack: to get a mask of appropriate size */
-              let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV48_LEVEL_BITS) - 1;
-              if (pte.PPNi() & mask) != EXTZ(0b0) then {
-                /* misaligned superpage mapping */
-/*              print("walk48: misaligned superpage mapping"); */
-                PTW_Failure(PTW_Misaligned)
+          match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte) {
+            PTE_Check_Failure() => {
+/*            print("walk48: pte permission check failure"); */
+              PTW_Failure(PTW_No_Permission()) },
+            PTE_Check_Ext(e)    => {
+/*            print("walk48: pte extension check failure"); */
+              PTW_Failure(PTW_Ext_Error(ext_ptw_error_of_pte_error(e))) },
+	    PTE_Check_Success() => {
+              if level > 0 then { /* superpage */
+                /* fixme hack: to get a mask of appropriate size */
+                let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV48_LEVEL_BITS) - 1;
+                if (pte.PPNi() & mask) != EXTZ(0b0) then {
+                  /* misaligned superpage mapping */
+/*                print("walk48: misaligned superpage mapping"); */
+                  PTW_Failure(PTW_Misaligned())
+                } else {
+                  /* add the appropriate bits of the VPN to the superpage PPN */
+                  let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
+/*                let res = append(ppn, va.PgOfs());
+                  print("walk48: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
+                        ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
+                  PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
+                }
               } else {
-                /* add the appropriate bits of the VPN to the superpage PPN */
-                let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
-/*              let res = append(ppn, va.PgOfs());
-                print("walk48: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())
-                      ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
-                PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
+                /* normal leaf PTE */
+/*              let res = append(pte.PPNi(), va.PgOfs());
+                print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
+                PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
               }
-            } else {
-              /* normal leaf PTE */
-/*            let res = append(pte.PPNi(), va.PgOfs());
-              print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
-              PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
             }
           }
         }
@@ -120,7 +125,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
           if ~ (plat_enable_dirty_update ())
           then {
             /* pte needs dirty/accessed update but that is not enabled */
-            TR_Failure(PTW_PTE_Update)
+            TR_Failure(PTW_PTE_Update())
           } else {
             w_pte : SV48_PTE = update_BITS(pte, pbits.bits());
 	    w_pte : SV48_PTE = update_Ext(w_pte, ext);
@@ -131,7 +136,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = {
               },
               MemException(e) => {
                 /* pte is not in valid memory */
-                TR_Failure(PTW_Access)
+                TR_Failure(PTW_Access())
               }
             }
           }