Rename enable-fiom to enable-writable-fiom

This is a much clearer name because the option allows code to enable FIOM, it doesn't enable FIOM itself.

11 files changed, 46 insertions, 46 deletions

diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index 52e050a..f2dfab4 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -37,9 +37,9 @@ bool sys_enable_zfinx(unit u)
   return rv_enable_zfinx;
 }
 
-bool sys_enable_fiom(unit u)
+bool sys_enable_writable_fiom(unit u)
 {
-  return rv_enable_fiom;
+  return rv_enable_writable_fiom;
 }
 
 bool sys_enable_writable_misa(unit u)
diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
index 8dadbd5..4442f95 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -6,7 +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 sys_enable_writable_fiom(unit);
 
 bool plat_enable_dirty_update(unit);
 bool plat_enable_misaligned_access(unit);
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index 805dd3c..34406ca 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -13,7 +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;
+bool rv_enable_writable_fiom = true;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index a2c758f..c74cda7 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -17,7 +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 bool rv_enable_writable_fiom;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index d841c6d..276be0c 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -50,7 +50,7 @@ const char *RV32ISA = "RV32IMAC";
 #define CSR_MIP 0x344
 
 #define OPT_TRACE_OUTPUT 1000
-#define OPT_ENABLE_FIOM 1001
+#define OPT_ENABLE_WRITABLE_FIOM 1001
 
 static bool do_dump_dts = false;
 static bool do_show_times = false;
@@ -117,35 +117,35 @@ char *sailcov_file = NULL;
 #endif
 
 static struct option options[] = {
-    {"enable-dirty-update",         no_argument,       0, 'd'             },
-    {"enable-misaligned",           no_argument,       0, 'm'             },
-    {"enable-pmp",                  no_argument,       0, 'P'             },
-    {"enable-next",                 no_argument,       0, 'N'             },
-    {"ram-size",                    required_argument, 0, 'z'             },
-    {"disable-compressed",          no_argument,       0, 'C'             },
-    {"disable-writable-misa",       no_argument,       0, 'I'             },
-    {"disable-fdext",               no_argument,       0, 'F'             },
-    {"mtval-has-illegal-inst-bits", no_argument,       0, 'i'             },
-    {"device-tree-blob",            required_argument, 0, 'b'             },
-    {"terminal-log",                required_argument, 0, 't'             },
-    {"show-times",                  required_argument, 0, 'p'             },
-    {"report-arch",                 no_argument,       0, 'a'             },
-    {"test-signature",              required_argument, 0, 'T'             },
-    {"signature-granularity",       required_argument, 0, 'g'             },
+    {"enable-dirty-update",         no_argument,       0, 'd'                     },
+    {"enable-misaligned",           no_argument,       0, 'm'                     },
+    {"enable-pmp",                  no_argument,       0, 'P'                     },
+    {"enable-next",                 no_argument,       0, 'N'                     },
+    {"ram-size",                    required_argument, 0, 'z'                     },
+    {"disable-compressed",          no_argument,       0, 'C'                     },
+    {"disable-writable-misa",       no_argument,       0, 'I'                     },
+    {"disable-fdext",               no_argument,       0, 'F'                     },
+    {"mtval-has-illegal-inst-bits", no_argument,       0, 'i'                     },
+    {"device-tree-blob",            required_argument, 0, 'b'                     },
+    {"terminal-log",                required_argument, 0, 't'                     },
+    {"show-times",                  required_argument, 0, 'p'                     },
+    {"report-arch",                 no_argument,       0, 'a'                     },
+    {"test-signature",              required_argument, 0, 'T'                     },
+    {"signature-granularity",       required_argument, 0, 'g'                     },
 #ifdef RVFI_DII
-    {"rvfi-dii",                    required_argument, 0, 'r'             },
+    {"rvfi-dii",                    required_argument, 0, 'r'                     },
 #endif
-    {"help",                        no_argument,       0, 'h'             },
-    {"trace",                       optional_argument, 0, 'v'             },
-    {"no-trace",                    optional_argument, 0, 'V'             },
-    {"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 },
+    {"help",                        no_argument,       0, 'h'                     },
+    {"trace",                       optional_argument, 0, 'v'                     },
+    {"no-trace",                    optional_argument, 0, 'V'                     },
+    {"trace-output",                required_argument, 0, OPT_TRACE_OUTPUT        },
+    {"inst-limit",                  required_argument, 0, 'l'                     },
+    {"enable-zfinx",                no_argument,       0, 'x'                     },
+    {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},
 #ifdef SAILCOV
-    {"sailcov-file",                required_argument, 0, 'c'             },
+    {"sailcov-file",                required_argument, 0, 'c'                     },
 #endif
-    {0,                             0,                 0, 0               }
+    {0,                             0,                 0, 0                       }
 };
 
 static void print_usage(const char *argv0, int ec)
@@ -304,10 +304,10 @@ 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:
+    case OPT_ENABLE_WRITABLE_FIOM:
       fprintf(stderr,
               "enabling FIOM (Fence of I/O implies Memory) bit in menvcfg.\n");
-      rv_enable_fiom = true;
+      rv_enable_writable_fiom = true;
       break;
     case 's':
       do_dump_dts = true;
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index 5d1fd85..5f92ee9 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -161,9 +161,9 @@ 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 sys_enable_writable_fiom : unit -> bool
+let sys_enable_writable_fiom () = true
+declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`
 
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v
index c879bf8..b17f753 100644
--- a/handwritten_support/riscv_extras.v
+++ b/handwritten_support/riscv_extras.v
@@ -200,7 +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.
+Axiom sys_enable_writable_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. *)
diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem
index a7b4899..102d082 100644
--- a/handwritten_support/riscv_extras_sequential.lem
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -153,9 +153,9 @@ 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 sys_enable_writable_fiom : unit -> bool
+let sys_enable_writable_fiom () = true
+declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`
 
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 77c9714..81a6c76 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -152,7 +152,7 @@ val sys_enable_zfinx = {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _
 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
+val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
 
 /* This function allows an extension to veto a write to Misa
    if it would violate an alignment restriction on
@@ -857,7 +857,7 @@ 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);
+  let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
   // Other extensions are not implemented yet so all other fields are read only zero.
   o
 }
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index 6bc9372..1e61165 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -11,7 +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 config_enable_writable_fiom        = ref true
 
 let platform_arch = ref P.RV64
 
@@ -84,7 +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 enable_writable_fiom ()          = !config_enable_writable_fiom
 
 let rom_base ()   = arch_bits_of_int64 P.rom_base
 let rom_size ()   = arch_bits_of_int   !rom_size_ref
diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml
index c5b427d..814f887b9 100644
--- a/ocaml_emulator/riscv_ocaml_sim.ml
+++ b/ocaml_emulator/riscv_ocaml_sim.ml
@@ -50,8 +50,8 @@ 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-writable-fiom",
+                           Arg.Set P.config_enable_writable_fiom,
                            " enable FIOM (Fence of I/O implies Memory) bit in menvcfg");
                           ("-disable-rvc",
                            Arg.Clear P.config_enable_rvc,