From 51a6c967fb320c2d47a3630b1f392e54eb69c3d7 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Sat, 23 Sep 2023 19:57:38 +0100 Subject: 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. --- model/riscv_insts_base.sail | 17 +++++++++++++++++ model/riscv_insts_zicsr.sail | 7 +++++++ model/riscv_sys_control.sail | 6 ++++++ model/riscv_sys_regs.sail | 45 ++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 75 insertions(+) (limited to 'model') diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index b5e699e..f5ef8cd 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 f6e7672..425f7a3 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 7746b6b..cfac8bd 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 cb44664..77c9714 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, + } +} -- cgit v1.1