From 694c67d7d9c6f583eee08f0776fa8eba7c786597 Mon Sep 17 00:00:00 2001 From: Riya Jain Date: Tue, 9 Apr 2024 17:06:00 +0530 Subject: [PATCH] Make use of extension() instead of have*() * Move definition of function of `extension` * Utilize extension() instead of `haveZmmul()` * Utilize extension() instead of `haveUsrMode()` * Utilize extension() instead of `haveSupMode()` * Utilize extension() instead of `haveNExt()` * Utilize extension() instead of `haveZkr()` * Utilize extension() instead of `haveUsrMode()` * Move comments from `have*` functions into `extension` function * Delete all unused `have*` definitions of various extensions --- model/riscv_fdext_control.sail | 6 +- model/riscv_insts_base.sail | 4 +- model/riscv_insts_dext.sail | 4 +- model/riscv_insts_fext.sail | 2 +- model/riscv_insts_next.sail | 2 +- model/riscv_insts_svinval.sail | 12 +-- model/riscv_insts_vext_vset.sail | 4 +- model/riscv_insts_zcb.sail | 48 ++++----- model/riscv_insts_zfh.sail | 2 +- model/riscv_next_control.sail | 16 +-- model/riscv_sys_control.sail | 82 +++++++------- model/riscv_sys_regs.sail | 180 +++++++++++-------------------- 12 files changed, 155 insertions(+), 207 deletions(-) diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index fd4361804..d5d3e46c1 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -17,9 +17,9 @@ /* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */ -function clause ext_is_CSR_defined (0x001, _) = extension("F") | haveZfinx() -function clause ext_is_CSR_defined (0x002, _) = extension("F") | haveZfinx() -function clause ext_is_CSR_defined (0x003, _) = extension("F") | haveZfinx() +function clause ext_is_CSR_defined (0x001, _) = extension("F") | extension("Zfinx") +function clause ext_is_CSR_defined (0x002, _) = extension("F") | extension("Zfinx") +function clause ext_is_CSR_defined (0x003, _) = extension("F") | extension("Zfinx") function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS])) function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM])) diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 3b833c04f..c34fc0432 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -662,8 +662,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_dext.sail b/model/riscv_insts_dext.sail index 4a43a5def..dc8120c28 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -224,13 +224,13 @@ function fle_D (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveDoubleFPU() -> bool = extension("D") | haveZdinx() +function haveDoubleFPU() -> bool = extension("D") | extension("Zdinx") /* RV32Zdinx requires even register pairs; can be omitted for code */ /* not used for RV32Zdinx (i.e. RV64-only or D-only). */ val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, dec, regidx)) -> bool function validDoubleRegs(n, regs) = { - if haveZdinx() & sizeof(xlen) == 32 then + if extension("Zdinx") & sizeof(xlen) == 32 then foreach (i from 0 to (n - 1)) if (regs[i][0] == bitone) then return false; true diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index a68e111c7..834aee7bb 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -259,7 +259,7 @@ function fle_S (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveSingleFPU() -> bool = extension("F") | haveZfinx() +function haveSingleFPU() -> bool = extension("F") | extension("Zfinx") /* ****************************************************************** */ /* Floating-point loads */ diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail index dd9197adb..2864081e9 100644 --- a/model/riscv_insts_next.sail +++ b/model/riscv_insts_next.sail @@ -15,7 +15,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_insts_svinval.sail b/model/riscv_insts_svinval.sail index 168fb17ff..66eaafe2e 100644 --- a/model/riscv_insts_svinval.sail +++ b/model/riscv_insts_svinval.sail @@ -9,8 +9,8 @@ union clause ast = SINVAL_VMA : (regidx, regidx) mapping clause encdec = - SINVAL_VMA(rs1, rs2) if haveSvinval() - <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + SINVAL_VMA(rs1, rs2) if extension("Svinval") + <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval") function clause execute SINVAL_VMA(rs1, rs2) = { execute(SFENCE_VMA(rs1, rs2)) @@ -24,8 +24,8 @@ mapping clause assembly = SINVAL_VMA(rs1, rs2) union clause ast = SFENCE_W_INVAL : unit mapping clause encdec = - SFENCE_W_INVAL() if haveSvinval() - <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + SFENCE_W_INVAL() if extension("Svinval") + <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval") function clause execute SFENCE_W_INVAL() = { if cur_privilege == User @@ -40,8 +40,8 @@ mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval" union clause ast = SFENCE_INVAL_IR : unit mapping clause encdec = - SFENCE_INVAL_IR() if haveSvinval() - <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval() + SFENCE_INVAL_IR() if extension("Svinval") + <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval") function clause execute SFENCE_INVAL_IR() = { if cur_privilege == User diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 035f91361..236d1d062 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -167,8 +167,8 @@ mapping clause assembly = VSETVL(rs2, rs1, rd) /* ********************************** vsetivli *********************************** */ union clause ast = VSETIVLI : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx) -mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if haveVExt() - <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt() +mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extension("V") + <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if extension("V") function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vtype */ diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail index 86253bff4..0fac41077 100644 --- a/model/riscv_insts_zcb.sail +++ b/model/riscv_insts_zcb.sail @@ -9,8 +9,8 @@ union clause ast = C_LBU : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_LBU(uimm1 @ uimm0, rdc, rs1c) if haveZcb() - <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb() + C_LBU(uimm1 @ uimm0, rdc, rs1c) if extension("Zcb") + <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb") mapping clause assembly = C_LBU(uimm, rdc, rs1c) <-> "c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -27,8 +27,8 @@ function clause execute C_LBU(uimm, rdc, rs1c) = { union clause ast = C_LHU : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_LHU(uimm1 @ 0b0, rdc, rs1c) if haveZcb() - <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb() + C_LHU(uimm1 @ 0b0, rdc, rs1c) if extension("Zcb") + <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb") mapping clause assembly = C_LHU(uimm, rdc, rs1c) <-> "c.lhu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -45,8 +45,8 @@ function clause execute C_LHU(uimm, rdc, rs1c) = { union clause ast = C_LH : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_LH(uimm1 @ 0b0, rdc, rs1c) if haveZcb() - <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb() + C_LH(uimm1 @ 0b0, rdc, rs1c) if extension("Zcb") + <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb") mapping clause assembly = C_LH(uimm, rdc, rs1c) <-> "c.lh" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -63,8 +63,8 @@ function clause execute C_LH(uimm, rdc, rs1c) = { union clause ast = C_SB : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_SB(uimm1 @ uimm0, rs1c, rs2c) if haveZcb() - <-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if haveZcb() + C_SB(uimm1 @ uimm0, rs1c, rs2c) if extension("Zcb") + <-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if extension("Zcb") mapping clause assembly = C_SB(uimm, rs1c, rs2c) <-> "c.sb" ^ spc() ^ creg_name(rs2c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")" @@ -81,8 +81,8 @@ function clause execute C_SB(uimm, rs1c, rs2c) = { union clause ast = C_SH : (bits(2), cregidx, cregidx) mapping clause encdec_compressed = - C_SH(uimm1 @ 0b0, rs1c, rs2c) if haveZcb() - <-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if haveZcb() + C_SH(uimm1 @ 0b0, rs1c, rs2c) if extension("Zcb") + <-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if extension("Zcb") mapping clause assembly = C_SH(uimm, rs1c, rs2c) <-> "c.sh" ^ spc() ^ creg_name(rs1c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs2c) ^ opt_spc() ^ ")" @@ -99,8 +99,8 @@ function clause execute C_SH(uimm, rs1c, rs2c) = { union clause ast = C_ZEXT_B : (cregidx) mapping clause encdec_compressed = - C_ZEXT_B(rsdc) if haveZcb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if haveZcb() + C_ZEXT_B(rsdc) if extension("Zcb") + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if extension("Zcb") mapping clause assembly = C_ZEXT_B(rsdc) <-> "c.zext.b" ^ spc() ^ creg_name(rsdc) @@ -116,8 +116,8 @@ function clause execute C_ZEXT_B(rsdc) = { union clause ast = C_SEXT_B : (cregidx) mapping clause encdec_compressed = - C_SEXT_B(rsdc) if haveZcb() & haveZbb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if haveZcb() & haveZbb() + C_SEXT_B(rsdc) if extension("Zcb") & extension("Zbb") + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if extension("Zcb") & extension("Zbb") mapping clause assembly = C_SEXT_B(rsdc) <-> "c.sext.b" ^ spc() ^ creg_name(rsdc) @@ -132,8 +132,8 @@ function clause execute C_SEXT_B(rsdc) = { union clause ast = C_ZEXT_H : (cregidx) mapping clause encdec_compressed = - C_ZEXT_H(rsdc) if haveZcb() & haveZbb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if haveZcb() & haveZbb() + C_ZEXT_H(rsdc) if extension("Zcb") & extension("Zbb") + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if extension("Zcb") & extension("Zbb") mapping clause assembly = C_ZEXT_H(rsdc) <-> "c.zext.h" ^ spc() ^ creg_name(rsdc) @@ -148,8 +148,8 @@ function clause execute C_ZEXT_H(rsdc) = { union clause ast = C_SEXT_H : (cregidx) mapping clause encdec_compressed = - C_SEXT_H(rsdc) if haveZcb() & haveZbb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if haveZcb() & haveZbb() + C_SEXT_H(rsdc) if extension("Zcb") & extension("Zbb") + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if extension("Zcb") & extension("Zbb") mapping clause assembly = C_SEXT_H(rsdc) <-> "c.sext.h" ^ spc() ^ creg_name(rsdc) @@ -164,8 +164,8 @@ function clause execute C_SEXT_H(rsdc) = { union clause ast = C_ZEXT_W : (cregidx) mapping clause encdec_compressed = - C_ZEXT_W(rsdc) if haveZcb() & haveZba() & sizeof(xlen) == 64 - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if haveZcb() & haveZba() & sizeof(xlen) == 64 + C_ZEXT_W(rsdc) if extension("Zcb") & extension("Zba") & sizeof(xlen) == 64 + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if extension("Zcb") & extension("Zba") & sizeof(xlen) == 64 mapping clause assembly = C_ZEXT_W(rsdc) <-> "c.zext.w" ^ spc() ^ creg_name(rsdc) @@ -180,8 +180,8 @@ function clause execute C_ZEXT_W(rsdc) = { union clause ast = C_NOT : (cregidx) mapping clause encdec_compressed = - C_NOT(rsdc) if haveZcb() - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if haveZcb() + C_NOT(rsdc) if extension("Zcb") + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if extension("Zcb") mapping clause assembly = C_NOT(rsdc) <-> "c.not" ^ spc() ^ creg_name(rsdc) @@ -197,8 +197,8 @@ function clause execute C_NOT(rsdc) = { union clause ast = C_MUL : (cregidx, cregidx) mapping clause encdec_compressed = - C_MUL(rsdc, rs2c) if haveZcb() & (haveMulDiv() | haveZmmul()) - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (haveMulDiv() | haveZmmul()) + C_MUL(rsdc, rs2c) if extension("Zcb") & (extension("M") | extension("Zmmul")) + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if extension("Zcb") & (extension("M") | extension("Zmmul")) mapping clause assembly = C_MUL(rsdc, rs2c) <-> "c.mul" ^ spc() ^ creg_name(rsdc) ^ sep() ^ creg_name(rs2c) diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 6d3078556..840e7619b 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -162,7 +162,7 @@ function fle_H (v1, v2, is_quiet) = { /* **************************************************************** */ /* Helper functions for 'encdec()' */ -function haveHalfFPU() -> bool = extension("Zfh") | haveZhinx() +function haveHalfFPU() -> bool = extension("Zfh") | extension("Zhinx") /* ****************************************************************** */ /* Floating-point loads */ diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 688d16d72..263850206 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -8,14 +8,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 95ed4d6a5..0f3058b9d 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -25,14 +25,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 @@ -59,35 +59,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) @@ -107,9 +107,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 @@ -168,11 +168,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) @@ -228,7 +228,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 { @@ -237,13 +237,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 { @@ -267,7 +267,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) { @@ -346,7 +346,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); @@ -371,7 +371,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); @@ -408,7 +408,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 df298a206..e259cca5c 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -125,60 +125,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 - -/* - * Illegal values legalized to least privileged mode supported. - * Note: the only valid combinations of supported modes are M, M+U, M+S+U. - */ -function lowest_supported_privLevel() -> Privilege = - if haveUsrMode() then User else Machine - -function have_privLevel(priv : priv_level) -> bool = - match priv { - 0b00 => haveUsrMode(), - 0b01 => haveSupMode(), - 0b10 => false, - 0b11 => true, - } - bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -223,6 +169,64 @@ bitfield Mstatus : xlenbits = { } register mstatus : 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, + "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, + "Svinval" => sys_enable_svinval(), + "V" => (misa[V] == 0b1) & (mstatus[VS] != 0b00), + "Zaamo" => extension("A"), + "Zalrsc" => extension("A"), + "Zba" => true, + "Zbb" => true, + "Zbc" => true, + "Zbkb" => true, + "Zbkc" => true, + "Zbkx" => true, + "Zbs" => true, + "Zcb" => sys_enable_zcb(), + "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 + } +} + +/* + * Illegal values legalized to least privileged mode supported. + * Note: the only valid combinations of supported modes are M, M+U, M+S+U. + */ +function lowest_supported_privLevel() -> Privilege = + if extension("U") then User else Machine + +function have_privLevel(priv : priv_level) -> bool = + match priv { + 0b00 => extension("U"), + 0b01 => extension("S"), + 0b10 => false, + 0b11 => true, + } + function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : Privilege) -> Privilege = if t != Execute() & m[MPRV] == 0b1 then privLevel_of_bits(m[MPP]) @@ -293,13 +297,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 = [m with UPIE = 0b0]; let m = [m with UIE = 0b0]; m } else m; - if not(haveUsrMode()) then { + if not(extension("U")) then { let m = [m with MPRV = 0b0]; m } else m @@ -324,24 +328,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) & sizeof(flen) >= 64 -/* 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) - -function haveSvinval() -> bool = sys_enable_svinval() - -/* Zcb has simple code-size saving instructions. (The Zcb extension depends on the Zca extension.) */ -function haveZcb() -> bool = sys_enable_zcb() - -/* 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 = { @@ -366,7 +352,7 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { * extension, the U-mode bits. */ let v = Mk_Minterrupts(v); let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]; - if haveUsrMode() & haveNExt() then { + if extension("U") & extension("N") then { [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } @@ -382,7 +368,7 @@ function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { SSI = 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 { [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m } @@ -670,7 +656,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 [m with SSI = s[SSI]] else m; - if haveNExt() then { + if extension("N") then { let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; m @@ -687,7 +673,7 @@ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru let m = if d[SEI] == 0b1 then [m with SEI = s[SEI]] else m; let m = if d[STI] == 0b1 then [m with STI = s[STI]] else m; let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; - if haveNExt() then { + if extension("N") then { let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; let m = if d[UTI] == 0b1 then [m with UTI = s[UTI]] else m; let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; @@ -938,41 +924,3 @@ function get_vtype_vma() = decode_agtype(vtype[vma]) val get_vtype_vta : unit -> agtype 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), - "Zaamo" => haveAtomics(), - "Zalrsc" => haveAtomics(), - "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 - } -}