From 338d6bced49455963b024c69c6c10764401099f9 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Sat, 23 Sep 2023 19:57:38 +0100 Subject: [PATCH 1/2] 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 | 5 +++ c_emulator/riscv_platform.h | 1 + c_emulator/riscv_platform_impl.c | 1 + c_emulator/riscv_platform_impl.h | 1 + c_emulator/riscv_sim.c | 7 +++ handwritten_support/riscv_extras.lem | 4 ++ handwritten_support/riscv_extras.v | 1 + .../riscv_extras_sequential.lem | 4 ++ model/riscv_insts_base.sail | 17 +++++++ model/riscv_insts_zicsr.sail | 7 +++ model/riscv_sys_control.sail | 6 +++ model/riscv_sys_regs.sail | 45 +++++++++++++++++++ ocaml_emulator/platform.ml | 2 + ocaml_emulator/riscv_ocaml_sim.ml | 3 ++ 14 files changed, 104 insertions(+) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 917a36a95..52e050ac3 100644 --- a/c_emulator/riscv_platform.c +++ b/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; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index aec59d017..8dadbd5de 100644 --- a/c_emulator/riscv_platform.h +++ b/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); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 148c72bd4..805dd3c90 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/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); diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index aa8d391de..a2c758fcb 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/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; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 8f7f9e1ca..d841c6da7 100644 --- a/c_emulator/riscv_sim.c +++ b/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; diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index a476136f7..5d1fd85a5 100644 --- a/handwritten_support/riscv_extras.lem +++ b/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` diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 14029ee4e..c879bf844 100644 --- a/handwritten_support/riscv_extras.v +++ b/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. *) diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 41ca9c6f8..a7b4899ef 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/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` diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index b5e699e70..f5ef8cd29 100644 --- a/model/riscv_insts_base.sail +++ b/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), diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index f6e767265..425f7a3dc 100644 --- a/model/riscv_insts_zicsr.sail +++ b/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()) }, diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index cf0a488cc..6911b0627 100644 --- a/model/riscv_sys_control.sail +++ b/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 diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 47744698d..3650e51f5 100644 --- a/model/riscv_sys_regs.sail +++ b/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, + } +} diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index ccf487589..6bc93723b 100644 --- a/ocaml_emulator/platform.ml +++ b/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 diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 6e612ad26..c5b427dd4 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/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"); From da76e06b3f5098763506b2a26b85e5ce44c389ea Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 10 Oct 2023 10:12:03 +0100 Subject: [PATCH 2/2] 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. --- c_emulator/riscv_platform.c | 4 +- c_emulator/riscv_platform.h | 2 +- c_emulator/riscv_platform_impl.c | 2 +- c_emulator/riscv_platform_impl.h | 2 +- c_emulator/riscv_sim.c | 56 +++++++++---------- handwritten_support/riscv_extras.lem | 6 +- handwritten_support/riscv_extras.v | 2 +- .../riscv_extras_sequential.lem | 6 +- model/riscv_sys_regs.sail | 4 +- ocaml_emulator/platform.ml | 4 +- ocaml_emulator/riscv_ocaml_sim.ml | 4 +- 11 files changed, 46 insertions(+), 46 deletions(-) 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 3650e51f5..098e15497 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,