Refactor chip reset

This simplifies, clarifies and fixes the reset functionality.

Until now the model conflates reset and initialisation, and does way more than it should on reset. The RISC-V spec only requires a very small number of things to be reset.

This change:

1. Renames the `init` functions to `reset`, to clarify that they correspond to resetting the chip.
2. Removes the `ext_init` and `ext_rvfi_init` functions. The latter is not used and the former is only used by the old CHERI code.
2. Removes the reset of the X and F registers. These are non-reset.
3. Removes the reset of various CSRs that are non-reset (`mip`, `mie`, `mideleg`, `mtvec`, `mepc`, etc).
4. Adds reset of `mstatus[MIE]` and `mstatus[MPRV]`. As far as I can see they were missing.
5. Add one-time init of `mhartid` etc to 0.

I didn't remove the vector register resets yet. That needs a bigger refactor.

Also note that currently there is no way to actually do a chip reset mid-simulation, but that will be needed eventually.

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);

c_emulator/riscv_sim.c

@@ -669,7 +669,6 @@ 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);

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);
 

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.

model/riscv_fdext_regs.sail

@@ -369,42 +369,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]               */

model/riscv_pmp_control.sail

@@ -126,7 +126,7 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, 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"

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
-}

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();
 }

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 = ()

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();
-  ()
-}

model/riscv_sys_control.sail

@@ -491,13 +491,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     = zero_extend(0b0);
-  mconfigptr  = zero_extend(0b0);
+function reset_misa() -> unit = {
+  misa.bits = zeros();
 
   misa[MXL] = arch_to_bits(if xlen == 32 then RV32 else RV64);
   misa[A]   = 0b1;                             /* atomics */
@@ -515,40 +510,48 @@ 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());
+}
 
-  /* set to little-endian mode */
-  if xlen == 64 then {
-    mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00])
-  };
-  mstatush.bits = zero_extend(0b0);
+// This function is called on reset, so it should perform the reset actions
+// described in the "Reset" section of the privileged architecture specification.
+function reset_sys() -> unit = {
+
+  // "Upon reset, a hard'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     = zero_extend(0b0);
-  mie.bits     = zero_extend(0b0);
-  mideleg.bits = zero_extend(0b0);
-  medeleg.bits = zero_extend(0b0);
-  mtvec.bits   = zero_extend(0b0);
-  mcause.bits  = zero_extend(0b0);
-  mepc            = zero_extend(0b0);
-  mtval           = zero_extend(0b0);
-  mscratch        = zero_extend(0b0);
+  // "The misa register is reset to enable the maximal set of supported extensions"
+  reset_misa();
 
-  mcycle          = zero_extend(0b0);
-  mtime           = zero_extend(0b0);
+  // "For implementations with the "A" standard extension, there is no valid load reservation."
+  cancel_reservation();
 
-  mcounteren.bits = zero_extend(0b0);
+  // "The pc is set to an implementation-defined reset vector."
+  // This is outside the scope of this function.
 
-  minstret           = zero_extend(0b0);
-  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 = zero_extend(0b0);
-  senvcfg.bits = zero_extend(0b0);
   /* initialize vector csrs */
   elen               = 0b1; /* ELEN=64 as the common case */
   vlen               = 0b0100; /* VLEN=512 as a default value */
@@ -567,9 +570,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(zero_extend(0b0) : xlenbits) ^ ")")

model/riscv_sys_regs.sail

@@ -213,35 +213,25 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv :
   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 = {
   /*
@@ -532,12 +522,12 @@ function write_mhpmevent(index : hpmidx, value : xlenbits) -> unit =
   if sys_writable_hpm_counters()[index] == bitone then mhpmevent[index] = value
 
 /* informational 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()
 
 /* S-mode registers */
 

model/riscv_vmem.sail

@@ -445,6 +445,6 @@ function translateAddr(vAddr   : xlenbits,
 // Initialize Virtual Memory state
 
 // PUBLIC: invoked from init_model()
-function init_vmem() -> unit = init_TLB()
+function reset_vmem() -> unit = reset_TLB()
 
 // ****************************************************************

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();
   }