Implement menvcfg

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
@@ -302,6 +304,11 @@ static int 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
@@ -597,6 +600,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, if sys_enable_fiom() then v.FIOM() else 0b0);
+  // 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");