diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 8141acec2..04ae9a67b 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -10,6 +10,9 @@
 /* This file specifies the atomic instructions in the 'A' extension.  */
 
 /* ****************************************************************** */
+enum clause extension = Ext_Zabha
+function clause extensionEnabled(Ext_Zabha) = true
+
 // Some print utils for lr/sc.
 
 function aqrl_str(aq : bool, rl : bool) -> string =
@@ -42,18 +45,21 @@ function lrsc_width_valid(size : word_width) -> bool = {
 
 function amo_width_valid(size : word_width) -> bool = {
   match size {
-    BYTE   => haveZabha(),
-    HALF   => haveZabha(),
+    BYTE   => extensionEnabled(Ext_Zabha),
+    HALF   => extensionEnabled(Ext_Zabha),
     WORD   => true,
     DOUBLE => sizeof(xlen) >= 64,
   }
 }
 
 /* ****************************************************************** */
+enum clause extension = Ext_Zalrsc
+function clause extensionEnabled(Ext_Zalrsc) = misa[A] == 0b1
+
 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
 
-mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if haveZalrsc() & lrsc_width_valid(size)
-  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & lrsc_width_valid(size)
+mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
+  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
 
 /* We could set load-reservations on physical or virtual addresses.
  * For now we set them on virtual addresses, since it makes the
@@ -96,8 +102,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
 /* ****************************************************************** */
 union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)
 
-mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)                                      if haveZalrsc() & lrsc_width_valid(size)
-  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & lrsc_width_valid(size)
+mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)                                      if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
+  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size)
 
 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
@@ -157,6 +163,9 @@ mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd)
   <-> "sc." ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
 
 /* ****************************************************************** */
+enum clause extension = Ext_Zaamo
+function clause extensionEnabled(Ext_Zaamo) = misa[A] == 0b1
+
 union clause ast = AMO : (amoop, bool, bool, regidx, regidx, word_width, regidx)
 
 mapping encdec_amoop : amoop <-> bits(5) = {
@@ -171,8 +180,8 @@ mapping encdec_amoop : amoop <-> bits(5) = {
   AMOMAXU <-> 0b11100
 }
 
-mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)                                                if haveZaamo() & amo_width_valid(size)
-  <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZaamo() & amo_width_valid(size)
+mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)                                                if extensionEnabled(Ext_Zaamo) & amo_width_valid(size)
+  <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zaamo) & amo_width_valid(size)
 
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index cfac3bb31..b153e792b 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -11,6 +11,12 @@
 
 /* ****************************************************************** */
 
+enum clause extension = Ext_M
+function clause extensionEnabled(Ext_M) = misa[M] == 0b1
+enum clause extension = Ext_Zmmul
+function clause extensionEnabled(Ext_Zmmul) = true
+
+
 union clause ast = MUL : (regidx, regidx, regidx, mul_op)
 
 mapping encdec_mul_op : mul_op <-> bits(3) = {
@@ -20,8 +26,8 @@ mapping encdec_mul_op : mul_op <-> bits(3) = {
   struct { high = true,  signed_rs1 = false, signed_rs2 = false } <-> 0b011
 }
 
-mapping clause encdec = MUL(rs2, rs1, rd, mul_op)                    if haveMulDiv() | haveZmmul()
-  <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if haveMulDiv() | haveZmmul()
+mapping clause encdec = MUL(rs2, rs1, rd, mul_op)                    if extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)
+  <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)
 
 function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
   let rs1_val = X(rs1);
@@ -49,8 +55,8 @@ mapping clause assembly = MUL(rs2, rs1, rd, mul_op)
 /* ****************************************************************** */
 union clause ast = DIV : (regidx, regidx, regidx, bool)
 
-mapping clause encdec = DIV(rs2, rs1, rd, s)                           if haveMulDiv()
-  <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
+mapping clause encdec = DIV(rs2, rs1, rd, s)                           if extensionEnabled(Ext_M)
+  <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if extensionEnabled(Ext_M)
 
 function clause execute (DIV(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1);
@@ -75,8 +81,8 @@ mapping clause assembly = DIV(rs2, rs1, rd, s)
 /* ****************************************************************** */
 union clause ast = REM : (regidx, regidx, regidx, bool)
 
-mapping clause encdec = REM(rs2, rs1, rd, s)                           if haveMulDiv()
-  <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
+mapping clause encdec = REM(rs2, rs1, rd, s)                           if extensionEnabled(Ext_M)
+  <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if extensionEnabled(Ext_M)
 
 function clause execute (REM(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1);
@@ -96,9 +102,9 @@ mapping clause assembly = REM(rs2, rs1, rd, s)
 union clause ast = MULW : (regidx, regidx, regidx)
 
 mapping clause encdec = MULW(rs2, rs1, rd)
-      if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
+      if sizeof(xlen) == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
   <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
+      if sizeof(xlen) == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
 
 function clause execute (MULW(rs2, rs1, rd)) = {
   let rs1_val = X(rs1)[31..0];
@@ -121,9 +127,9 @@ mapping clause assembly = MULW(rs2, rs1, rd)
 union clause ast = DIVW : (regidx, regidx, regidx, bool)
 
 mapping clause encdec = DIVW(rs2, rs1, rd, s)
-      if sizeof(xlen) == 64 & haveMulDiv()
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_M)
   <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
-      if sizeof(xlen) == 64 & haveMulDiv()
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_M)
 
 function clause execute (DIVW(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1)[31..0];
@@ -146,9 +152,9 @@ mapping clause assembly = DIVW(rs2, rs1, rd, s)
 union clause ast = REMW : (regidx, regidx, regidx, bool)
 
 mapping clause encdec = REMW(rs2, rs1, rd, s)
-      if sizeof(xlen) == 64 & haveMulDiv()
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_M)
   <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
-      if sizeof(xlen) == 64 & haveMulDiv()
+      if sizeof(xlen) == 64 & extensionEnabled(Ext_M)
 
 function clause execute (REMW(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1)[31..0];
diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail
index 86253bff4..71a6e4c46 100644
--- a/model/riscv_insts_zcb.sail
+++ b/model/riscv_insts_zcb.sail
@@ -197,8 +197,8 @@ function clause execute C_NOT(rsdc) = {
 union clause ast = C_MUL : (cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_MUL(rsdc, rs2c)                                             if haveZcb() & (haveMulDiv() | haveZmmul())
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (haveMulDiv() | haveZmmul())
+      C_MUL(rsdc, rs2c)                                             if haveZcb() & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul))
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (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_sys_regs.sail b/model/riscv_sys_regs.sail
index 58f5e91dc..7429787e6 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -130,8 +130,6 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
 
 /* helpers to check support for various extensions. */
 /* we currently don't model 'E', so always assume 'I'. */
-function haveAtomics() -> bool = misa[A] == 0b1
-function haveMulDiv()  -> bool = misa[M] == 0b1
 function haveSupMode() -> bool = misa[S] == 0b1
 function haveUsrMode() -> bool = misa[U] == 0b1
 function haveNExt()    -> bool = misa[N] == 0b1
@@ -142,15 +140,6 @@ function haveBExt() -> bool = misa[B] == 0b1
 function haveZba()  -> bool = true | haveBExt()
 function haveZbb()  -> bool = true | haveBExt()
 
-function haveZmmul()  -> bool = true
-
-/* A extension sub-extensions */
-function haveZaamo()  -> bool = haveAtomics()
-function haveZalrsc() -> bool = haveAtomics()
-
-/* Zabha extension support */
-function haveZabha() -> bool = true
-
 /*
  * Illegal values legalized to least privileged mode supported.
  * Note: the only valid combinations of supported modes are M, M+U, M+S+U.