diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
index d7e62f711..fa411bac0 100644
--- 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, Privilege) -> 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
index 95d3f785f..599c0a7a4 100644
--- 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
index 3b2c34d96..f366c487a 100644
--- 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
index cff9d938a..3a5509ea4 100644
--- 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
index dd9197adb..52d8bc26d 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(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
index 168fb17ff..2816fdc14 100644
--- 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
diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail
index 6104e7ee4..b351b01bb 100644
--- a/model/riscv_insts_vext_arith.sail
+++ b/model/riscv_insts_vext_arith.sail
@@ -40,8 +40,8 @@ mapping encdec_vvfunct6 : vvfunct6 <-> bits(6) = {
   VV_VSSRA         <-> 0b101011
 }
 
-mapping clause encdec = VVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_vvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW_pow  = get_sew_pow();
@@ -174,8 +174,8 @@ mapping encdec_nvsfunct6 : nvsfunct6 <-> bits(6) = {
   NVS_VNSRA       <-> 0b101101
 }
 
-mapping clause encdec = NVSTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_nvsfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = NVSTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_nvsfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -241,8 +241,8 @@ mapping encdec_nvfunct6 : nvfunct6 <-> bits(6) = {
   NV_VNCLIP      <-> 0b101111
 }
 
-mapping clause encdec = NVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_nvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = NVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_nvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -303,8 +303,8 @@ mapping clause assembly = NVTYPE(funct6, vm, vs2, vs1, vd)
 /* ********************** OPIVV (Integer Merge Instruction) ********************** */
 union clause ast = MASKTYPEV : (regidx, regidx, regidx)
 
-mapping clause encdec = MASKTYPEV (vs2, vs1,  vd) if haveVExt()
-  <-> 0b010111 @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MASKTYPEV (vs2, vs1,  vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MASKTYPEV(vs2, vs1, vd)) = {
   let start_element = get_start_element();
@@ -351,8 +351,8 @@ mapping clause assembly = MASKTYPEV(vs2, vs1, vd)
 /* ********************** OPIVV (Integer Move Instruction) *********************** */
 union clause ast = MOVETYPEV : (regidx, regidx)
 
-mapping clause encdec = MOVETYPEV (vs1, vd) if haveVExt()
-  <-> 0b010111 @ 0b1 @ 0b00000 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MOVETYPEV (vs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b1 @ 0b00000 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MOVETYPEV(vs1, vd)) = {
   let SEW      = get_sew();
@@ -410,8 +410,8 @@ mapping encdec_vxfunct6 : vxfunct6 <-> bits(6) = {
   VX_VSSRA      <-> 0b101011
 }
 
-mapping clause encdec = VXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_vxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -526,8 +526,8 @@ mapping encdec_nxsfunct6 : nxsfunct6 <-> bits(6) = {
   NXS_VNSRA       <-> 0b101101
 }
 
-mapping clause encdec = NXSTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_nxsfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = NXSTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_nxsfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -593,8 +593,8 @@ mapping encdec_nxfunct6 : nxfunct6 <-> bits(6) = {
   NX_VNCLIP      <-> 0b101111
 }
 
-mapping clause encdec = NXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_nxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = NXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_nxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -662,8 +662,8 @@ mapping encdec_vxsgfunct6 : vxsgfunct6 <-> bits(6) = {
   VX_VRGATHER     <-> 0b001100
 }
 
-mapping clause encdec = VXSG(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_vxsgfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VXSG(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vxsgfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = {
   let SEW_pow  = get_sew_pow();
@@ -725,8 +725,8 @@ mapping clause assembly = VXSG(funct6, vm, vs2, rs1, vd)
 /* ********************** OPIVX (Integer Merge Instruction) ********************** */
 union clause ast = MASKTYPEX : (regidx, regidx, regidx)
 
-mapping clause encdec = MASKTYPEX(vs2, rs1, vd) if haveVExt()
-  <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MASKTYPEX(vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MASKTYPEX(vs2, rs1, vd)) = {
   let start_element = get_start_element();
@@ -773,8 +773,8 @@ mapping clause assembly = MASKTYPEX(vs2, rs1, vd)
 /* ********************** OPIVX (Integer Move Instruction) *********************** */
 union clause ast = MOVETYPEX : (regidx, regidx)
 
-mapping clause encdec = MOVETYPEX (rs1, vd) if haveVExt()
-  <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MOVETYPEX (rs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MOVETYPEX(rs1, vd)) = {
   let SEW      = get_sew();
@@ -824,8 +824,8 @@ mapping encdec_vifunct6 : vifunct6 <-> bits(6) = {
   VI_VSSRA      <-> 0b101011
 }
 
-mapping clause encdec = VITYPE(funct6, vm, vs2, simm, vd) if haveVExt()
-  <-> encdec_vifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VITYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = {
   let SEW      = get_sew();
@@ -916,8 +916,8 @@ mapping encdec_nisfunct6 : nisfunct6 <-> bits(6) = {
   NIS_VNSRA       <-> 0b101101
 }
 
-mapping clause encdec = NISTYPE(funct6, vm, vs2, simm, vd) if haveVExt()
-  <-> encdec_nisfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = NISTYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_nisfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = {
   let SEW      = get_sew();
@@ -983,8 +983,8 @@ mapping encdec_nifunct6 : nifunct6 <-> bits(6) = {
   NI_VNCLIP      <-> 0b101111
 }
 
-mapping clause encdec = NITYPE(funct6, vm, vs2, simm, vd) if haveVExt()
-  <-> encdec_nifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = NITYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_nifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = {
   let SEW      = get_sew();
@@ -1052,8 +1052,8 @@ mapping encdec_visgfunct6 : visgfunct6 <-> bits(6) = {
   VI_VRGATHER     <-> 0b001100
 }
 
-mapping clause encdec = VISG(funct6, vm, vs2, simm, vd) if haveVExt()
-  <-> encdec_visgfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VISG(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_visgfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VISG(funct6, vm, vs2, simm, vd)) = {
   let SEW_pow  = get_sew_pow();
@@ -1115,8 +1115,8 @@ mapping clause assembly = VISG(funct6, vm, vs2, simm, vd)
 /* ********************** OPIVI (Integer Merge Instruction) ********************** */
 union clause ast = MASKTYPEI : (regidx, bits(5), regidx)
 
-mapping clause encdec = MASKTYPEI(vs2, simm, vd) if haveVExt()
-  <-> 0b010111 @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MASKTYPEI(vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MASKTYPEI(vs2, simm, vd)) = {
   let start_element = get_start_element();
@@ -1163,8 +1163,8 @@ mapping clause assembly = MASKTYPEI(vs2, simm, vd)
 /* ********************** OPIVI (Integer Move Instruction) *********************** */
 union clause ast = MOVETYPEI : (regidx, bits(5))
 
-mapping clause encdec = MOVETYPEI (vd, simm) if haveVExt()
-  <-> 0b010111 @ 0b1 @ 0b00000 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MOVETYPEI (vd, simm) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b1 @ 0b00000 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MOVETYPEI(vd, simm)) = {
   let SEW      = get_sew();
@@ -1199,8 +1199,8 @@ mapping clause assembly = MOVETYPEI(vd, simm)
 /* ********************* OPIVI (Whole Vector Register Move) ********************** */
 union clause ast = VMVRTYPE : (regidx, bits(5), regidx)
 
-mapping clause encdec = VMVRTYPE(vs2, simm, vd) if haveVExt()
-  <-> 0b100111 @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VMVRTYPE(vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> 0b100111 @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VMVRTYPE(vs2, simm, vd)) = {
   let start_element = get_start_element();
@@ -1257,8 +1257,8 @@ mapping encdec_mvvfunct6 : mvvfunct6 <-> bits(6) = {
   MVV_VREM        <-> 0b100011
 }
 
-mapping clause encdec = MVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_mvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_mvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -1366,8 +1366,8 @@ mapping encdec_mvvmafunct6 : mvvmafunct6 <-> bits(6) = {
   MVV_VNMSUB      <-> 0b101011
 }
 
-mapping clause encdec = MVVMATYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_mvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MVVMATYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_mvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -1426,8 +1426,8 @@ mapping encdec_wvvfunct6 : wvvfunct6 <-> bits(6) = {
   WVV_VWMULSU    <-> 0b111010
 }
 
-mapping clause encdec = WVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_wvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = WVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_wvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -1496,8 +1496,8 @@ mapping encdec_wvfunct6 : wvfunct6 <-> bits(6) = {
   WV_VSUBU      <-> 0b110110
 }
 
-mapping clause encdec = WVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_wvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = WVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_wvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -1559,8 +1559,8 @@ mapping encdec_wmvvfunct6 : wmvvfunct6 <-> bits(6) = {
   WMVV_VWMACCSU  <-> 0b111111
 }
 
-mapping clause encdec =  WMVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_wmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec =  WMVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_wmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -1620,8 +1620,8 @@ mapping vext2_vs1 : vext2funct6 <-> bits(5) = {
   VEXT2_SVF2  <-> 0b00111
 }
 
-mapping clause encdec = VEXT2TYPE(funct6, vm, vs2, vd) if haveVExt()
-  <-> 0b010010 @ vm @ vs2 @ vext2_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VEXT2TYPE(funct6, vm, vs2, vd) if extensionEnabled(Ext_V)
+  <-> 0b010010 @ vm @ vs2 @ vext2_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = {
   let SEW = get_sew();
@@ -1678,8 +1678,8 @@ mapping vext4_vs1 : vext4funct6 <-> bits(5) = {
   VEXT4_SVF4  <-> 0b00101
 }
 
-mapping clause encdec = VEXT4TYPE(funct6, vm, vs2, vd) if haveVExt()
-  <-> 0b010010 @ vm @ vs2 @ vext4_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VEXT4TYPE(funct6, vm, vs2, vd) if extensionEnabled(Ext_V)
+  <-> 0b010010 @ vm @ vs2 @ vext4_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = {
   let SEW = get_sew();
@@ -1736,8 +1736,8 @@ mapping vext8_vs1 : vext8funct6 <-> bits(5) = {
   VEXT8_SVF8  <-> 0b00011
 }
 
-mapping clause encdec = VEXT8TYPE(funct6, vm, vs2, vd) if haveVExt()
-  <-> 0b010010 @ vm @ vs2 @ vext8_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VEXT8TYPE(funct6, vm, vs2, vd) if extensionEnabled(Ext_V)
+  <-> 0b010010 @ vm @ vs2 @ vext8_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = {
   let SEW = get_sew();
@@ -1788,8 +1788,8 @@ mapping clause assembly = VEXT8TYPE(funct6, vm, vs2, vd)
 /* ************************ OPMVV (vmv.x.s in VWXUNARY0) ************************* */
 union clause ast = VMVXS : (regidx, regidx)
 
-mapping clause encdec = VMVXS(vs2, rd) if haveVExt()
-  <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b010 @ rd @ 0b1010111 if haveVExt()
+mapping clause encdec = VMVXS(vs2, rd) if extensionEnabled(Ext_V)
+  <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b010 @ rd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VMVXS(vs2, rd)) = {
   let SEW      = get_sew();
@@ -1816,8 +1816,8 @@ mapping clause assembly = VMVXS(vs2, rd)
 /* ********************* OPMVV (Vector Compress Instruction) ********************* */
 union clause ast = MVVCOMPRESS : (regidx, regidx, regidx)
 
-mapping clause encdec = MVVCOMPRESS(vs2, vs1, vd) if haveVExt()
-  <-> 0b010111 @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MVVCOMPRESS(vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = {
   let start_element = get_start_element();
@@ -1890,8 +1890,8 @@ mapping encdec_mvxfunct6 : mvxfunct6 <-> bits(6) = {
   MVX_VREM          <-> 0b100011
 }
 
-mapping clause encdec = MVXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_mvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MVXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_mvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -2010,8 +2010,8 @@ mapping encdec_mvxmafunct6 : mvxmafunct6 <-> bits(6) = {
   MVX_VNMSUB        <-> 0b101011
 }
 
-mapping clause encdec = MVXMATYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_mvxmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MVXMATYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_mvxmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -2071,8 +2071,8 @@ mapping encdec_wvxfunct6 : wvxfunct6 <-> bits(6) = {
   WVX_VWMULSU    <-> 0b111010
 }
 
-mapping clause encdec = WVXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_wvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = WVXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_wvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -2140,8 +2140,8 @@ mapping encdec_wxfunct6 : wxfunct6 <-> bits(6) = {
   WX_VSUBU      <-> 0b110110
 }
 
-mapping clause encdec = WXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_wxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = WXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_wxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -2203,8 +2203,8 @@ mapping encdec_wmvxfunct6 : wmvxfunct6 <-> bits(6) = {
   WMVX_VWMACCSU   <-> 0b111111
 }
 
-mapping clause encdec = WMVXTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_wmvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = WMVXTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_wmvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -2259,8 +2259,8 @@ mapping clause assembly = WMVXTYPE(funct6, vm, vs2, rs1, vd)
 /* ****************************** OPMVX (VRXUNARY0) ****************************** */
 union clause ast = VMVSX : (regidx, regidx)
 
-mapping clause encdec = VMVSX(rs1, vd) if haveVExt()
-  <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b110 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VMVSX(rs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b110 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VMVSX(rs1, vd)) = {
   let SEW      = get_sew();
diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail
index 0b36b01b6..945199da8 100755
--- a/model/riscv_insts_vext_fp.sail
+++ b/model/riscv_insts_vext_fp.sail
@@ -27,8 +27,8 @@ mapping encdec_fvvfunct6 : fvvfunct6 <-> bits(6) = {
   FVV_VMUL       <-> 0b100100
 }
 
-mapping clause encdec = FVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_fvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -102,8 +102,8 @@ mapping encdec_fvvmafunct6 : fvvmafunct6 <-> bits(6) = {
   FVV_VNMSAC     <-> 0b101111
 }
 
-mapping clause encdec = FVVMATYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_fvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FVVMATYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -169,8 +169,8 @@ mapping encdec_fwvvfunct6 : fwvvfunct6 <-> bits(6) = {
   FWVV_VMUL       <-> 0b111000
 }
 
-mapping clause encdec = FWVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_fwvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FWVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fwvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -234,8 +234,8 @@ mapping encdec_fwvvmafunct6 : fwvvmafunct6 <-> bits(6) = {
   FWVV_VNMSAC     <-> 0b111111
 }
 
-mapping clause encdec = FWVVMATYPE(funct6, vm, vs1, vs2, vd) if haveVExt()
-  <-> encdec_fwvvmafunct6(funct6) @ vm @ vs1 @ vs2 @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FWVVMATYPE(funct6, vm, vs1, vs2, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fwvvmafunct6(funct6) @ vm @ vs1 @ vs2 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -298,8 +298,8 @@ mapping encdec_fwvfunct6 : fwvfunct6 <-> bits(6) = {
   FWV_VSUB       <-> 0b110110
 }
 
-mapping clause encdec = FWVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_fwvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FWVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fwvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -361,8 +361,8 @@ mapping encdec_vfunary0_vs1 : vfunary0 <-> bits(5) = {
   FV_CVT_RTZ_X_F    <-> 0b00111
 }
 
-mapping clause encdec = VFUNARY0(vm, vs2, vfunary0, vd) if haveVExt()
-  <-> 0b010010 @ vm @ vs2 @ encdec_vfunary0_vs1(vfunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFUNARY0(vm, vs2, vfunary0, vd) if extensionEnabled(Ext_V)
+  <-> 0b010010 @ vm @ vs2 @ encdec_vfunary0_vs1(vfunary0) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -475,8 +475,8 @@ mapping encdec_vfwunary0_vs1 : vfwunary0 <-> bits(5) = {
   FWV_CVT_RTZ_X_F   <-> 0b01111
 }
 
-mapping clause encdec = VFWUNARY0(vm, vs2, vfwunary0, vd) if haveVExt()
-  <-> 0b010010 @ vm @ vs2 @ encdec_vfwunary0_vs1(vfwunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFWUNARY0(vm, vs2, vfwunary0, vd) if extensionEnabled(Ext_V)
+  <-> 0b010010 @ vm @ vs2 @ encdec_vfwunary0_vs1(vfwunary0) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -605,8 +605,8 @@ mapping encdec_vfnunary0_vs1 : vfnunary0 <-> bits(5) = {
   FNV_CVT_RTZ_X_F   <-> 0b10111
 }
 
-mapping clause encdec = VFNUNARY0(vm, vs2, vfnunary0, vd) if haveVExt()
-  <-> 0b010010 @ vm @ vs2 @ encdec_vfnunary0_vs1(vfnunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFNUNARY0(vm, vs2, vfnunary0, vd) if extensionEnabled(Ext_V)
+  <-> 0b010010 @ vm @ vs2 @ encdec_vfnunary0_vs1(vfnunary0) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -741,8 +741,8 @@ mapping encdec_vfunary1_vs1 : vfunary1 <-> bits(5) = {
   FVV_VCLASS      <-> 0b10000
 }
 
-mapping clause encdec = VFUNARY1(vm, vs2, vfunary1, vd) if haveVExt()
-  <-> 0b010011 @ vm @ vs2 @ encdec_vfunary1_vs1(vfunary1) @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFUNARY1(vm, vs2, vfunary1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010011 @ vm @ vs2 @ encdec_vfunary1_vs1(vfunary1) @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -817,8 +817,8 @@ mapping clause assembly = VFUNARY1(vm, vs2, vfunary1, vd)
 /* ****************************** OPFVV (VWFUNARY0) ****************************** */
 union clause ast = VFMVFS : (regidx, regidx)
 
-mapping clause encdec = VFMVFS(vs2, rd) if haveVExt()
-  <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b001 @ rd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFMVFS(vs2, rd) if extensionEnabled(Ext_V)
+  <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b001 @ rd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFMVFS(vs2, rd)) = {
   let rm_3b    = fcsr[FRM];
@@ -865,8 +865,8 @@ mapping encdec_fvffunct6 : fvffunct6 <-> bits(6) = {
   VF_VRSUB         <-> 0b100111
 }
 
-mapping clause encdec = FVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_fvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FVFTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -955,8 +955,8 @@ mapping encdec_fvfmafunct6 : fvfmafunct6 <-> bits(6) = {
   VF_VNMSAC     <-> 0b101111
 }
 
-mapping clause encdec = FVFMATYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_fvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FVFMATYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -1022,8 +1022,8 @@ mapping encdec_fwvffunct6 : fwvffunct6 <-> bits(6) = {
   FWVF_VMUL       <-> 0b111000
 }
 
-mapping clause encdec = FWVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_fwvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FWVFTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fwvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -1086,8 +1086,8 @@ mapping encdec_fwvfmafunct6 : fwvfmafunct6 <-> bits(6) = {
   FWVF_VNMSAC     <-> 0b111111
 }
 
-mapping clause encdec = FWVFMATYPE(funct6, vm, rs1, vs2, vd) if haveVExt()
-  <-> encdec_fwvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FWVFMATYPE(funct6, vm, rs1, vs2, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fwvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -1149,8 +1149,8 @@ mapping encdec_fwffunct6 : fwffunct6 <-> bits(6) = {
   FWF_VSUB       <-> 0b110110
 }
 
-mapping clause encdec = FWFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_fwffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FWFTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fwffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -1203,8 +1203,8 @@ mapping clause assembly = FWFTYPE(funct6, vm, vs2, rs1, vd)
 /* This instruction operates on all body elements regardless of mask value */
 union clause ast = VFMERGE : (regidx, regidx, regidx)
 
-mapping clause encdec = VFMERGE(vs2, rs1, vd) if haveVExt()
-  <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFMERGE(vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFMERGE(vs2, rs1, vd)) = {
   let rm_3b         = fcsr[FRM];
@@ -1254,8 +1254,8 @@ mapping clause assembly = VFMERGE(vs2, rs1, vd)
 /* This instruction shares the encoding with vfmerge.vfm, but with vm=1 and vs2=v0 */
 union clause ast = VFMV : (regidx, regidx)
 
-mapping clause encdec = VFMV(rs1, vd) if haveVExt()
-  <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFMV(rs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFMV(rs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -1292,8 +1292,8 @@ mapping clause assembly = VFMV(rs1, vd)
 /* ****************************** OPFVF (VRFUNARY0) ****************************** */
 union clause ast = VFMVSF : (regidx, regidx)
 
-mapping clause encdec = VFMVSF(rs1, vd) if haveVExt()
-  <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFMVSF(rs1, vd) if extensionEnabled(Ext_V)
+  <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFMVSF(rs1, vd)) = {
   let rm_3b    = fcsr[FRM];
diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail
index f04ae1acb..241e210fd 100755
--- a/model/riscv_insts_vext_mask.sail
+++ b/model/riscv_insts_vext_mask.sail
@@ -25,8 +25,8 @@ mapping encdec_mmfunct6 : mmfunct6 <-> bits(6) = {
   MM_VMXNOR    <-> 0b011111
 }
 
-mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if haveVExt()
-  <-> encdec_mmfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_mmfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -83,8 +83,8 @@ mapping clause assembly = MMTYPE(funct6, vs2, vs1, vd)
 /* ************************* OPMVV (vpopc in VWXUNARY0) ************************** */
 union clause ast = VCPOP_M : (bits(1), regidx, regidx)
 
-mapping clause encdec = VCPOP_M(vm, vs2, rd) if haveVExt()
-  <-> 0b010000 @ vm @ vs2 @ 0b10000 @ 0b010 @ rd @ 0b1010111 if haveVExt()
+mapping clause encdec = VCPOP_M(vm, vs2, rd) if extensionEnabled(Ext_V)
+  <-> 0b010000 @ vm @ vs2 @ 0b10000 @ 0b010 @ rd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VCPOP_M(vm, vs2, rd)) = {
   let SEW      = get_sew();
@@ -119,8 +119,8 @@ mapping clause assembly = VCPOP_M(vm, vs2, rd)
 /* ************************* OPMVV (vfirst in VWXUNARY0) ************************* */
 union clause ast = VFIRST_M : (bits(1), regidx, regidx)
 
-mapping clause encdec = VFIRST_M(vm, vs2, rd) if haveVExt()
-  <-> 0b010000 @ vm @ vs2 @ 0b10001 @ 0b010 @ rd @ 0b1010111 if haveVExt()
+mapping clause encdec = VFIRST_M(vm, vs2, rd) if extensionEnabled(Ext_V)
+  <-> 0b010000 @ vm @ vs2 @ 0b10001 @ 0b010 @ rd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VFIRST_M(vm, vs2, rd)) = {
   let SEW      = get_sew();
@@ -157,8 +157,8 @@ mapping clause assembly = VFIRST_M(vm, vs2, rd)
 /* ************************** OPMVV (vmsbf in VMUNARY0) ************************** */
 union clause ast = VMSBF_M : (bits(1), regidx, regidx)
 
-mapping clause encdec = VMSBF_M(vm, vs2, vd) if haveVExt()
-  <-> 0b010100 @ vm @ vs2 @ 0b00001 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VMSBF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
+  <-> 0b010100 @ vm @ vs2 @ 0b00001 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VMSBF_M(vm, vs2, vd)) = {
   let SEW      = get_sew();
@@ -198,8 +198,8 @@ mapping clause assembly = VMSBF_M(vm, vs2, vd)
 /* ************************** OPMVV (vmsif in VMUNARY0) ************************** */
 union clause ast = VMSIF_M : (bits(1), regidx, regidx)
 
-mapping clause encdec = VMSIF_M(vm, vs2, vd) if haveVExt()
-  <-> 0b010100 @ vm @ vs2 @ 0b00011 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VMSIF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
+  <-> 0b010100 @ vm @ vs2 @ 0b00011 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VMSIF_M(vm, vs2, vd)) = {
   let SEW      = get_sew();
@@ -239,8 +239,8 @@ mapping clause assembly = VMSIF_M(vm, vs2, vd)
 /* ************************** OPMVV (vmsof in VMUNARY0) ************************** */
 union clause ast = VMSOF_M : (bits(1), regidx, regidx)
 
-mapping clause encdec = VMSOF_M(vm, vs2, vd) if haveVExt()
-  <-> 0b010100 @ vm @ vs2 @ 0b00010 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VMSOF_M(vm, vs2, vd) if extensionEnabled(Ext_V)
+  <-> 0b010100 @ vm @ vs2 @ 0b00010 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VMSOF_M(vm, vs2, vd)) = {
   let SEW      = get_sew();
@@ -284,8 +284,8 @@ mapping clause assembly = VMSOF_M(vm, vs2, vd)
 /* ************************** OPMVV (viota in VMUNARY0) ************************** */
 union clause ast = VIOTA_M : (bits(1), regidx, regidx)
 
-mapping clause encdec = VIOTA_M(vm, vs2, vd) if haveVExt()
-  <-> 0b010100 @ vm @ vs2 @ 0b10000 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VIOTA_M(vm, vs2, vd) if extensionEnabled(Ext_V)
+  <-> 0b010100 @ vm @ vs2 @ 0b10000 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VIOTA_M(vm, vs2, vd)) = {
   let SEW      = get_sew();
@@ -325,8 +325,8 @@ mapping clause assembly = VIOTA_M(vm, vs2, vd)
 /* *************************** OPMVV (vid in VMUNARY0) *************************** */
 union clause ast = VID_V : (bits(1), regidx)
 
-mapping clause encdec = VID_V(vm, vd) if haveVExt()
-  <-> 0b010100 @ vm @ 0b00000 @ 0b10001 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VID_V(vm, vd) if extensionEnabled(Ext_V)
+  <-> 0b010100 @ vm @ 0b00000 @ 0b10001 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VID_V(vm, vd)) = {
   let SEW      = get_sew();
diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
index 4da82e18f..9ffb56eff 100644
--- a/model/riscv_insts_vext_mem.sail
+++ b/model/riscv_insts_vext_mem.sail
@@ -64,8 +64,8 @@ mapping vlewidth_pow : vlewidth <-> {3, 4, 5, 6} = {
 /* ******************** Vector Load Unit-Stride Normal & Segment (mop=0b00, lumop=0b00000) ********************* */
 union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx)
 
-mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if haveVExt()
-  <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt()
+mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V)
 
 val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
 function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
@@ -130,8 +130,8 @@ mapping clause assembly = VLSEGTYPE(nf, vm, rs1, width, vd)
 /* ************ Vector Load Unit-Stride Normal & Segment Fault-Only-First (mop=0b00, lumop=0b10000) ************ */
 union clause ast = VLSEGFFTYPE : (bits(3), bits(1), regidx, vlewidth, regidx)
 
-mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if haveVExt()
-  <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt()
+mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V)
 
 val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
 function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
@@ -235,8 +235,8 @@ mapping clause assembly = VLSEGFFTYPE(nf, vm, rs1, width, vd)
 /* ******************** Vector Store Unit-Stride Normal & Segment (mop=0b00, sumop=0b00000) ******************** */
 union clause ast = VSSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx)
 
-mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if haveVExt()
-  <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt()
+mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V)
 
 val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
 function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = {
@@ -304,8 +304,8 @@ mapping clause assembly = VSSEGTYPE(nf, vm, rs1, width, vs3)
 /* ****************************** Vector Load Strided Normal & Segment (mop=0b10) ****************************** */
 union clause ast = VLSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx)
 
-mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if haveVExt()
-  <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt()
+mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V)
 
 val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
 function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
@@ -371,8 +371,8 @@ mapping clause assembly = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd)
 /* ***************************** Vector Store Strided Normal & Segment (mop=0b10) ****************************** */
 union clause ast = VSSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx)
 
-mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if haveVExt()
-  <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt()
+mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V)
 
 val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
 function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
@@ -441,8 +441,8 @@ mapping clause assembly = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3)
 /* ************************* Vector Load Indexed Unordered Normal & Segment (mop=0b01) ************************* */
 union clause ast = VLUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx)
 
-mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if haveVExt()
-  <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt()
+mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V)
 
 val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
 function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
@@ -509,8 +509,8 @@ mapping clause assembly = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd)
 /* ************************** Vector Load Indexed Ordered Normal & Segment (mop=0b11) ************************** */
 union clause ast = VLOXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx)
 
-mapping clause encdec = VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd) if haveVExt()
-  <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt()
+mapping clause encdec = VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V)
 
 function clause execute(VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = {
   let EEW_index_pow = vlewidth_pow(width);
@@ -533,8 +533,8 @@ mapping clause assembly = VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd)
 /* ************************ Vector Store Indexed Unordered Normal & Segment (mop=0b01) ************************* */
 union clause ast = VSUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx)
 
-mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if haveVExt()
-  <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt()
+mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V)
 
 val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
 function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
@@ -604,8 +604,8 @@ mapping clause assembly = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3)
 /* ************************* Vector Store Indexed Ordered Normal & Segment (mop=0b11) ************************** */
 union clause ast = VSOXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, regidx)
 
-mapping clause encdec = VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if haveVExt()
-  <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if haveVExt()
+mapping clause encdec = VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V)
 
 function clause execute(VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = {
   let EEW_index_pow = vlewidth_pow(width);
@@ -628,8 +628,8 @@ mapping clause assembly = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3)
 /* ***************** Vector Load Unit-Stride Whole Register (vm=0b1, mop=0b00, lumop=0b01000) ****************** */
 union clause ast = VLRETYPE : (bits(3), regidx, vlewidth, regidx)
 
-mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if haveVExt()
-  <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if haveVExt()
+mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V)
 
 val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired
 function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
@@ -710,8 +710,8 @@ mapping clause assembly = VLRETYPE(nf, rs1, width, vd)
 /* ***************** Vector Store Unit-Stride Whole Register (vm=0b1, mop=0b00, lumop=0b01000) ***************** */
 union clause ast = VSRETYPE : (bits(3), regidx, regidx)
 
-mapping clause encdec = VSRETYPE(nf, rs1, vs3) if haveVExt()
-  <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ 0b000 @ vs3 @ 0b0100111 if haveVExt()
+mapping clause encdec = VSRETYPE(nf, rs1, vs3) if extensionEnabled(Ext_V)
+  <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ 0b000 @ vs3 @ 0b0100111 if extensionEnabled(Ext_V)
 
 val process_vsre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), int('b), regidx, regidx, int('n)) -> Retired
 function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
@@ -815,8 +815,8 @@ mapping encdec_lsop : vmlsop <-> bits(7) = {
   VSM      <-> 0b0100111
 }
 
-mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if haveVExt()
-  <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if haveVExt()
+mapping clause encdec = VMTYPE(rs1, vd_or_vs3, op) if extensionEnabled(Ext_V)
+  <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if extensionEnabled(Ext_V)
 
 val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired
 function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail
index 358836b02..1bd7657d5 100755
--- a/model/riscv_insts_vext_red.sail
+++ b/model/riscv_insts_vext_red.sail
@@ -19,8 +19,8 @@ mapping encdec_rivvfunct6 : rivvfunct6 <-> bits(6) = {
   IVV_VWREDSUM    <-> 0b110001
 }
 
-mapping clause encdec = RIVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_rivvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = RIVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_rivvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -84,8 +84,8 @@ mapping encdec_rmvvfunct6 : rmvvfunct6 <-> bits(6) = {
   MVV_VREDMAX     <-> 0b000111
 }
 
-mapping clause encdec = RMVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_rmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = RMVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_rmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -155,8 +155,8 @@ mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = {
   FVV_VFWREDUSUM  <-> 0b110001
 }
 
-mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired
 function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {
diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail
index 1f963e771..745f53e13 100755
--- a/model/riscv_insts_vext_vm.sail
+++ b/model/riscv_insts_vext_vm.sail
@@ -22,8 +22,8 @@ mapping encdec_vvmfunct6 : vvmfunct6 <-> bits(6) = {
   VVM_VMSBC    <-> 0b010011
 }
 
-mapping clause encdec = VVMTYPE(funct6, vs2, vs1, vd) if haveVExt()
-  <-> encdec_vvmfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VVMTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vvmfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -78,8 +78,8 @@ mapping encdec_vvmcfunct6 : vvmcfunct6 <-> bits(6) = {
   VVMC_VMSBC    <-> 0b010011
 }
 
-mapping clause encdec = VVMCTYPE(funct6, vs2, vs1, vd) if haveVExt()
-  <-> encdec_vvmcfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VVMCTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vvmcfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -133,8 +133,8 @@ mapping encdec_vvmsfunct6 : vvmsfunct6 <-> bits(6) = {
   VVMS_VSBC     <-> 0b010010
 }
 
-mapping clause encdec = VVMSTYPE(funct6, vs2, vs1, vd) if haveVExt()
-  <-> encdec_vvmsfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VVMSTYPE(funct6, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vvmsfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -196,8 +196,8 @@ mapping encdec_vvcmpfunct6 : vvcmpfunct6 <-> bits(6) = {
   VVCMP_VMSLE    <-> 0b011101
 }
 
-mapping clause encdec = VVCMPTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_vvcmpfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VVCMPTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vvcmpfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = {
   let SEW      = get_sew();
@@ -260,8 +260,8 @@ mapping encdec_vxmfunct6 : vxmfunct6 <-> bits(6) = {
   VXM_VMSBC    <-> 0b010011
 }
 
-mapping clause encdec = VXMTYPE(funct6, vs2, rs1, vd) if haveVExt()
-  <-> encdec_vxmfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VXMTYPE(funct6, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vxmfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -316,8 +316,8 @@ mapping encdec_vxmcfunct6 : vxmcfunct6 <-> bits(6) = {
   VXMC_VMSBC    <-> 0b010011
 }
 
-mapping clause encdec = VXMCTYPE(funct6, vs2, rs1, vd) if haveVExt()
-  <-> encdec_vxmcfunct6(funct6) @ 0b1 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VXMCTYPE(funct6, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vxmcfunct6(funct6) @ 0b1 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -371,8 +371,8 @@ mapping encdec_vxmsfunct6 : vxmsfunct6 <-> bits(6) = {
   VXMS_VSBC     <-> 0b010010
 }
 
-mapping clause encdec = VXMSTYPE(funct6, vs2, rs1, vd) if haveVExt()
-  <-> encdec_vxmsfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VXMSTYPE(funct6, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vxmsfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -436,8 +436,8 @@ mapping encdec_vxcmpfunct6 : vxcmpfunct6 <-> bits(6) = {
   VXCMP_VMSGT    <-> 0b011111
 }
 
-mapping clause encdec = VXCMPTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_vxcmpfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VXCMPTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vxcmpfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = {
   let SEW      = get_sew();
@@ -503,8 +503,8 @@ mapping encdec_vimfunct6 : vimfunct6 <-> bits(6) = {
   VIM_VMADC    <-> 0b010001 /* carry in, carry out */
 }
 
-mapping clause encdec = VIMTYPE(funct6, vs2, simm, vd) if haveVExt()
-  <-> encdec_vimfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VIMTYPE(funct6, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vimfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = {
   let SEW      = get_sew();
@@ -556,8 +556,8 @@ mapping encdec_vimcfunct6 : vimcfunct6 <-> bits(6) = {
   VIMC_VMADC    <-> 0b010001 /* carry in, carry out */
 }
 
-mapping clause encdec = VIMCTYPE(funct6, vs2, simm, vd) if haveVExt()
-  <-> encdec_vimcfunct6(funct6) @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VIMCTYPE(funct6, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vimcfunct6(funct6) @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = {
   let SEW      = get_sew();
@@ -608,8 +608,8 @@ mapping encdec_vimsfunct6 : vimsfunct6 <-> bits(6) = {
   VIMS_VADC     <-> 0b010000 /* Carry in, no carry out */
 }
 
-mapping clause encdec = VIMSTYPE(funct6, vs2, simm, vd) if haveVExt()
-  <-> encdec_vimsfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VIMSTYPE(funct6, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vimsfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = {
   let SEW      = get_sew();
@@ -669,8 +669,8 @@ mapping encdec_vicmpfunct6 : vicmpfunct6 <-> bits(6) = {
   VICMP_VMSGT    <-> 0b011111
 }
 
-mapping clause encdec = VICMPTYPE(funct6, vm, vs2, simm, vd) if haveVExt()
-  <-> encdec_vicmpfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = VICMPTYPE(funct6, vm, vs2, simm, vd) if extensionEnabled(Ext_V)
+  <-> encdec_vicmpfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = {
   let SEW      = get_sew();
@@ -733,8 +733,8 @@ mapping encdec_fvvmfunct6 : fvvmfunct6 <-> bits(6) = {
   FVVM_VMFNE      <-> 0b011100
 }
 
-mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
-  <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
   let rm_3b    = fcsr[FRM];
@@ -797,8 +797,8 @@ mapping encdec_fvfmfunct6 : fvfmfunct6 <-> bits(6) = {
   VFM_VMFGE      <-> 0b011111
 }
 
-mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
-  <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
+mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if extensionEnabled(Ext_V)
+  <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rm_3b    = fcsr[FRM];
diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
index 40a7ea9e7..16adf2806 100644
--- a/model/riscv_insts_vext_vset.sail
+++ b/model/riscv_insts_vext_vset.sail
@@ -11,6 +11,9 @@
 /* Chapter 6: Configuration-Setting Instructions                                   */
 /* ******************************************************************************* */
 
+enum clause extension = Ext_V
+function clause extensionEnabled(Ext_V) = (misa[V] == 0b1) & (mstatus[VS] != 0b00)
+
 mapping sew_flag : string <-> bits(3) = {
   "e8"    <-> 0b000,
   "e16"   <-> 0b001,
@@ -65,8 +68,8 @@ function calculate_new_vl(AVL, VLMAX) = {
 /* *********************************** vsetvli *********************************** */
 union clause ast = VSETVLI : (bits(1), bits(1), bits(3), bits(3), regidx, regidx)
 
-mapping clause encdec = VSETVLI(ma, ta, sew, lmul, rs1, rd) if haveVExt()
-  <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
+mapping clause encdec = VSETVLI(ma, ta, sew, lmul, rs1, rd) if extensionEnabled(Ext_V)
+  <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
   let LMUL_pow_ori  = get_lmul_pow();
@@ -116,8 +119,8 @@ mapping clause assembly = VSETVLI(ma, ta, sew, lmul, rs1, rd)
 /* *********************************** vsetvl ************************************ */
 union clause ast = VSETVL : (regidx, regidx, regidx)
 
-mapping clause encdec = VSETVL(rs2, rs1, rd) if haveVExt()
-  <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
+mapping clause encdec = VSETVL(rs2, rs1, rd) if extensionEnabled(Ext_V)
+  <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute VSETVL(rs2, rs1, rd) = {
   let LMUL_pow_ori  = get_lmul_pow();
@@ -167,8 +170,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 extensionEnabled(Ext_V)
+  <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if extensionEnabled(Ext_V)
 
 function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
   /* set vtype */
diff --git a/model/riscv_insts_zba.sail b/model/riscv_insts_zba.sail
index 4f078d342..21dd026f1 100644
--- a/model/riscv_insts_zba.sail
+++ b/model/riscv_insts_zba.sail
@@ -6,11 +6,17 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+enum clause extension = Ext_B
+function clause extensionEnabled(Ext_B) = misa[B] == 0b1
+
+enum clause extension = Ext_Zba
+function clause extensionEnabled(Ext_Zba) = true | extensionEnabled(Ext_B)
+
 /* ****************************************************************** */
 union clause ast = RISCV_SLLIUW : (bits(6), regidx, regidx)
 
-mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if haveZba() & sizeof(xlen) == 64
-  <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZba() & sizeof(xlen) == 64
+mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
+  <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_SLLIUW(shamt, rs1, rd)
   <-> "slli.uw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt)
@@ -25,17 +31,17 @@ function clause execute (RISCV_SLLIUW(shamt, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = ZBA_RTYPEUW : (regidx, regidx, regidx, bropw_zba)
 
-mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if haveZba() & sizeof(xlen) == 64
-  <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64
+mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
 
-mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if haveZba() & sizeof(xlen) == 64
-  <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64
+mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
 
-mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if haveZba() & sizeof(xlen) == 64
-  <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64
+mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
 
-mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if haveZba() & sizeof(xlen) == 64
-  <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if haveZba() & sizeof(xlen) == 64
+mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
 
 mapping zba_rtypeuw_mnemonic : bropw_zba <-> string = {
   RISCV_ADDUW    <-> "add.uw",
@@ -64,12 +70,12 @@ function clause execute (ZBA_RTYPEUW(rs2, rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = ZBA_RTYPE : (regidx, regidx, regidx, brop_zba)
 
-mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH1ADD) if haveZba()
-  <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZba()
-mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH2ADD) if haveZba()
-  <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZba()
-mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH3ADD) if haveZba()
-  <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZba()
+mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH1ADD) if extensionEnabled(Ext_Zba)
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if extensionEnabled(Ext_Zba)
+mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH2ADD) if extensionEnabled(Ext_Zba)
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zba)
+mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH3ADD) if extensionEnabled(Ext_Zba)
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extensionEnabled(Ext_Zba)
 
 mapping zba_rtype_mnemonic : brop_zba <-> string = {
   RISCV_SH1ADD <-> "sh1add",
diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail
index c07284811..696619dfe 100644
--- a/model/riscv_insts_zbb.sail
+++ b/model/riscv_insts_zbb.sail
@@ -6,14 +6,17 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+enum clause extension = Ext_Zbb
+function clause extensionEnabled(Ext_Zbb) = true | extensionEnabled(Ext_B)
+
 enum clause extension = Ext_Zbkb
 function clause extensionEnabled(Ext_Zbkb) = true
 
 /* ****************************************************************** */
 union clause ast = RISCV_RORIW : (bits(5), regidx, regidx)
 
-mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
-  <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+  <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_RORIW(shamt, rs1, rd)
   <-> "roriw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt)
@@ -28,8 +31,8 @@ function clause execute (RISCV_RORIW(shamt, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_RORI : (bits(6), regidx, regidx)
 
-mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
-  <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+  <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
 
 mapping clause assembly = RISCV_RORI(shamt, rs1, rd)
   <-> "rori" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt)
@@ -46,11 +49,11 @@ function clause execute (RISCV_RORI(shamt, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = ZBB_RTYPEW : (regidx, regidx, regidx, bropw_zbb)
 
-mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
 
-mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
 
 mapping zbb_rtypew_mnemonic : bropw_zbb <-> string = {
   RISCV_ROLW <-> "rolw",
@@ -74,32 +77,32 @@ function clause execute (ZBB_RTYPEW(rs2, rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = ZBB_RTYPE : (regidx, regidx, regidx, brop_zbb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if haveZbb() | extensionEnabled(Ext_Zbkb)
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb)
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb() | extensionEnabled(Ext_Zbkb)
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb)
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb() | extensionEnabled(Ext_Zbkb)
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb)
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if haveZbb()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAX) if extensionEnabled(Ext_Zbb)
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAXU) if haveZbb()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MAXU) if extensionEnabled(Ext_Zbb)
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if haveZbb()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MIN) if extensionEnabled(Ext_Zbb)
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MINU) if haveZbb()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_MINU) if extensionEnabled(Ext_Zbb)
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb() | extensionEnabled(Ext_Zbkb)
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb)
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb() | extensionEnabled(Ext_Zbkb)
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | extensionEnabled(Ext_Zbkb)
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)
 
 mapping zbb_rtype_mnemonic : brop_zbb <-> string = {
   RISCV_ANDN <-> "andn",
@@ -141,17 +144,17 @@ function clause execute (ZBB_RTYPE(rs2, rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = ZBB_EXTOP : (regidx, regidx, extop_zbb)
 
-mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTB) if haveZbb()
-  <-> 0b0110000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb()
+mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTB) if extensionEnabled(Ext_Zbb)
+  <-> 0b0110000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb)
 
-mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTH) if haveZbb()
-  <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb()
+mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTH) if extensionEnabled(Ext_Zbb)
+  <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb)
 
-mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if haveZbb() & sizeof(xlen) == 32
-  <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() & sizeof(xlen) == 32
+mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 32
+  <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 32
 
-mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
+  <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
 
 mapping zbb_extop_mnemonic : extop_zbb <-> string = {
   RISCV_SEXTB <-> "sext.b",
@@ -176,11 +179,11 @@ function clause execute (ZBB_EXTOP(rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_REV8 : (regidx, regidx)
 
-mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32
-  <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32
+mapping clause encdec = RISCV_REV8(rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32
+  <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32
 
-mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
-  <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+mapping clause encdec = RISCV_REV8(rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
+  <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_REV8(rs1, rd)
   <-> "rev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -197,8 +200,8 @@ function clause execute (RISCV_REV8(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_ORCB : (regidx, regidx)
 
-mapping clause encdec = RISCV_ORCB(rs1, rd) if haveZbb()
-  <-> 0b001010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbb()
+mapping clause encdec = RISCV_ORCB(rs1, rd) if extensionEnabled(Ext_Zbb)
+  <-> 0b001010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb)
 
 mapping clause assembly = RISCV_ORCB(rs1, rd)
   <-> "orc.b" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -217,8 +220,8 @@ function clause execute (RISCV_ORCB(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CPOP : (regidx, regidx)
 
-mapping clause encdec = RISCV_CPOP(rs1, rd) if haveZbb()
-  <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb()
+mapping clause encdec = RISCV_CPOP(rs1, rd) if extensionEnabled(Ext_Zbb)
+  <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb)
 
 mapping clause assembly = RISCV_CPOP(rs1, rd)
   <-> "cpop" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -235,8 +238,8 @@ function clause execute (RISCV_CPOP(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CPOPW : (regidx, regidx)
 
-mapping clause encdec = RISCV_CPOPW(rs1, rd) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = RISCV_CPOPW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
+  <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_CPOPW(rs1, rd)
   <-> "cpopw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -253,8 +256,8 @@ function clause execute (RISCV_CPOPW(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CLZ : (regidx, regidx)
 
-mapping clause encdec = RISCV_CLZ(rs1, rd) if haveZbb()
-  <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb()
+mapping clause encdec = RISCV_CLZ(rs1, rd) if extensionEnabled(Ext_Zbb)
+  <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb)
 
 mapping clause assembly = RISCV_CLZ(rs1, rd)
   <-> "clz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -274,8 +277,8 @@ function clause execute (RISCV_CLZ(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CLZW : (regidx, regidx)
 
-mapping clause encdec = RISCV_CLZW(rs1, rd) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = RISCV_CLZW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
+  <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_CLZW(rs1, rd)
   <-> "clzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -295,8 +298,8 @@ function clause execute (RISCV_CLZW(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CTZ : (regidx, regidx)
 
-mapping clause encdec = RISCV_CTZ(rs1, rd) if haveZbb()
-  <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbb()
+mapping clause encdec = RISCV_CTZ(rs1, rd) if extensionEnabled(Ext_Zbb)
+  <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb)
 
 mapping clause assembly = RISCV_CTZ(rs1, rd)
   <-> "ctz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -316,8 +319,8 @@ function clause execute (RISCV_CTZ(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CTZW : (regidx, regidx)
 
-mapping clause encdec = RISCV_CTZW(rs1, rd) if haveZbb() & sizeof(xlen) == 64
-  <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if haveZbb() & sizeof(xlen) == 64
+mapping clause encdec = RISCV_CTZW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
+  <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_CTZW(rs1, rd)
   <-> "ctzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail
index d3d4bc395..348b702ec 100644
--- a/model/riscv_insts_zbs.sail
+++ b/model/riscv_insts_zbs.sail
@@ -7,7 +7,7 @@
 /*=======================================================================================*/
 
 enum clause extension = Ext_Zbs
-function clause extensionEnabled(Ext_Zbs) = true | haveBExt()
+function clause extensionEnabled(Ext_Zbs) = true | extensionEnabled(Ext_B)
 
 /* ****************************************************************** */
 union clause ast = ZBS_IOP : (bits(6), regidx, regidx, biop_zbs)
diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail
index 71a6e4c46..e0e104081 100644
--- a/model/riscv_insts_zcb.sail
+++ b/model/riscv_insts_zcb.sail
@@ -6,11 +6,14 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+enum clause extension = Ext_Zcb
+function clause extensionEnabled(Ext_Zcb) = sys_enable_zcb()
+
 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 extensionEnabled(Ext_Zcb)
+  <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_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 +30,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 extensionEnabled(Ext_Zcb)
+  <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_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 +48,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 extensionEnabled(Ext_Zcb)
+  <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extensionEnabled(Ext_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 +66,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 extensionEnabled(Ext_Zcb)
+  <-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if extensionEnabled(Ext_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 +84,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 extensionEnabled(Ext_Zcb)
+  <-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if extensionEnabled(Ext_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 +102,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 extensionEnabled(Ext_Zcb)
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if extensionEnabled(Ext_Zcb)
 
 mapping clause assembly = C_ZEXT_B(rsdc) <->
   "c.zext.b" ^ spc() ^ creg_name(rsdc)
@@ -116,8 +119,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 extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb)
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb)
 
 mapping clause assembly = C_SEXT_B(rsdc) <->
   "c.sext.b" ^ spc() ^ creg_name(rsdc)
@@ -132,8 +135,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 extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb)
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb)
 
 mapping clause assembly = C_ZEXT_H(rsdc) <->
   "c.zext.h" ^ spc() ^ creg_name(rsdc)
@@ -148,8 +151,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 extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb)
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zbb)
 
 mapping clause assembly = C_SEXT_H(rsdc) <->
   "c.sext.h" ^ spc() ^ creg_name(rsdc)
@@ -164,8 +167,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 extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & sizeof(xlen) == 64
 
 mapping clause assembly = C_ZEXT_W(rsdc) <->
   "c.zext.w" ^ spc() ^ creg_name(rsdc)
@@ -180,8 +183,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 extensionEnabled(Ext_Zcb)
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if extensionEnabled(Ext_Zcb)
 
 mapping clause assembly = C_NOT(rsdc) <->
   "c.not" ^ spc() ^ creg_name(rsdc)
@@ -197,8 +200,8 @@ function clause execute C_NOT(rsdc) = {
 union clause ast = C_MUL : (cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_MUL(rsdc, rs2c)                                             if haveZcb() & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
+      C_MUL(rsdc, rs2c)                                             if extensionEnabled(Ext_Zcb) & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if extensionEnabled(Ext_Zcb) & (extensionEnabled(Ext_M) | extensionEnabled(Ext_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 af54b5679..5e55fb8a2 100644
--- a/model/riscv_insts_zfh.sail
+++ b/model/riscv_insts_zfh.sail
@@ -6,6 +6,9 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+enum clause extension = Ext_Zhinx
+function clause extensionEnabled(Ext_Zhinx) = sys_enable_zfinx()
+
 /* **************************************************************** */
 /* This file specifies the instructions in the Zfh extension        */
 /* (half precision floating point).                                 */
@@ -162,7 +165,7 @@ function fle_H   (v1,       v2,        is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()'                                  */
 
-function haveHalfFPU() -> bool = extensionEnabled(Ext_Zfh) | haveZhinx()
+function haveHalfFPU() -> bool = extensionEnabled(Ext_Zfh) | extensionEnabled(Ext_Zhinx)
 
 /* ****************************************************************** */
 /* Floating-point loads                                               */
diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail
index 688d16d72..2d6c0b122 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, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus
+function clause ext_is_CSR_defined(0x004, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie
+function clause ext_is_CSR_defined(0x005, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec
+function clause ext_is_CSR_defined(0x040, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch
+function clause ext_is_CSR_defined(0x041, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc
+function clause ext_is_CSR_defined(0x042, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause
+function clause ext_is_CSR_defined(0x043, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval
+function clause ext_is_CSR_defined(0x044, _) = extensionEnabled(Ext_U) & extensionEnabled(Ext_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 2d28e11d4..91d86a06e 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -27,14 +27,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 & (extensionEnabled(Ext_S) | extensionEnabled(Ext_N)), // medeleg
+    0x303 => p == Machine & (extensionEnabled(Ext_S) | extensionEnabled(Ext_N)), // mideleg
     0x304 => p == Machine, // mie
     0x305 => p == Machine, // mtvec
-    0x306 => p == Machine & haveUsrMode(), // mcounteren
-    0x30A => p == Machine & haveUsrMode(), // menvcfg
+    0x306 => p == Machine & extensionEnabled(Ext_U), // mcounteren
+    0x30A => p == Machine & extensionEnabled(Ext_U), // menvcfg
     0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush
-    0x31A => p == Machine & haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh
+    0x31A => p == Machine & extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // menvcfgh
     0x320 => p == Machine, // mcountinhibit
     /* machine mode: trap handling */
     0x340 => p == Machine, // mscratch
@@ -61,32 +61,32 @@ 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 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // sstatus
+    0x102 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N) & (p == Machine | p == Supervisor), // sedeleg
+    0x103 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N) & (p == Machine | p == Supervisor), // sideleg
+    0x104 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // sie
+    0x105 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // stvec
+    0x106 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // scounteren
+    0x10A => extensionEnabled(Ext_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 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // sscratch
+    0x141 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // sepc
+    0x142 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // scause
+    0x143 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // stval
+    0x144 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // sip
 
     /* supervisor mode: address translation */
-    0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp
+    0x180 => extensionEnabled(Ext_S) & (p == Machine | p == Supervisor), // satp
 
     /* user mode: counters */
-    0xC00 => haveUsrMode(),    // cycle
-    0xC01 => haveUsrMode(),    // time
-    0xC02 => haveUsrMode(),    // instret
+    0xC00 => extensionEnabled(Ext_U),    // cycle
+    0xC01 => extensionEnabled(Ext_U),    // time
+    0xC02 => extensionEnabled(Ext_U),    // instret
 
-    0xC80 => haveUsrMode() & (sizeof(xlen) == 32),     // cycleh
-    0xC81 => haveUsrMode() & (sizeof(xlen) == 32),     // timeh
-    0xC82 => haveUsrMode() & (sizeof(xlen) == 32),     // instreth
+    0xC80 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32),     // cycleh
+    0xC81 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32),     // timeh
+    0xC82 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32),     // instreth
 
     /* user mode: Zkr */
     0x015 => extensionEnabled(Ext_Zkr),
@@ -109,9 +109,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(extensionEnabled(Ext_S)) | scounteren[CY] == 0b1),
+    (0xC01, User) => mcounteren[TM] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[TM] == 0b1),
+    (0xC02, User) => mcounteren[IR] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[IR] == 0b1),
 
     (_, _) => /* no HPM counters for now */
               if   0xC03 <=_u csr & csr <=_u 0xC1F
@@ -170,11 +170,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   extensionEnabled(Ext_S)
+              then super & extensionEnabled(Ext_N) & bit_to_bool(sedeleg.bits[idx])
+              else super & extensionEnabled(Ext_N);
+  let deleg = if      extensionEnabled(Ext_U) & user  then User
+              else if extensionEnabled(Ext_S) & super then Supervisor
               else                               Machine;
   /* We cannot transition to a less-privileged mode. */
   if   privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
@@ -230,7 +230,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(extensionEnabled(Ext_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 {
@@ -239,13 +239,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 = extensionEnabled(Ext_S) & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1));
+    let uIE = extensionEnabled(Ext_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(extensionEnabled(Ext_S)) then {
           if uIE then let r = (d, User) in Some(r)
           else                             None()
         } else {
@@ -269,7 +269,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(extensionEnabled(Ext_U)) | (not(extensionEnabled(Ext_S)) & not(extensionEnabled(Ext_N))) then {
     assert(priv == Machine, "invalid current privilege");
     let enabled_pending = mip.bits & mie.bits;
     match findPendingInterrupt(enabled_pending) {
@@ -348,7 +348,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 (extensionEnabled(Ext_S), "no supervisor mode present for delegation");
 
        scause[IsInterrupt] = bool_to_bits(intr);
        scause[Cause]       = zero_extend(c);
@@ -373,7 +373,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(extensionEnabled(Ext_U), "no user mode present for delegation");
 
        ucause[IsInterrupt] = bool_to_bits(intr);
        ucause[Cause]       = zero_extend(c);
@@ -410,7 +410,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 extensionEnabled(Ext_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 7429787e6..fc19d5161 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -128,29 +128,26 @@ 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 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 haveBExt() -> bool = misa[B] == 0b1
-function haveZba()  -> bool = true | haveBExt()
-function haveZbb()  -> bool = true | haveBExt()
+enum clause extension = Ext_N
+function clause extensionEnabled(Ext_N) = misa[N] == 0b1
+
+enum clause extension = Ext_U
+function clause extensionEnabled(Ext_U) = misa[U] == 0b1
+
+enum clause extension = Ext_S
+function clause extensionEnabled(Ext_S) = misa[S] == 0b1
 
 /*
  * 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
+  if extensionEnabled(Ext_U) then User else Machine
 
 function have_privLevel(priv : priv_level) -> bool =
   match priv {
-    0b00 => haveUsrMode(),
-    0b01 => haveSupMode(),
+    0b00 => extensionEnabled(Ext_U),
+    0b01 => extensionEnabled(Ext_S),
     0b10 => false,
     0b11 => true,
   }
@@ -269,13 +266,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(extensionEnabled(Ext_N)) then {
              let m = [m with UPIE = 0b0];
              let m = [m with UIE = 0b0];
              m
           } else m;
 
-  if not(haveUsrMode()) then {
+  if not(extensionEnabled(Ext_U)) then {
     let m = [m with MPRV = 0b0];
     m
   } else m
@@ -300,19 +297,6 @@ function in32BitMode() -> bool = {
   cur_Architecture() == RV32
 }
 
-/* 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 = {
@@ -337,7 +321,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 extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then {
     [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]]
   } else m
 }
@@ -353,7 +337,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 extensionEnabled(Ext_U) & extensionEnabled(Ext_N) then {
     [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]]
   } else m
 }
@@ -641,7 +625,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 extensionEnabled(Ext_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
@@ -658,7 +642,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 extensionEnabled(Ext_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;