diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 82bfa0685..79a24c2cb 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -968,8 +968,8 @@ mapping clause encdec = SRET() function clause execute SRET() = { let sret_illegal : bool = match cur_privilege { User => true, - Supervisor => not(haveSupMode ()) | mstatus.TSR() == 0b1, - Machine => not(haveSupMode ()) + Supervisor => not(extension("S")) | mstatus.TSR() == 0b1, + Machine => not(extension("S")) }; if sret_illegal then { handle_illegal(); RETIRE_FAIL } diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index 2704fc5c1..2de2a9830 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -87,7 +87,7 @@ mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2) if extension(" <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011 function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = { - if extension("M") | haveZmmul() then { + if extension("M") | extension("Zmmul") then { let rs1_val = X(rs1); let rs2_val = X(rs2); let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val); @@ -179,7 +179,7 @@ mapping clause encdec = MULW(rs2, rs1, rd) if extension("M") & sizeof(xlen) == 64 function clause execute (MULW(rs2, rs1, rd)) = { - if extension("M") | haveZmmul() then { + if extension("M") | extension("Zmmul") then { let rs1_val = X(rs1)[31..0]; let rs2_val = X(rs2)[31..0]; let rs1_int : int = signed(rs1_val); diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail index 584f1cc02..7532debc5 100644 --- a/model/riscv_insts_next.sail +++ b/model/riscv_insts_next.sail @@ -77,7 +77,7 @@ mapping clause encdec = URET() <-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute URET() = { - if not(haveUsrMode()) | not(sys_enable_next()) + if not(extension("U")) | not(sys_enable_next()) then handle_illegal() else if not(ext_check_xret_priv(User)) then ext_fail_xret_priv() diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 432fd0d6e..d37093b93 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -70,14 +70,14 @@ /* Functional specification for the 'N' user-level interrupts standard extension. */ -function clause ext_is_CSR_defined(0x000, _) = haveUsrMode() & haveNExt() // ustatus -function clause ext_is_CSR_defined(0x004, _) = haveUsrMode() & haveNExt() // uie -function clause ext_is_CSR_defined(0x005, _) = haveUsrMode() & haveNExt() // utvec -function clause ext_is_CSR_defined(0x040, _) = haveUsrMode() & haveNExt() // uscratch -function clause ext_is_CSR_defined(0x041, _) = haveUsrMode() & haveNExt() // uepc -function clause ext_is_CSR_defined(0x042, _) = haveUsrMode() & haveNExt() // ucause -function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() & haveNExt() // utval -function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() & haveNExt() // uip +function clause ext_is_CSR_defined(0x000, _) = extension("U") & extension("N") // ustatus +function clause ext_is_CSR_defined(0x004, _) = extension("U") & extension("N") // uie +function clause ext_is_CSR_defined(0x005, _) = extension("U") & extension("N") // utvec +function clause ext_is_CSR_defined(0x040, _) = extension("U") & extension("N") // uscratch +function clause ext_is_CSR_defined(0x041, _) = extension("U") & extension("N") // uepc +function clause ext_is_CSR_defined(0x042, _) = extension("U") & extension("N") // ucause +function clause ext_is_CSR_defined(0x043, _) = extension("U") & extension("N") // utval +function clause ext_is_CSR_defined(0x044, _) = extension("U") & extension("N") // uip function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits()) function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits()) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 3830725d1..a03397572 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -86,14 +86,14 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = /* machine mode: trap setup */ 0x300 => p == Machine, // mstatus 0x301 => p == Machine, // misa - 0x302 => p == Machine & (haveSupMode() | haveNExt()), // medeleg - 0x303 => p == Machine & (haveSupMode() | haveNExt()), // mideleg + 0x302 => p == Machine & (extension("S") | extension("N")), // medeleg + 0x303 => p == Machine & (extension("S") | extension("N")), // mideleg 0x304 => p == Machine, // mie 0x305 => p == Machine, // mtvec - 0x306 => p == Machine & haveUsrMode(), // mcounteren - 0x30A => p == Machine & haveUsrMode(), // menvcfg + 0x306 => p == Machine & extension("U"), // mcounteren + 0x30A => p == Machine & extension("U"), // menvcfg 0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush - 0x31A => p == Machine & haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh + 0x31A => p == Machine & extension("U") & (sizeof(xlen) == 32), // menvcfgh 0x320 => p == Machine, // mcountinhibit /* machine mode: trap handling */ 0x340 => p == Machine, // mscratch @@ -135,35 +135,35 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x7a0 => p == Machine, /* supervisor mode: trap setup */ - 0x100 => haveSupMode() & (p == Machine | p == Supervisor), // sstatus - 0x102 => haveSupMode() & haveNExt() & (p == Machine | p == Supervisor), // sedeleg - 0x103 => haveSupMode() & haveNExt() & (p == Machine | p == Supervisor), // sideleg - 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 + 0x100 => extension("S") & (p == Machine | p == Supervisor), // sstatus + 0x102 => extension("S") & extension("N") & (p == Machine | p == Supervisor), // sedeleg + 0x103 => extension("S") & extension("N") & (p == Machine | p == Supervisor), // sideleg + 0x104 => extension("S") & (p == Machine | p == Supervisor), // sie + 0x105 => extension("S") & (p == Machine | p == Supervisor), // stvec + 0x106 => extension("S") & (p == Machine | p == Supervisor), // scounteren + 0x10A => extension("S") & (p == Machine | p == Supervisor), // senvcfg /* supervisor mode: trap handling */ - 0x140 => haveSupMode() & (p == Machine | p == Supervisor), // sscratch - 0x141 => haveSupMode() & (p == Machine | p == Supervisor), // sepc - 0x142 => haveSupMode() & (p == Machine | p == Supervisor), // scause - 0x143 => haveSupMode() & (p == Machine | p == Supervisor), // stval - 0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip + 0x140 => extension("S") & (p == Machine | p == Supervisor), // sscratch + 0x141 => extension("S") & (p == Machine | p == Supervisor), // sepc + 0x142 => extension("S") & (p == Machine | p == Supervisor), // scause + 0x143 => extension("S") & (p == Machine | p == Supervisor), // stval + 0x144 => extension("S") & (p == Machine | p == Supervisor), // sip /* supervisor mode: address translation */ - 0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp + 0x180 => extension("S") & (p == Machine | p == Supervisor), // satp /* user mode: counters */ - 0xC00 => haveUsrMode(), // cycle - 0xC01 => haveUsrMode(), // time - 0xC02 => haveUsrMode(), // instret + 0xC00 => extension("U"), // cycle + 0xC01 => extension("U"), // time + 0xC02 => extension("U"), // instret - 0xC80 => haveUsrMode() & (sizeof(xlen) == 32), // cycleh - 0xC81 => haveUsrMode() & (sizeof(xlen) == 32), // timeh - 0xC82 => haveUsrMode() & (sizeof(xlen) == 32), // instreth + 0xC80 => extension("U") & (sizeof(xlen) == 32), // cycleh + 0xC81 => extension("U") & (sizeof(xlen) == 32), // timeh + 0xC82 => extension("U") & (sizeof(xlen) == 32), // instreth /* user mode: Zkr */ - 0x015 => haveZkr(), + 0x015 => extension("Zkr"), /* check extensions */ _ => ext_is_CSR_defined(csr, p) @@ -183,9 +183,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool = (0xC01, Supervisor) => mcounteren.TM() == 0b1, (0xC02, Supervisor) => mcounteren.IR() == 0b1, - (0xC00, User) => mcounteren.CY() == 0b1 & (not(haveSupMode()) | scounteren.CY() == 0b1), - (0xC01, User) => mcounteren.TM() == 0b1 & (not(haveSupMode()) | scounteren.TM() == 0b1), - (0xC02, User) => mcounteren.IR() == 0b1 & (not(haveSupMode()) | scounteren.IR() == 0b1), + (0xC00, User) => mcounteren.CY() == 0b1 & (not(extension("S")) | scounteren.CY() == 0b1), + (0xC01, User) => mcounteren.TM() == 0b1 & (not(extension("S")) | scounteren.TM() == 0b1), + (0xC02, User) => mcounteren.IR() == 0b1 & (not(extension("S")) | scounteren.IR() == 0b1), (_, _) => /* no HPM counters for now */ if 0xC03 <=_u csr & csr <=_u 0xC1F @@ -244,11 +244,11 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { let idx = num_of_ExceptionType(e); let super = bit_to_bool(medeleg.bits()[idx]); /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */ - let user = if haveSupMode() - then super & haveNExt() & bit_to_bool(sedeleg.bits()[idx]) - else super & haveNExt(); - let deleg = if haveUsrMode() & user then User - else if haveSupMode() & super then Supervisor + let user = if extension("S") + then super & extension("N") & bit_to_bool(sedeleg.bits()[idx]) + else super & extension("N"); + let deleg = if extension("U") & user then User + else if extension("S") & super then Supervisor else Machine; /* We cannot transition to a less-privileged mode. */ if privLevel_to_bits(deleg) <_u privLevel_to_bits(p) @@ -304,7 +304,7 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits * allows for example the M_Timer to be delegated to the U-mode. */ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { - assert(haveUsrMode(), "no user mode: M/U or M/S/U system required"); + assert(extension("U"), "no user mode: M/U or M/S/U system required"); let effective_pending = mip.bits() & mie.bits(); if effective_pending == zero_extend(0b0) then None() /* fast path */ else { @@ -313,13 +313,13 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { * considered blocked. */ let mIE = priv != Machine | (priv == Machine & mstatus.MIE() == 0b1); - let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus.SIE() == 0b1)); - let uIE = haveNExt() & (priv == User & mstatus.UIE() == 0b1); + let sIE = extension("S") & (priv == User | (priv == Supervisor & mstatus.SIE() == 0b1)); + let uIE = extension("N") & (priv == User & mstatus.UIE() == 0b1); match processPending(mip, mie, mideleg.bits(), mIE) { Ints_Empty() => None(), Ints_Pending(p) => let r = (p, Machine) in Some(r), Ints_Delegated(d) => - if not(haveSupMode()) then { + if not(extension("S")) then { if uIE then let r = (d, User) in Some(r) else None() } else { @@ -343,7 +343,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege /* If we don't have different privilege levels, we don't need to check delegation. * Absence of U-mode implies absence of S-mode. */ - if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then { + if not(extension("U")) | (not(extension("S")) & not(extension("N"))) then { assert(priv == Machine, "invalid current privilege"); let enabled_pending = mip.bits() & mie.bits(); match findPendingInterrupt(enabled_pending) { @@ -422,7 +422,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen prepare_trap_vector(del_priv, mcause) }, Supervisor => { - assert (haveSupMode(), "no supervisor mode present for delegation"); + assert (extension("S"), "no supervisor mode present for delegation"); scause->IsInterrupt() = bool_to_bits(intr); scause->Cause() = zero_extend(c); @@ -447,7 +447,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen prepare_trap_vector(del_priv, scause) }, User => { - assert(haveUsrMode(), "no user mode present for delegation"); + assert(extension("U"), "no user mode present for delegation"); ucause->IsInterrupt() = bool_to_bits(intr); ucause->Cause() = zero_extend(c); @@ -484,7 +484,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, mstatus->MIE() = mstatus.MPIE(); mstatus->MPIE() = 0b1; cur_privilege = privLevel_of_bits(mstatus.MPP()); - mstatus->MPP() = privLevel_to_bits(if haveUsrMode() then User else Machine); + mstatus->MPP() = privLevel_to_bits(if extension("U") then User else Machine); if cur_privilege != Machine then mstatus->MPRV() = 0b0; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 97d43a350..92068f328 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -176,45 +176,6 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { } } -/* helpers to check support for various extensions. */ -/* we currently don't model 'E', so always assume 'I'. */ -function haveAtomics() -> bool = misa.A() == 0b1 -function haveRVC() -> bool = misa.C() == 0b1 -function haveMulDiv() -> bool = misa.M() == 0b1 -function haveSupMode() -> bool = misa.S() == 0b1 -function haveUsrMode() -> bool = misa.U() == 0b1 -function haveNExt() -> bool = misa.N() == 0b1 -/* see below for F and D (and Z*inx counterparts) extension tests */ - -/* BitManip extension support. */ -function haveZba() -> bool = true -function haveZbb() -> bool = true -function haveZbc() -> bool = true -function haveZbs() -> bool = true - -/* Zfa (additional FP) extension */ -function haveZfa() -> bool = true - -/* Scalar Cryptography extensions support. */ -function haveZbkb() -> bool = true -function haveZbkc() -> bool = true -function haveZbkx() -> bool = true - -/* Cryptography extension support. Note these will need updating once */ -/* Sail can be dynamically configured with different extension support */ -/* and have dynamic changes of XLEN via S/UXL */ -function haveZkr() -> bool = true -function haveZksh() -> bool = true -function haveZksed() -> bool = true -function haveZknh() -> bool = true -function haveZkne() -> bool = true -function haveZknd() -> bool = true - -function haveZmmul() -> bool = true - -/* Zicond extension support */ -function haveZicond() -> bool = true - bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -294,6 +255,67 @@ function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { } } +val extension : (string) -> bool + +/* helper to check support for various extensions. */ +/* we currently don't model 'E', so always assume 'I'. */ +function extension(ext) = { + match ext { + "A" => misa.A() == 0b1, + "C" => misa.C() == 0b1, + + /* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */ + "D" => (misa.D() == 0b1) & (mstatus.FS() != 0b00), + "F" => (misa.F() == 0b1) & (mstatus.FS() != 0b00), + + "M" => misa.M() == 0b1, + "N" => misa.N() == 0b1, + "U" => misa.U() == 0b1, + "S" => misa.S() == 0b1, + + /* V extension has to enable both via misa.V as well as mstatus.VS */ + "V" => (misa.V() == 0b1) & (mstatus.VS() != 0b00), + + /* BitManip extension support. */ + "Zba" => true, + "Zbb" => true, + "Zbc" => true, + "Zbs" => true, + + /* Scalar Cryptography extensions support. */ + "Zbkb" => true, + "Zbkc" => true, + "Zbkx" => true, + + /* Zfa (additional FP) extension */ + "Zfa" => true, + + /* Zfh (half-precision) extension depends on misa.F and mstatus.FS */ + "Zfh" => (misa.F() == 0b1) & (mstatus.FS() != 0b00), + + /* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */ + "Zdinx" => sys_enable_zfinx() & sizeof(flen) >= 64, + "Zfinx" => sys_enable_zfinx(), + "Zhinx" => sys_enable_zfinx(), + + /* Zicond extension support */ + "Zicond" => true, + + /* Cryptography extension support. Note these will need updating once */ + /* Sail can be dynamically configured with different extension support */ + /* and have dynamic changes of XLEN via S/UXL */ + "Zkr" => true, + "Zksh" => true, + "Zksed" => true, + "Zknd" => true, + "Zkne" => true, + "Zknh" => true, + + "Zmmul" => true, + _ => false + } +} + function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { /* * Populate all defined fields using the bits of v, stripping anything @@ -325,13 +347,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { } else m; /* Hardwired to zero in the absence of 'U' or 'N'. */ - let m = if not(haveNExt()) then { + let m = if not(extension("N")) then { let m = update_UPIE(m, 0b0); let m = update_UIE(m, 0b0); m } else m; - if not(haveUsrMode()) then { + if not(extension("U")) then { let m = update_MPRV(m, 0b0); m } else m @@ -356,19 +378,6 @@ function in32BitMode() -> bool = { cur_Architecture() == RV32 } -/* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */ -function haveFExt() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00) -function haveDExt() -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00) -/* Zfh (half-precision) extension depends on misa.F and mstatus.FS */ -function haveZfh() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00) -/* V extension has to enable both via misa.V as well as mstatus.VS */ -function haveVExt() -> bool = (misa.V() == 0b1) & (mstatus.VS() != 0b00) - -/* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */ -function haveZhinx() -> bool = sys_enable_zfinx() -function haveZfinx() -> bool = sys_enable_zfinx() -function haveZdinx() -> bool = sys_enable_zfinx() & sizeof(flen) >= 64 - /* interrupt processing state */ bitfield Minterrupts : xlenbits = { @@ -395,7 +404,7 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { let m = update_SEI(o, v.SEI()); let m = update_STI(m, v.STI()); let m = update_SSI(m, v.SSI()); - if haveUsrMode() & haveNExt() then { + if extension("U") & extension("N") then { let m = update_UEI(m, v.UEI()); let m = update_UTI(m, v.UTI()); let m = update_USI(m, v.USI()); @@ -412,7 +421,7 @@ function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { let m = update_STI(m, v.STI()); let m = update_SSI(m, v.SSI()); /* The U-mode bits will be modified if we have the 'N' extension. */ - if haveUsrMode() & haveNExt() then { + if extension("U") & extension("N") then { let m = update_UEI(m, v.UEI()); let m = update_UTI(m, v.UTI()); let m = update_USI(m, v.USI()); @@ -716,7 +725,7 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m; - if haveNExt() then { + if extension("N") then { let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m; let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m; m @@ -733,7 +742,7 @@ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru let m = if d.SEI() == 0b1 then update_SEI(m, s.SEI()) else m; let m = if d.STI() == 0b1 then update_STI(m, s.STI()) else m; let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m; - if haveNExt() then { + if extension("N") then { let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m; let m = if d.UTI() == 0b1 then update_UTI(m, s.UTI()) else m; let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m; @@ -964,40 +973,3 @@ function get_vtype_vma() = decode_agtype(vtype.vma()) val get_vtype_vta : unit -> agtype effect {rreg} function get_vtype_vta() = decode_agtype(vtype.vta()) - -val extension : (string) -> bool - -function extension(ext) = { - match ext { - "A" => misa.A() == 0b1, - "C" => misa.C() == 0b1, - "D" => (misa.D() == 0b1) & (mstatus.FS() != 0b00), - "F" => (misa.F() == 0b1) & (mstatus.FS() != 0b00), - "M" => misa.M() == 0b1, - "N" => misa.N() == 0b1, - "U" => misa.U() == 0b1, - "S" => misa.S() == 0b1, - "V" => (misa.V() == 0b1) & (mstatus.VS() != 0b00), - "Zba" => true, - "Zbb" => true, - "Zbc" => true, - "Zbkb" => true, - "Zbkc" => true, - "Zbkx" => true, - "Zbs" => true, - "Zfa" => true, - "Zfh" => (misa.F() == 0b1) & (mstatus.FS() != 0b00), - "Zdinx" => sys_enable_zfinx() & sizeof(flen) >= 64, - "Zfinx" => sys_enable_zfinx(), - "Zhinx" => sys_enable_zfinx(), - "Zicond" => true, - "Zkr" => true, - "Zksh" => true, - "Zksed" => true, - "Zknd" => true, - "Zkne" => true, - "Zknh" => true, - "Zmmul" => true, - _ => false - } -}