diff --git a/Makefile b/Makefile
index c2a0b332f..6e6483320 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ SAIL_VLEN := riscv_vlen.sail
 
 # Instruction sources, depending on target
 SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail
-SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_hints.sail
+SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_hints.sail
 SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_zcf.sail
 SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_zcd.sail
 
@@ -72,10 +72,8 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 # System and platform sources
 SAIL_SYS_SRCS =  riscv_csr_begin.sail       # Start of CSR scattered definitions.
 SAIL_SYS_SRCS += riscv_vext_control.sail    # helpers for the 'V' extension
-SAIL_SYS_SRCS += riscv_next_regs.sail
 SAIL_SYS_SRCS += riscv_sys_exceptions.sail  # default basic helpers for exception handling
 SAIL_SYS_SRCS += riscv_sync_exception.sail  # define the exception structure used in the model
-SAIL_SYS_SRCS += riscv_next_control.sail    # helpers for the 'N' extension
 SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
 SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 
diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 29ff4eed8..c75176971 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -15,16 +15,6 @@ scattered mapping csr_name_map
 // TODO: These csr_name_map definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* user trap setup */
-mapping clause csr_name_map = 0x000  <-> "ustatus"
-mapping clause csr_name_map = 0x004  <-> "uie"
-mapping clause csr_name_map = 0x005  <-> "utvec"
-/* user trap handling */
-mapping clause csr_name_map = 0x040  <-> "uscratch"
-mapping clause csr_name_map = 0x041  <-> "uepc"
-mapping clause csr_name_map = 0x042  <-> "ucause"
-mapping clause csr_name_map = 0x043  <-> "utval"
-mapping clause csr_name_map = 0x044  <-> "uip"
 /* user floating-point context */
 mapping clause csr_name_map = 0x001  <-> "fflags"
 mapping clause csr_name_map = 0x002  <-> "frm"
@@ -100,8 +90,6 @@ mapping clause csr_name_map = 0xC9F  <-> "hpmcounter31h"
 
 /* supervisor trap setup */
 mapping clause csr_name_map = 0x100  <-> "sstatus"
-mapping clause csr_name_map = 0x102  <-> "sedeleg"
-mapping clause csr_name_map = 0x103  <-> "sideleg"
 mapping clause csr_name_map = 0x104  <-> "sie"
 mapping clause csr_name_map = 0x105  <-> "stvec"
 mapping clause csr_name_map = 0x106  <-> "scounteren"
diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail
deleted file mode 100644
index 52d8bc26d..000000000
--- a/model/riscv_insts_next.sail
+++ /dev/null
@@ -1,26 +0,0 @@
-/*=======================================================================================*/
-/*  This Sail RISC-V architecture model, comprising all files and                        */
-/*  directories except where otherwise noted is subject the BSD                          */
-/*  two-clause license in the LICENSE file.                                              */
-/*                                                                                       */
-/*  SPDX-License-Identifier: BSD-2-Clause                                                */
-/*=======================================================================================*/
-
-/* *****************************************************************/
-/* This file specifies the instruction added by the 'N' extension. */
-
-union clause ast = URET : unit
-
-mapping clause encdec = URET()
-  <-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
-
-function clause execute URET() = {
-  if   not(extensionEnabled(Ext_U)) | not(sys_enable_next())
-  then handle_illegal()
-  else if not(ext_check_xret_priv(User))
-  then ext_fail_xret_priv()
-  else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC));
-  RETIRE_FAIL
-}
-
-mapping clause assembly = URET() <-> "uret"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 8e8c0dce2..5e4d47b9e 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -74,8 +74,6 @@ function clause read_CSR(0x7a0) = ~(tselect)  /* this indicates we don't have an
 
 /* supervisor mode */
 function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
-function clause read_CSR(0x102) = sedeleg.bits
-function clause read_CSR(0x103) = sideleg.bits
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
 function clause read_CSR(0x105) = get_stvec()
 function clause read_CSR(0x106) = zero_extend(scounteren.bits)
@@ -162,8 +160,6 @@ function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
 
 /* supervisor mode */
 function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
-function clause write_CSR(0x102, value) = { sedeleg = legalize_sedeleg(sedeleg, value); sedeleg.bits }
-function clause write_CSR(0x103, value) = { sideleg.bits = value; sideleg.bits } /* TODO: does this need legalization? */
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
 function clause write_CSR(0x105, value) = { set_stvec(value) }
 function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) }
diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail
deleted file mode 100644
index aa10bad98..000000000
--- a/model/riscv_next_control.sail
+++ /dev/null
@@ -1,40 +0,0 @@
-/*=======================================================================================*/
-/*  This Sail RISC-V architecture model, comprising all files and                        */
-/*  directories except where otherwise noted is subject the BSD                          */
-/*  two-clause license in the LICENSE file.                                              */
-/*                                                                                       */
-/*  SPDX-License-Identifier: BSD-2-Clause                                                */
-/*=======================================================================================*/
-
-/* Functional specification for the 'N' user-level interrupts standard extension. */
-
-function clause is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus
-function clause is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie
-function clause is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec
-function clause is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch
-function clause is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc
-function clause is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause
-function clause is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval
-function clause is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uip
-
-function clause read_CSR(0x000) = lower_sstatus(lower_mstatus(mstatus)).bits
-function clause read_CSR(0x004) = lower_sie(lower_mie(mie, mideleg), sideleg).bits
-function clause read_CSR(0x005) = get_utvec()
-function clause read_CSR(0x040) = uscratch
-function clause read_CSR(0x041) = get_xret_target(User) & pc_alignment_mask()
-function clause read_CSR(0x042) = ucause.bits
-function clause read_CSR(0x043) = utval
-function clause read_CSR(0x044) = lower_sip(lower_mip(mip, mideleg), sideleg).bits
-
-function clause write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); mstatus.bits }
-function clause write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value);
-                                                 mie = lift_sie(mie, mideleg, sie);
-                                                 mie.bits }
-function clause write_CSR(0x005, value) = { set_utvec(value) }
-function clause write_CSR(0x040, value) = { uscratch = value; uscratch }
-function clause write_CSR(0x041, value) = { set_xret_target(User, value) }
-function clause write_CSR(0x042, value) = { ucause.bits = value; ucause.bits }
-function clause write_CSR(0x043, value) = { utval = value; utval }
-function clause write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value);
-                                                 mip = lift_sip(mip, mideleg, sip);
-                                                 mip.bits }
diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail
deleted file mode 100644
index 64c9f77c2..000000000
--- a/model/riscv_next_regs.sail
+++ /dev/null
@@ -1,96 +0,0 @@
-/*=======================================================================================*/
-/*  This Sail RISC-V architecture model, comprising all files and                        */
-/*  directories except where otherwise noted is subject the BSD                          */
-/*  two-clause license in the LICENSE file.                                              */
-/*                                                                                       */
-/*  SPDX-License-Identifier: BSD-2-Clause                                                */
-/*=======================================================================================*/
-
-/* Architectural state for the 'N' user-level interrupts standard extension. */
-
-/* ustatus reveals a subset of mstatus */
-bitfield Ustatus : xlenbits = {
-  UPIE : 4,
-  UIE  : 0
-}
-
-/* This is a view, so there is no register defined. */
-function lower_sstatus(s : Sstatus) -> Ustatus = {
-  let u = Mk_Ustatus(zero_extend(0b0));
-
-  [u with
-    UPIE = s[UPIE],
-    UIE = s[UIE],
-  ]
-}
-
-function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = {
-  [s with
-    UPIE = u[UPIE],
-    UIE = u[UIE],
-  ]
-}
-
-function legalize_ustatus(m : Mstatus, v : xlenbits) -> Mstatus = {
-  let u = Mk_Ustatus(v);
-  let s = lower_mstatus(m);     // lower current mstatus to sstatus
-  let s = lift_ustatus(s, u);   // get updated sstatus
-  let m = lift_sstatus(m, s);   // lift it to an updated mstatus
-  m
-}
-
-bitfield Uinterrupts : xlenbits = {
-  UEI : 8,  /* external interrupt */
-  UTI : 4,  /* timer interrupt    */
-  USI : 0   /* software interrupt */
-}
-
-/* Provides the uip read view of sip (s) as delegated by sideleg (d). */
-function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
-  let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0));
-  [u with
-    UEI = s[UEI] & d[UEI],
-    UTI = s[UTI] & d[UTI],
-    USI = s[USI] & d[USI],
-  ]
-}
-
-/* Provides the uie read view of sie as delegated by sideleg. */
-function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
-  let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0));
-  [u with
-    UEI = s[UEI] & d[UEI],
-    UTI = s[UTI] & d[UTI],
-    USI = s[USI] & d[USI],
-  ]
-}
-
-/* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */
-function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
-  let s : Sinterrupts = o;
-  let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s;
-  s
-}
-
-function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterrupts = {
-  lift_uip(s, d, Mk_Uinterrupts(v))
-}
-
-/* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */
-function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
-  let s : Sinterrupts = o;
-  let s = if d[UEI] == 0b1 then [s with UEI = u[UEI]] else s;
-  let s = if d[UTI] == 0b1 then [s with UTI = u[UTI]] else s;
-  let s = if d[USI] == 0b1 then [s with USI = u[USI]] else s;
-  s
-}
-
-function legalize_uie(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterrupts = {
-  lift_uie(s, d, Mk_Uinterrupts(v))
-}
-
-register utvec    : Mtvec
-register uscratch : xlenbits
-register uepc     : xlenbits
-register ucause   : Mcause
-register utval    : xlenbits
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 80e6ea5c7..f408c0942 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -28,8 +28,8 @@ function clause is_CSR_defined(0xf15) = true // mconfigptr
 /* machine mode: trap setup */
 function clause is_CSR_defined(0x300) = true // mstatus
 function clause is_CSR_defined(0x301) = true // misa
-function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // medeleg
-function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // mideleg
+function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) // medeleg
+function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) // mideleg
 function clause is_CSR_defined(0x304) = true // mie
 function clause is_CSR_defined(0x305) = true // mtvec
 function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren
@@ -73,8 +73,6 @@ function clause is_CSR_defined(0x7a0) = true
 
 /* supervisor mode: trap setup */
 function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
-function clause is_CSR_defined(0x102) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sedeleg
-function clause is_CSR_defined(0x103) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sideleg
 function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
 function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
 function clause is_CSR_defined(0x106) = extensionEnabled(Ext_S) // scounteren
@@ -183,13 +181,7 @@ val cancel_reservation = impure {interpreter: "Platform.cancel_reservation", c:
 function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
   let idx   = num_of_ExceptionType(e);
   let super = bit_to_bool(medeleg.bits[idx]);
-  /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */
-  let user  = if   extensionEnabled(Ext_S)
-              then super & extensionEnabled(Ext_N) & bit_to_bool(sedeleg.bits[idx])
-              else super & extensionEnabled(Ext_N);
-  let deleg = if      extensionEnabled(Ext_U) & user  then User
-              else if extensionEnabled(Ext_S) & super then Supervisor
-              else                               Machine;
+  let deleg = if extensionEnabled(Ext_S) & super then Supervisor else Machine;
   /* We cannot transition to a less-privileged mode. */
   if   privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
   then p else deleg
@@ -206,10 +198,7 @@ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
   else if ip[SEI] == 0b1 then Some(I_S_External)
   else if ip[SSI] == 0b1 then Some(I_S_Software)
   else if ip[STI] == 0b1 then Some(I_S_Timer)
-  else if ip[UEI] == 0b1 then Some(I_U_External)
-  else if ip[USI] == 0b1 then Some(I_U_Software)
-  else if ip[UTI] == 0b1 then Some(I_U_Timer)
-  else                         None()
+  else                        None()
 }
 
 /* Process the pending interrupts xip at a privilege according to
@@ -225,28 +214,26 @@ union interrupt_set = {
 function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits,
                         priv_enabled : bool) -> interrupt_set = {
   /* interrupts that are enabled but not delegated are pending */
-  let  effective_pend = xip.bits & xie.bits & (~ (xideleg));
+  let  effective_pend = xip.bits & xie.bits & ~(xideleg);
   /* the others are delegated */
   let  effective_delg = xip.bits & xideleg;
   /* we have pending interrupts if this privilege is enabled */
-  if      priv_enabled & (effective_pend != zero_extend(0b0))
+  if      priv_enabled & (effective_pend != zeros())
   then    Ints_Pending(effective_pend)
-  else if effective_delg != zero_extend(0b0)
+  else if effective_delg != zeros()
   then    Ints_Delegated(effective_delg)
   else    Ints_Empty()
 }
 
 /* Given the current privilege level, iterate over privileges to get a
- * pending set for an enabled privilege. This is only called for M/U or
- * M/S/U systems.
+ * pending set for an enabled privilege.
  *
  * We don't use the lowered views of {xie,xip} here, since the spec
- * allows for example the M_Timer to be delegated to the U-mode.
+ * allows for example the M_Timer to be delegated to the S-mode.
  */
 function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
-  assert(extensionEnabled(Ext_U), "no user mode: M/U or M/S/U system required");
   let effective_pending = mip.bits & mie.bits;
-  if  effective_pending == zero_extend(0b0) then None() /* fast path */
+  if  effective_pending == zeros() then None() /* fast path */
   else {
     /* Higher privileges than the current one are implicitly enabled,
      * while lower privileges are blocked.  An unsupported privilege is
@@ -254,24 +241,10 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
      */
     let mIE = priv != Machine | (priv == Machine & mstatus[MIE] == 0b1);
     let sIE = extensionEnabled(Ext_S) & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1));
-    let uIE = extensionEnabled(Ext_N) & (priv == User & mstatus[UIE] == 0b1);
     match processPending(mip, mie, mideleg.bits, mIE) {
       Ints_Empty()      => None(),
-      Ints_Pending(p)   => let r = (p, Machine) in Some(r),
-      Ints_Delegated(d) =>
-        if not(extensionEnabled(Ext_S)) then {
-          if uIE then let r = (d, User) in Some(r)
-          else                             None()
-        } else {
-          /* the delegated bits are pending for S-mode */
-          match processPending(Mk_Minterrupts(d), mie, sideleg.bits, sIE) {
-            Ints_Empty()      => None(),
-            Ints_Pending(p)   => let r = (p, Supervisor) in Some(r),
-            Ints_Delegated(d) => if   uIE
-                                 then let r = (d, User) in Some(r)
-                                 else None()
-          }
-        }
+      Ints_Pending(p)   => Some((p, Machine)),
+      Ints_Delegated(d) => if sIE then Some((d, Supervisor)) else None(),
     }
   }
 }
@@ -280,32 +253,12 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
  * handled (if any), and the privilege it should be handled at.
  */
 function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege)) = {
-  /* If we don't have different privilege levels, we don't need to check delegation.
-   * Absence of U-mode implies absence of S-mode.
-   */
-  let multipleModesSupported = extensionEnabled(Ext_U);
-  if not(multipleModesSupported) then {
-    assert(priv == Machine, "invalid current privilege")
-  };
-  /* Even with U-mode, we don't need to check delegation when M-mode is the only
-     one that can take interrupts, i.e. when we don't have S-mode and don't have
-     the N extension
-  */
-  let delegationPossible = extensionEnabled(Ext_S) | extensionEnabled(Ext_N);
-  if multipleModesSupported & delegationPossible then {
-    match getPendingSet(priv) {
-      None()      => None(),
-      Some(ip, p) => match findPendingInterrupt(ip) {
-                       None()  => None(),
-                       Some(i) => let r = (i, p) in Some(r)
-                     }
-    }
-  } else {
-    let enabled_pending = mip.bits & mie.bits;
-    match findPendingInterrupt(enabled_pending) {
-      Some(i) => let r = (i, Machine) in Some(r),
-      None()  => None()
-    }
+  match getPendingSet(priv) {
+    None()       => None(),
+    Some(ip, p)  => match findPendingInterrupt(ip) {
+                      None()  => None(),
+                      Some(i) => Some((i, p)),
+                    }
   }
 }
 
@@ -315,7 +268,6 @@ union ctl_result = {
   CTL_TRAP : sync_exception,
   CTL_SRET : unit,
   CTL_MRET : unit,
-  CTL_URET : unit
 }
 
 /* trap value */
@@ -392,26 +344,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
        prepare_trap_vector(del_priv, scause)
     },
-    User => {
-       assert(extensionEnabled(Ext_U), "no user mode present for delegation");
-
-       ucause[IsInterrupt] = bool_to_bits(intr);
-       ucause[Cause]       = zero_extend(c);
-
-       mstatus[UPIE] = mstatus[UIE];
-       mstatus[UIE]  = 0b0;
-       utval           = tval(info);
-       uepc            = pc;
-
-       cur_privilege   = del_priv;
-
-       handle_trap_extension(del_priv, pc, ext);
-
-       if   get_config_print_reg()
-       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
-
-       prepare_trap_vector(del_priv, ucause)
-    }
+    User => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
   };
 }
 
@@ -458,19 +391,6 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
 
       prepare_xret_target(Supervisor) & pc_alignment_mask()
     },
-    (_, CTL_URET())  => {
-      let prev_priv   = cur_privilege;
-      mstatus[UIE]  = mstatus[UPIE];
-      mstatus[UPIE] = 0b1;
-      cur_privilege   = User;
-
-      if   get_config_print_reg()
-      then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits));
-      if   get_config_print_platform()
-      then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
-
-      prepare_xret_target(User) & pc_alignment_mask()
-    }
   }
 }
 
diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail
index 0059e2a7f..4e4b550ad 100644
--- a/model/riscv_sys_exceptions.sail
+++ b/model/riscv_sys_exceptions.sail
@@ -22,7 +22,7 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
   let tvec : Mtvec = match p {
                        Machine    => mtvec,
                        Supervisor => stvec,
-                       User       => utvec
+                       User       => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
                      };
   match tvec_addr(tvec, cause) {
     Some(epc) => epc,
@@ -42,7 +42,7 @@ function get_xret_target(p) =
   match p {
     Machine    => mepc,
     Supervisor => sepc,
-    User       => uepc
+    User       => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
   }
 
 val set_xret_target : (Privilege, xlenbits) -> xlenbits
@@ -51,7 +51,7 @@ function set_xret_target(p, value) = {
   match p {
     Machine    => mepc = target,
     Supervisor => sepc = target,
-    User       => uepc = target
+    User       => internal_error(__FILE__, __LINE__, "Invalid privilege level"),
   };
   target
 }
@@ -68,9 +68,6 @@ function get_mtvec() -> xlenbits =
 function get_stvec() -> xlenbits =
   stvec.bits
 
-function get_utvec() -> xlenbits =
-  utvec.bits
-
 function set_mtvec(value : xlenbits) -> xlenbits = {
   mtvec = legalize_tvec(mtvec, value);
   mtvec.bits
@@ -80,8 +77,3 @@ function set_stvec(value : xlenbits) -> xlenbits = {
   stvec = legalize_tvec(stvec, value);
   stvec.bits
 }
-
-function set_utvec(value : xlenbits) -> xlenbits = {
-  utvec = legalize_tvec(utvec, value);
-  utvec.bits
-}
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 2a5a219c8..787b77fd9 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -136,9 +136,6 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
   }
 }
 
-enum clause extension = Ext_N
-function clause extensionEnabled(Ext_N) = misa[N] == 0b1
-
 enum clause extension = Ext_U
 function clause extensionEnabled(Ext_U) = misa[U] == 0b1
 
@@ -200,11 +197,9 @@ bitfield Mstatus : xlenbits = {
 
   MPIE : 7,
   SPIE : 5,
-  UPIE : 4,
 
   MIE  : 3,
   SIE  : 1,
-  UIE  : 0
 }
 register mstatus : Mstatus
 
@@ -277,11 +272,6 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
              Mk_Mstatus([m.bits with 37 .. 36 = 0b00])
           } else m;
 
-  /* Hardwired to zero in the absence of 'U' or 'N'. */
-  let m = if not(extensionEnabled(Ext_N)) then {
-             [m with UPIE = 0b0, UIE = 0b0]
-          } else m;
-
   if not(extensionEnabled(Ext_U)) then {
     let m = [m with MPRV = 0b0];
     m
@@ -312,15 +302,12 @@ function in32BitMode() -> bool = {
 bitfield Minterrupts : xlenbits = {
   MEI : 11, /* external interrupts */
   SEI : 9,
-  UEI : 8,
 
   MTI : 7,  /* timers interrupts */
   STI : 5,
-  UTI : 4,
 
   MSI : 3,  /* software interrupts */
   SSI : 1,
-  USI : 0,
 }
 register mip     : Minterrupts /* Pending */
 register mie     : Minterrupts /* Enabled */
@@ -330,26 +317,19 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = {
   /* The only writable bits are the S-mode bits, and with the 'N'
    * extension, the U-mode bits. */
   let v = Mk_Minterrupts(v);
-  let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]];
-  if extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then {
-    [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]]
-  } else m
+  [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]
 }
 
 function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = {
   let v = Mk_Minterrupts(v);
-  let m = [o with
+  [o with
     MEI = v[MEI],
     MTI = v[MTI],
     MSI = v[MSI],
     SEI = v[SEI],
     STI = v[STI],
     SSI = v[SSI]
-  ];
-  /* The U-mode bits will be modified if we have the 'N' extension. */
-  if extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then {
-    [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]]
-  } else m
+  ]
 }
 
 function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = {
@@ -554,9 +534,7 @@ bitfield Sstatus : xlenbits = {
   VS   : 10 .. 9,
   SPP  : 8,
   SPIE : 5,
-  UPIE : 4,
   SIE  : 1,
-  UIE  : 0
 }
 /* sstatus is a view of mstatus, so there is no register defined. */
 
@@ -584,9 +562,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
     VS = m[VS],
     SPP = m[SPP],
     SPIE = m[SPIE],
-    UPIE = m[UPIE],
     SIE = m[SIE],
-    UIE = m[UIE],
   ]
 }
 
@@ -603,9 +579,7 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
     VS = s[VS],
     SPP = s[SPP],
     SPIE = s[SPIE],
-    UPIE = s[UPIE],
     SIE = s[SIE],
-    UIE = s[UIE],
   ]
 }
 
@@ -613,32 +587,14 @@ function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = {
   legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits)
 }
 
-bitfield Sedeleg : xlenbits = {
-  UEnvCall          : 8,
-  SAMO_Access_Fault : 7,
-  SAMO_Addr_Align   : 6,
-  Load_Access_Fault : 5,
-  Load_Addr_Align   : 4,
-  Breakpoint        : 3,
-  Illegal_Instr     : 2,
-  Fetch_Access_Fault: 1,
-  Fetch_Addr_Align  : 0
-}
-register sedeleg : Sedeleg
 
-function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = {
-  Mk_Sedeleg(zero_extend(v[8..0]))
-}
 
 bitfield Sinterrupts : xlenbits = {
   SEI : 9,  /* external interrupts */
-  UEI : 8,
 
   STI : 5,  /* timers interrupts */
-  UTI : 4,
 
   SSI : 1,  /* software interrupts */
-  USI : 0
 }
 
 /* Provides the sip read view of mip (m) as delegated by mideleg (d). */
@@ -649,9 +605,6 @@ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
     SEI = m[SEI] & d[SEI],
     STI = m[STI] & d[STI],
     SSI = m[SSI] & d[SSI],
-    UEI = m[UEI] & d[UEI],
-    UTI = m[UTI] & d[UTI],
-    USI = m[USI] & d[USI],
   ]
 }
 
@@ -663,9 +616,6 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
     SEI = m[SEI] & d[SEI],
     STI = m[STI] & d[STI],
     SSI = m[SSI] & d[SSI],
-    UEI = m[UEI] & d[UEI],
-    UTI = m[UTI] & d[UTI],
-    USI = m[USI] & d[USI],
   ]
 }
 
@@ -673,11 +623,7 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
 function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
   let m : Minterrupts = o;
   let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m;
-  if extensionEnabled(Ext_N) then {
-    let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m;
-    let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m;
-    m
-  } else m
+  m
 }
 
 function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
@@ -690,19 +636,13 @@ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru
   let m = if d[SEI] == 0b1 then [m with SEI = s[SEI]] else m;
   let m = if d[STI] == 0b1 then [m with STI = s[STI]] else m;
   let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m;
-  if extensionEnabled(Ext_N) then {
-    let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m;
-    let m = if d[UTI] == 0b1 then [m with UTI = s[UTI]] else m;
-    let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m;
-    m
-  } else m
+  m
 }
 
 function legalize_sie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
   lift_sie(m, d, Mk_Sinterrupts(v))
 }
 
-register sideleg : Sinterrupts
 
 /* other non-VM related supervisor state */
 register stvec    : Mtvec