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
ThinkOpenly · Jul 3, 2024 · f492251 · f492251
1 parent 207b864
commit f492251
Show file tree

Hide file tree

Showing 12 changed files with 155 additions and 207 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)