diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h
index da29c2ba9..d184c1225 100644
--- a/c_emulator/riscv_sail.h
+++ b/c_emulator/riscv_sail.h
@@ -24,7 +24,6 @@ unit z_set_Misa_D(struct zMisa *, mach_bits);
 unit z_set_Misa_F(struct zMisa *, mach_bits);
 
 #ifdef RVFI_DII
-unit zext_rvfi_init(unit);
 unit zrvfi_set_instr_packet(mach_bits);
 mach_bits zrvfi_get_cmd(unit);
 mach_bits zrvfi_get_insn(unit);
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index 8ffe60026..25028330d 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -658,17 +658,11 @@ void init_sail_reset_vector(uint64_t entry)
   zPC = rv_rom_base;
 }
 
-void preinit_sail()
-{
-  model_init();
-}
-
 void init_sail(uint64_t elf_entry)
 {
   zinit_model(UNIT);
 #ifdef RVFI_DII
   if (rvfi_dii) {
-    zext_rvfi_init(UNIT);
     rv_ram_base = UINT64_C(0x80000000);
     rv_ram_size = UINT64_C(0x800000);
     rv_rom_base = UINT64_C(0);
@@ -1142,8 +1136,7 @@ void init_logs()
 
 int main(int argc, char **argv)
 {
-  // Initialize model so that we can check or report its architecture.
-  preinit_sail();
+  model_init();
 
   int files_start = process_args(argc, argv);
   char *initial_elf_file = argv[files_start];
diff --git a/model/main.sail b/model/main.sail
index 9e0357c29..e6e121f05 100644
--- a/model/main.sail
+++ b/model/main.sail
@@ -24,9 +24,6 @@ function get_entry_point() = zero_extend(0x1000)
 $endif
 
 function main() : unit -> unit = {
-  // initialize extensions
-  ext_init();
-
   PC = get_entry_point();
   print_bits("PC = ", PC);
 
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index efe9bae70..c699d9633 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -10,20 +10,6 @@
  * overridden by extensions.
  */
 
-val ext_init_regs : unit -> unit
-function ext_init_regs () = ()
-
-/*!
-This function is called after above when running rvfi and allows the model
-to be initialised differently (e.g. CHERI cap regs are initialised
-to omnipotent instead of null).
- */
-val ext_rvfi_init : unit -> unit
-function ext_rvfi_init () = {
-  x1 = x1 // to avoid hook being optimized out
-}
-
-
 /*!
 THIS(csrno, priv, isWrite) allows an extension to block access to csrno,
 at Privilege level priv. It should return true if the access is allowed.
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index 58f7c3758..2dc97811d 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -353,42 +353,6 @@ mapping freg_or_reg_name = {
   reg if sys_enable_zfinx() <-> reg_name(reg)  if sys_enable_zfinx()
 }
 
-val init_fdext_regs : unit -> unit
-function init_fdext_regs () = {
-  f0  = zero_freg;
-  f1  = zero_freg;
-  f2  = zero_freg;
-  f3  = zero_freg;
-  f4  = zero_freg;
-  f5  = zero_freg;
-  f6  = zero_freg;
-  f7  = zero_freg;
-  f8  = zero_freg;
-  f9  = zero_freg;
-  f10 = zero_freg;
-  f11 = zero_freg;
-  f12 = zero_freg;
-  f13 = zero_freg;
-  f14 = zero_freg;
-  f15 = zero_freg;
-  f16 = zero_freg;
-  f17 = zero_freg;
-  f18 = zero_freg;
-  f19 = zero_freg;
-  f20 = zero_freg;
-  f21 = zero_freg;
-  f22 = zero_freg;
-  f23 = zero_freg;
-  f24 = zero_freg;
-  f25 = zero_freg;
-  f26 = zero_freg;
-  f27 = zero_freg;
-  f28 = zero_freg;
-  f29 = zero_freg;
-  f30 = zero_freg;
-  f31 = zero_freg
-}
-
 /* **************************************************************** */
 /* Floating Point CSR                                               */
 /*     fflags    address 0x001    same as fcrs [4..0]               */
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index c662da2d6..59ed270ec 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -126,7 +126,7 @@ function pmpCheck forall 'n, 'n > 0. (addr: physaddr, width: int('n), acc: Acces
   if priv == Machine then None() else Some(accessToFault(acc))
 }
 
-function init_pmp() -> unit = {
+function reset_pmp() -> unit = {
   assert(
     sys_pmp_count() == 0 | sys_pmp_count() == 16 | sys_pmp_count() == 64,
     "sys_pmp_count() must be 0, 16, or 64"
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index 26faef210..d8b21d716 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -198,38 +198,3 @@ mapping creg_name : cregidx <-> string = {
   0b110 <-> "a4",
   0b111 <-> "a5"
 }
-
-val init_base_regs : unit -> unit
-function init_base_regs () = {
-  x1  = zero_reg;
-  x2  = zero_reg;
-  x3  = zero_reg;
-  x4  = zero_reg;
-  x5  = zero_reg;
-  x6  = zero_reg;
-  x7  = zero_reg;
-  x8  = zero_reg;
-  x9  = zero_reg;
-  x10 = zero_reg;
-  x11 = zero_reg;
-  x12 = zero_reg;
-  x13 = zero_reg;
-  x14 = zero_reg;
-  x15 = zero_reg;
-  x16 = zero_reg;
-  x17 = zero_reg;
-  x18 = zero_reg;
-  x19 = zero_reg;
-  x20 = zero_reg;
-  x21 = zero_reg;
-  x22 = zero_reg;
-  x23 = zero_reg;
-  x24 = zero_reg;
-  x25 = zero_reg;
-  x26 = zero_reg;
-  x27 = zero_reg;
-  x28 = zero_reg;
-  x29 = zero_reg;
-  x30 = zero_reg;
-  x31 = zero_reg
-}
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 9f8e919cc..62c770675 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -123,13 +123,14 @@ function loop () : unit -> unit = {
   }
 }
 
-/* initialize model state */
-function init_model () -> unit = {
-  init_platform (); /* devices */
-  init_sys ();      /* processor */
-  init_vmem ();     /* virtual memory */
+// Chip reset. This only does the minimum resets required by the RISC-V spec.
+function reset() -> unit = {
+  reset_sys();
+  reset_vmem();
+}
 
-  /* initialize extensions last */
-  ext_init ();
-  ext_init_regs ();
+// Initialize model state. This is only called once; not for every chip reset.
+function init_model() -> unit = {
+  init_platform();
+  reset();
 }
diff --git a/model/riscv_step_ext.sail b/model/riscv_step_ext.sail
index b8c82b742..ee16ec383 100644
--- a/model/riscv_step_ext.sail
+++ b/model/riscv_step_ext.sail
@@ -8,8 +8,6 @@
 
 /* The default implementation of hooks for the step() and main() functions. */
 
-function ext_init() -> unit = ()
-
 function ext_fetch_hook(f : FetchResult) -> FetchResult = f
 
 function ext_pre_step_hook()  -> unit = ()
diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail
index 53ebb1595..2cc1db90b 100644
--- a/model/riscv_step_rvfi.sail
+++ b/model/riscv_step_rvfi.sail
@@ -16,13 +16,3 @@ function ext_post_step_hook() -> unit = {
   /* record the next pc */
   rvfi_pc_data[rvfi_pc_wdata] = zero_extend(get_arch_pc())
 }
-
-val ext_init : unit -> unit
-function ext_init() = {
-  init_base_regs();
-  init_fdext_regs();
-  /* these are here so that the C backend doesn't prune them out. */
-  // let _ = rvfi_step(0);
-  ext_rvfi_init();
-  ()
-}
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 28731f6be..4eeff04fd 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -343,15 +343,8 @@ function handle_exception(e: ExceptionType) -> unit = {
 function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
   set_next_pc(trap_handler(del_priv, true, interruptType_to_bits(i), PC, None(), None()))
 
-/* state state initialization */
-
-function init_sys() -> unit = {
-  cur_privilege = Machine;
-
-  mhartid     = zeros();
-  mconfigptr  = zeros();
-
-  misa[MXL] = arch_to_bits(if xlen == 32 then RV32 else RV64);
+// Reset misa to enable the maximal set of supported extensions.
+function reset_misa() -> unit = {
   misa[A]   = 0b1;                             /* atomics */
   misa[C]   = bool_to_bits(sys_enable_rvc());  /* RVC */
   misa[B]   = bool_to_bits(sys_enable_bext()); /* Bit-manipulation */
@@ -367,40 +360,47 @@ function init_sys() -> unit = {
   /* We currently support both F and D */
   misa[F]   = bool_to_bits(sys_enable_fdext());      /* single-precision */
   misa[D]   = if   flen >= 64
-                then bool_to_bits(sys_enable_fdext())  /* double-precision */
-                else 0b0;
+              then bool_to_bits(sys_enable_fdext())  /* double-precision */
+              else 0b0;
+}
 
-  mstatus = set_mstatus_SXL(mstatus, misa[MXL]);
-  mstatus = set_mstatus_UXL(mstatus, misa[MXL]);
-  mstatus[SD]   = 0b0;
-  mstatus[MPP] = privLevel_to_bits(lowest_supported_privLevel());
+// This function is called on reset, so it should only perform the reset actions
+// described in the "Reset" section of the privileged architecture specification.
+function reset_sys() -> unit = {
 
-  /* set to little-endian mode */
-  if xlen == 64 then {
-    mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00])
-  };
-  mstatush.bits = zeros();
+  // "Upon reset, a hart's privilege mode is set to M."
+  cur_privilege = Machine;
+
+  // "The mstatus fields MIE and MPRV are reset to 0."
+  mstatus[MIE] = 0b0;
+  mstatus[MPRV] = 0b0;
+
+  // "If little-endian memory accesses are supported, the mstatus/mstatush field
+  // MBE is reset to 0."
+  // The model doesn't support little-endian (see legalize_mstatus()).
 
-  mip.bits     = zeros();
-  mie.bits     = zeros();
-  mideleg.bits = zeros();
-  medeleg.bits = zeros();
-  mtvec.bits   = zeros();
-  mcause.bits  = zeros();
-  mepc            = zeros();
-  mtval           = zeros();
-  mscratch        = zeros();
+  // "The misa register is reset to enable the maximal set of supported extensions"
+  reset_misa();
 
-  mcycle          = zeros();
-  mtime           = zeros();
+  // "For implementations with the "A" standard extension, there is no valid load reservation."
+  cancel_reservation();
 
-  mcounteren.bits = zeros();
+  // "The pc is set to an implementation-defined reset vector."
+  // This is outside the scope of this function.
 
-  minstret           = zeros();
-  minstret_increment = true;
+  // "The mcause register is set to a value indicating the cause of the reset."
+  // "The mcause values after reset have implementation-specific interpretation,
+  // but the value 0 should be returned on implementations that do not
+  // distinguish different reset conditions."
+  mcause.bits = zeros();
+
+  // "Writable PMP registers’ A and L fields are set to 0, unless the platform
+  // mandates a different reset value for some PMP registers’ A and L fields."
+  reset_pmp();
+
+  // TODO: Probably need to remove these vector resets too but it needs
+  // refactoring anyway. See https://github.com/riscv/sail-riscv/issues/566 etc.
 
-  menvcfg.bits = zeros();
-  senvcfg.bits = zeros();
   /* initialize vector csrs */
   vstart             = zeros();
   vl                 = zeros();
@@ -413,9 +413,6 @@ function init_sys() -> unit = {
   vtype[vsew]      = 0b000;
   vtype[vlmul]     = 0b000;
 
-  // PMP's L and A fields are set to 0 on reset.
-  init_pmp();
-
   // log compatibility with spike
   if   get_config_print_reg()
   then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zeros() : xlenbits) ^ ")")
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index b4fadd26b..8b9a96724 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -76,7 +76,11 @@ bitfield Misa : xlenbits = {
   B    : 1,
   A    : 0
 }
-register misa : Misa
+register misa : Misa =
+  [ Mk_Misa(zeros()) with
+    // MXL is a read-only field that specifies the native XLEN.
+    MXL = arch_to_bits(if xlen == 32 then RV32 else RV64),
+  ]
 
 /* whether misa is R/W */
 val sys_enable_writable_misa = pure "sys_enable_writable_misa" : unit -> bool
@@ -207,42 +211,31 @@ bitfield Mstatus : xlenbits = {
   MIE  : 3,
   SIE  : 1,
 }
-register mstatus : Mstatus
 
 function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : Privilege) -> Privilege =
   if   t != Execute() & m[MPRV] == 0b1
   then privLevel_of_bits(m[MPP])
   else priv
 
-function get_mstatus_SXL(m : Mstatus) -> arch_xlen = {
+function get_mstatus_SXL(m : Mstatus) -> arch_xlen =
   if   xlen == 32
   then arch_to_bits(RV32)
   else m.bits[35 .. 34]
-}
 
-function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
+function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus =
   if   xlen == 32
   then m
-  else {
-    let m = vector_update_subrange(m.bits, 35, 34,  a);
-    Mk_Mstatus(m)
-  }
-}
+  else Mk_Mstatus([m.bits with 35..34 = a])
 
-function get_mstatus_UXL(m : Mstatus) -> arch_xlen = {
+function get_mstatus_UXL(m : Mstatus) -> arch_xlen =
   if   xlen == 32
   then arch_to_bits(RV32)
   else m.bits[33 .. 32]
-}
 
-function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
+function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus =
   if   xlen == 32
   then m
-  else {
-    let m = vector_update_subrange(m.bits, 33, 32,  a);
-    Mk_Mstatus(m)
-  }
-}
+  else Mk_Mstatus([m.bits with 33..32 = a])
 
 function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
   /*
@@ -285,6 +278,15 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
   } else m
 }
 
+register mstatus : Mstatus = {
+  // Initialise SXL and UXL.
+  let mxl = arch_to_bits(if xlen == 32 then RV32 else RV64);
+  let m = Mk_Mstatus(zeros());
+  let m = set_mstatus_SXL(m, mxl);
+  let m = set_mstatus_UXL(m, mxl);
+  m
+}
+
 mapping clause csr_name_map = 0x300  <-> "mstatus"
 
 function clause is_CSR_defined(0x300) = true // mstatus
@@ -645,12 +647,12 @@ function retire_instruction() -> unit = {
 }
 
 /* machine information registers */
-register mvendorid : bits(32)
-register mimpid : xlenbits
-register marchid : xlenbits
+register mvendorid : bits(32) = zeros()
+register mimpid : xlenbits = zeros()
+register marchid : xlenbits = zeros()
 /* TODO: this should be readonly, and always 0 for now */
-register mhartid : xlenbits
-register mconfigptr : xlenbits
+register mhartid : xlenbits = zeros()
+register mconfigptr : xlenbits = zeros()
 
 mapping clause csr_name_map = 0xF11  <-> "mvendorid"
 mapping clause csr_name_map = 0xF12  <-> "marchid"
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
index 64fe15696..5bb7b974d 100644
--- a/model/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
@@ -449,6 +449,6 @@ function translateAddr(vAddr   : virtaddr,
 // Initialize Virtual Memory state
 
 // PUBLIC: invoked from init_model()
-function init_vmem() -> unit = init_TLB()
+function reset_vmem() -> unit = reset_TLB()
 
 // ****************************************************************
diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail
index d066f1356..86508710b 100644
--- a/model/riscv_vmem_tlb.sail
+++ b/model/riscv_vmem_tlb.sail
@@ -48,8 +48,8 @@ register tlb : vector(num_tlb_entries, option(TLB_Entry)) = [
 function tlb_hash(vaddr : bits(64)) -> tlb_index_range =
   unsigned(vaddr[17 .. 12])
 
-// PUBLIC: invoked in init_vmem() [riscv_vmem.sail]
-function init_TLB() -> unit = {
+// PUBLIC: invoked in reset_vmem() [riscv_vmem.sail]
+function reset_TLB() -> unit = {
   foreach (i from 0 to (length(tlb) - 1)) {
     tlb[i] = None();
   }