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

@@ -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];

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

@@ -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]               */

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"

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

@@ -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) ^ ")")