Make use of extensionEnabled() instead of have*()

* Utilize extensionEnabled() instead of `haveZmmul()`, `haveUsrMode()`, `haveSupMode()`, `haveNExt()`, etc.. * Delete all unused `have*` definitions of various extensions
riscv · Jul 12, 2024 · d8ea69e · d8ea69e
1 parent d9e14d3
commit d8ea69e
Show file tree

Hide file tree

Showing 21 changed files with 385 additions and 374 deletions.
diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
@@ -21,11 +21,14 @@ function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b0
 enum clause extension = Ext_D
 function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64
 
+enum clause extension = Ext_Zfinx
+function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx()
+
 /* val clause ext_is_CSR_defined : (csreg) -> bool */
 
-function clause ext_is_CSR_defined (0x001) = extensionEnabled(Ext_F) | haveZfinx()
-function clause ext_is_CSR_defined (0x002) = extensionEnabled(Ext_F) | haveZfinx()
-function clause ext_is_CSR_defined (0x003) = extensionEnabled(Ext_F) | haveZfinx()
+function clause ext_is_CSR_defined (0x001) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
+function clause ext_is_CSR_defined (0x002) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
+function clause ext_is_CSR_defined (0x003) = extensionEnabled(Ext_F) | extensionEnabled(Ext_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
@@ -664,8 +664,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(extensionEnabled(Ext_S)) | mstatus[TSR] == 0b1,
+ Machine => not(extensionEnabled(Ext_S))
  };
  if sret_illegal
  then { handle_illegal(); RETIRE_FAIL }

diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
@@ -224,13 +224,16 @@ function fle_D (v1, v2, is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()' */
 
-function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | haveZdinx()
+enum clause extension = Ext_Zdinx
+function clause extensionEnabled(Ext_Zdinx) = sys_enable_zfinx() & sizeof(flen) >= 64
+
+function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | extensionEnabled(Ext_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 extensionEnabled(Ext_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
@@ -262,7 +262,7 @@ function fle_S (v1, v2, is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()' */
 
-function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | haveZfinx()
+function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
 
 /* ****************************************************************** */
 /* Floating-point loads */

diff --git 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(extensionEnabled(Ext_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
@@ -6,11 +6,14 @@
 /* SPDX-License-Identifier: BSD-2-Clause */
 /*=======================================================================================*/
 
+enum clause extension = Ext_Svinval
+function clause extensionEnabled(Ext_Svinval) = sys_enable_svinval()
+
 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 extensionEnabled(Ext_Svinval)
+ <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)
 
 function clause execute SINVAL_VMA(rs1, rs2) = {
  execute(SFENCE_VMA(rs1, rs2))
@@ -24,8 +27,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 extensionEnabled(Ext_Svinval)
+ <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)
 
 function clause execute SFENCE_W_INVAL() = {
  if cur_privilege == User
@@ -40,8 +43,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 extensionEnabled(Ext_Svinval)
+ <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)
 
 function clause execute SFENCE_INVAL_IR() = {
  if cur_privilege == User