Implement menvcfg

This implements the m/senvcfg(h) CSRs. This CSR is used to enable/disable extensions and behaviours for lower privilege modes. Currently the only implemented bit is FIOM which affects how fences work.

It also affects how atomic memory accesses work in non-cacheable regions, but the model does not currently support PMAs so that can't easily be implemented.

c_emulator/riscv_platform.c

@@ -37,6 +37,11 @@ bool sys_enable_zfinx(unit u)
  return rv_enable_zfinx;
 }
 
+bool sys_enable_fiom(unit u)
+{
+ return rv_enable_fiom;
+}
+
 bool sys_enable_writable_misa(unit u)
 {
  return rv_enable_writable_misa;

c_emulator/riscv_platform.h

@@ -6,6 +6,7 @@ bool sys_enable_next(unit);
 bool sys_enable_fdext(unit);
 bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
+bool sys_enable_fiom(unit);
 
 bool plat_enable_dirty_update(unit);
 bool plat_enable_misaligned_access(unit);

c_emulator/riscv_platform_impl.c

@@ -13,6 +13,7 @@ bool rv_enable_fdext = true;
 bool rv_enable_dirty_update = false;
 bool rv_enable_misaligned = false;
 bool rv_mtval_has_illegal_inst_bits = false;
+bool rv_enable_fiom = true;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);

c_emulator/riscv_platform_impl.h

@@ -17,6 +17,7 @@ extern bool rv_enable_writable_misa;
 extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
 extern bool rv_mtval_has_illegal_inst_bits;
+extern bool rv_enable_fiom;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;

c_emulator/riscv_sim.c

@@ -50,6 +50,7 @@ const char *RV32ISA = "RV32IMAC";
 #define CSR_MIP 0x344
 
 #define OPT_TRACE_OUTPUT 1000
+#define OPT_ENABLE_FIOM 1001
 
 static bool do_dump_dts = false;
 static bool do_show_times = false;
@@ -140,6 +141,7 @@ static struct option options[] = {
  {"trace-output", required_argument, 0, OPT_TRACE_OUTPUT},
  {"inst-limit", required_argument, 0, 'l' },
  {"enable-zfinx", no_argument, 0, 'x' },
+ {"enable-fiom", no_argument, 0, OPT_ENABLE_FIOM },
 #ifdef SAILCOV
  {"sailcov-file", required_argument, 0, 'c' },
 #endif
@@ -298,6 +300,11 @@ char *process_args(int argc, char **argv)
  fprintf(stderr, "enabling storing illegal instruction bits in mtval.\n");
  rv_mtval_has_illegal_inst_bits = true;
  break;
+ case OPT_ENABLE_FIOM:
+ fprintf(stderr,
+ "enabling FIOM (Fence of I/O implies Memory) bit in menvcfg.\n");
+ rv_enable_fiom = true;
+ break;
  case 's':
  do_dump_dts = true;
  break;

handwritten_support/riscv_extras.lem

@@ -161,6 +161,10 @@ val sys_enable_zfinx : unit -> bool
 let sys_enable_zfinx () = false
 declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
 
+val sys_enable_fiom : unit -> bool
+let sys_enable_fiom () = true
+declare ocaml target_rep function sys_enable_fiom = `Platform.enable_fiom`
+
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`

handwritten_support/riscv_extras.v

@@ -200,6 +200,7 @@ Axiom sys_enable_rvc : unit -> bool.
 Axiom sys_enable_fdext : unit -> bool.
 Axiom sys_enable_next : unit -> bool.
 Axiom sys_enable_zfinx : unit -> bool.
+Axiom sys_enable_fiom : unit -> bool.
 
 (* The constraint solver can do this itself, but a Coq bug puts
  anonymous_subproof into the term instead of an actual subproof. *)

handwritten_support/riscv_extras_sequential.lem

@@ -153,6 +153,10 @@ val sys_enable_next : unit -> bool
 let sys_enable_next () = true
 declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
 
+val sys_enable_fiom : unit -> bool
+let sys_enable_fiom () = true
+declare ocaml target_rep function sys_enable_fiom = `Platform.enable_fiom`
+
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`

model/riscv_insts_base.sail

@@ -637,10 +637,22 @@ union clause ast = FENCE : (bits(4), bits(4))
 mapping clause encdec = FENCE(pred, succ)
  <-> 0b0000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
+function effective_fence_set(set : bits(4), fiom : bool) -> bits(4) = {
+ // The bits are IORW. If FIOM is set then I implies R and O implies W.
+ if fiom then {
+ set[3 .. 2] @ (set[1 .. 0] | set[3 .. 2])
+ } else set
+}
+
 /* For future versions of Sail where barriers can be parameterised */
 $ifdef FEATURE_UNION_BARRIER
 
 function clause execute (FENCE(pred, succ)) = {
+ // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W.
+ let fiom = is_fiom_active();
+ let pred = effective_fence_set(pred, fiom);
+ let succ = effective_fence_set(succ, fiom);
+
  match (pred, succ) {
  (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw()),
  (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw()),
@@ -664,6 +676,11 @@ function clause execute (FENCE(pred, succ)) = {
 $else
 
 function clause execute (FENCE(pred, succ)) = {
+ // If the FIOM bit in menvcfg/senvcfg is set then the I/O bits can imply R/W.
+ let fiom = is_fiom_active();
+ let pred = effective_fence_set(pred, fiom);
+ let succ = effective_fence_set(succ, fiom);
+
  match (pred, succ) {
  (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw),
  (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw),

model/riscv_insts_zicsr.sail

@@ -98,7 +98,9 @@ function readCSR csr : csreg -> xlenbits = {
  (0x304, _) => mie.bits(),
  (0x305, _) => get_mtvec(),
  (0x306, _) => zero_extend(mcounteren.bits()),
+ (0x30A, _) => menvcfg.bits()[sizeof(xlen) - 1 .. 0],
  (0x310, 32) => mstatush.bits(),
+ (0x31A, 32) => menvcfg.bits()[63 .. 32],
  (0x320, _) => zero_extend(mcountinhibit.bits()),
 
  (0x340, _) => mscratch,
@@ -145,6 +147,7 @@ function readCSR csr : csreg -> xlenbits = {
  (0x104, _) => lower_mie(mie, mideleg).bits(),
  (0x105, _) => get_stvec(),
  (0x106, _) => zero_extend(scounteren.bits()),
+ (0x10A, _) => senvcfg.bits()[sizeof(xlen) - 1 .. 0],
  (0x140, _) => sscratch,
  (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(),
  (0x142, _) => scause.bits(),
@@ -186,7 +189,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
  (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) },
  (0x305, _) => { Some(set_mtvec(value)) },
  (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) },
+ (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) },
+ (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) },
  (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now
+ (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) },
  (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) },
  (0x340, _) => { mscratch = value; Some(mscratch) },
  (0x341, _) => { Some(set_xret_target(Machine, value)) },
@@ -233,6 +239,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
  (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) },
  (0x105, _) => { Some(set_stvec(value)) },
  (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) },
+ (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) },
  (0x140, _) => { sscratch = value; Some(sscratch) },
  (0x141, _) => { Some(set_xret_target(Supervisor, value)) },
  (0x142, _) => { scause->bits() = value; Some(scause.bits()) },

model/riscv_sys_control.sail

@@ -91,7 +91,9 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
  0x304 => p == Machine, // mie
  0x305 => p == Machine, // mtvec
  0x306 => p == Machine & haveUsrMode(), // mcounteren
+ 0x30A => p == Machine & haveUsrMode(), // menvcfg
  0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush
+ 0x31A => p == Machine & haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh
  0x320 => p == Machine, // mcountinhibit
  /* machine mode: trap handling */
  0x340 => p == Machine, // mscratch
@@ -139,6 +141,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
  0x104 => haveSupMode() & (p == Machine | p == Supervisor), // sie
  0x105 => haveSupMode() & (p == Machine | p == Supervisor), // stvec
  0x106 => haveSupMode() & (p == Machine | p == Supervisor), // scounteren
+ 0x10A => haveSupMode() & (p == Machine | p == Supervisor), // senvcfg
 
  /* supervisor mode: trap handling */
  0x140 => haveSupMode() & (p == Machine | p == Supervisor), // sscratch
@@ -598,6 +601,9 @@ function init_sys() -> unit = {
  minstret = zero_extend(0b0);
  minstret_increment = true;
 
+ menvcfg->bits() = zero_extend(0b0);
+ senvcfg->bits() = zero_extend(0b0);
+
  init_pmp();
 
  // log compatibility with spike

model/riscv_sys_regs.sail

@@ -150,6 +150,9 @@ val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _
 val sys_enable_zfinx = {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool
 /* whether the N extension was enabled at boot */
 val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool
+/* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
+ supervisor mode is implemented and non-bare addressing modes are supported. */
+val sys_enable_fiom = {c: "sys_enable_fiom", ocaml: "Platform.enable_fiom", _: "sys_enable_fiom"} : unit -> bool
 
 /* This function allows an extension to veto a write to Misa
  if it would violate an alignment restriction on
@@ -827,3 +830,45 @@ function read_seed_csr() -> xlenbits = {
 
 /* Writes to the seed CSR are ignored */
 function write_seed_csr () -> option(xlenbits) = None()
+
+// menvcfg is 64 bits. senvcfg is SXLEN bits and does not have the two
+// upper fields so for simplicity we can use the same type.
+bitfield Envcfg : bits(64) = {
+ // Supervisor TimeCmp Extension
+ STCE : 63,
+ // Page Based Memory Types Extension
+ PBMTE : 62,
+ // Reserved WPRI bits.
+ wpri_1 : 61 .. 8,
+ // Cache Block Zero instruction Enable
+ CBZE : 7,
+ // Cache Block Clean and Flush instruction Enable
+ CBCFE : 6,
+ // Cache Block Invalidate instruction Enable
+ CBIE : 5 .. 4,
+ // Reserved WPRI bits.
+ wpri_0 : 3 .. 1,
+ // Fence of I/O implies Memory
+ FIOM : 0,
+}
+
+register menvcfg : Envcfg
+register senvcfg : Envcfg
+
+function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
+ let v = Mk_Envcfg(v);
+ let o = update_FIOM(o, v.FIOM());
+ // Other extensions are not implemented yet so all other fields are read only zero.
+ o
+}
+
+// Return whether or not FIOM is currently active, based on the current
+// privilege and the menvcfg/senvcfg settings. This means that I/O fences
+// imply memory fence.
+function is_fiom_active() -> bool = {
+ match cur_privilege {
+ Machine => false,
+ Supervisor => menvcfg.FIOM() == 0b1,
+ User => (menvcfg.FIOM() | senvcfg.FIOM()) == 0b1,
+ }
+}

ocaml_emulator/platform.ml

@@ -11,6 +11,7 @@ let config_enable_dirty_update = ref false
 let config_enable_misaligned_access = ref false
 let config_mtval_has_illegal_inst_bits = ref false
 let config_enable_pmp = ref false
+let config_enable_fiom = ref true
 
 let platform_arch = ref P.RV64
 
@@ -83,6 +84,7 @@ let enable_misaligned_access () = !config_enable_misaligned_access
 let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
 let enable_pmp () = !config_enable_pmp
 let enable_zfinx () = false
+let enable_fiom () = !config_enable_fiom
 
 let rom_base () = arch_bits_of_int64 P.rom_base
 let rom_size () = arch_bits_of_int !rom_size_ref

ocaml_emulator/riscv_ocaml_sim.ml

@@ -50,6 +50,9 @@ let options = Arg.align ([("-dump-dts",
  ("-mtval-has-illegal-inst-bits",
  Arg.Set P.config_mtval_has_illegal_inst_bits,
  " mtval stores instruction bits on an illegal instruction exception");
+ ("-enable-fiom",
+ Arg.Set P.config_enable_fiom,
+ " enable FIOM (Fence of I/O implies Memory) bit in menvcfg");
  ("-disable-rvc",
  Arg.Clear P.config_enable_rvc,
  " disable the RVC extension on boot");