aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--c_emulator/riscv_platform.c4
-rw-r--r--c_emulator/riscv_platform.h2
-rw-r--r--c_emulator/riscv_platform_impl.c2
-rw-r--r--c_emulator/riscv_platform_impl.h2
-rw-r--r--c_emulator/riscv_sim.c56
-rw-r--r--handwritten_support/riscv_extras.lem6
-rw-r--r--handwritten_support/riscv_extras.v2
-rw-r--r--handwritten_support/riscv_extras_sequential.lem6
-rw-r--r--model/riscv_sys_regs.sail4
-rw-r--r--ocaml_emulator/platform.ml4
-rw-r--r--ocaml_emulator/riscv_ocaml_sim.ml4
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,
generated by cgit v1.1 at 2024-11-16 20:19:11 +0000