diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 52e050ac3..f2dfab4af 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 8dadbd5de..4442f9503 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 805dd3c90..34406cae5 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 a2c758fcb..c74cda739 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 d841c6da7..276be0cbe 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 5d1fd85a5..5f92ee904 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 c879bf844..b17f75343 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 a7b4899ef..102d08242 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 77c971412..81a6c7664 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 6bc93723b..1e611657a 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 c5b427dd4..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,