diff --git a/Makefile b/Makefile
index d62c85839..3aeb75757 100644
--- a/Makefile
+++ b/Makefile
@@ -203,6 +203,19 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
 all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH)
 .PHONY: all
 
+json: $(SAIL_SRCS) model/main.sail Makefile
+	@sail -json $(SAIL_FLAGS) $(SAIL_SRCS)
+
+.PHONY: check-json
+check-json:
+	sail -json $(SAIL_FLAGS) $(SAIL_SRCS) | python3 -c "import json; import sys; j=json.load(sys.stdin)"
+
+output: $(SAIL_SRCS) model/main.sail Makefile
+	sail -output-sail $(SAIL_FLAGS) $(SAIL_SRCS)
+
+decode: $(SAIL_SRCS) model/main.sail Makefile
+	sail -plugin $(HOME)/projects/Sail/riscvdecode/riscv_decode.cmxs -riscv_decode $(SAIL_FLAGS) $(SAIL_SRCS)
+
 # the following ensures empty sail-generated .c files don't hang around and
 # break future builds if sail exits badly
 .DELETE_ON_ERROR: generated_definitions/c/%.c
diff --git a/README.md b/README.md
index dcfea78f4..777e56f80 100644
--- a/README.md
+++ b/README.md
@@ -347,6 +347,10 @@ There is also (as yet unmerged) support for [integration with riscv-config](http
 For booting operating system images, see the information under the
 [os-boot/](os-boot/) subdirectory.
 
+### How to use the out-of-tree JSON backend to generate JSON from Sail
+
+For details, see [JSON.md](doc/JSON.md).
+
 ### Using development versions of Sail
 
 Rarely, the version of Sail packaged in opam may not meet your needs. This could happen if you need a bug fix or new feature not yet in the released Sail version, or you are actively working on Sail. In this case you can tell the `sail-riscv` `Makefile` to use a local copy of Sail by setting `SAIL_DIR` to the root of a checkout of the Sail repo when you invoke `make`. Alternatively, you can use `opam pin` to install Sail from a local checkout of the Sail repo as described in the Sail installation instructions.
diff --git a/doc/JSON.md b/doc/JSON.md
new file mode 100644
index 000000000..fc7f9cc01
--- /dev/null
+++ b/doc/JSON.md
@@ -0,0 +1,18 @@
+STEPS TO BUILD AND COMPILE THE PROJECT
+=======================================
+
+After Installing the prerequisites
+
+1.  We first need to build the sail parser.
+    1. Find a directory to clone this repository, and make that directory your current working directory.
+    2. `git clone https://github.com/ThinkOpenly/sail`
+    3. `cd sail`
+    4. `make`
+
+2.  Then, set up the environment for building in the RISC-V Sail repository:
+    1. `eval $(opam env)`
+    2. `export PATH=<path-to-sail-repository>:$PATH`
+
+3.  Clone this sail-riscv repository.
+
+4.  Within that clone : `make json`
diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
index 8f299994b..d5d3e46c1 100644
--- a/model/riscv_fdext_control.sail
+++ b/model/riscv_fdext_control.sail
@@ -17,9 +17,9 @@
 
 /* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */
 
-function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx()
-function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx()
-function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx()
+function clause ext_is_CSR_defined (0x001, _) = extension("F") | extension("Zfinx")
+function clause ext_is_CSR_defined (0x002, _) = extension("F") | extension("Zfinx")
+function clause ext_is_CSR_defined (0x003, _) = extension("F") | extension("Zfinx")
 
 function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS]))
 function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM]))
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index 6fd66917d..8ee928f43 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -19,7 +19,7 @@ function fetch() -> FetchResult =
   match ext_fetch_check_pc(PC, PC) {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extension("C"))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _)     => F_Error(e, PC),
diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail
index d25237572..8c7df53c7 100644
--- a/model/riscv_fetch_rvfi.sail
+++ b/model/riscv_fetch_rvfi.sail
@@ -17,7 +17,7 @@ function fetch() -> FetchResult = {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
       /* then check PC alignment */
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extension("C"))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _) => F_Error(e, PC),
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 3bf44b8f5..f7ef3c846 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -43,8 +43,8 @@ function amo_width_valid(size : word_width) -> bool = {
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
 
-mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if haveZalrsc() & amo_width_valid(size)
-  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
+mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if extension("Zalrsc") & amo_width_valid(size)
+  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_width_valid(size)
 
 
 /* We could set load-reservations on physical or virtual addresses.
@@ -88,8 +88,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() & amo_width_valid(size)
-  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
+mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)                                      if extension("Zalrsc") & amo_width_valid(size)
+  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_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)) = {
@@ -163,8 +163,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 extension("Zaamo") & amo_width_valid(size)
+  <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("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_base.sail b/model/riscv_insts_base.sail
index 26915f22c..bc435e53b 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -67,7 +67,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
     },
     Ext_ControlAddr_OK(target) => {
       /* Perform standard alignment check */
-      if bit_to_bool(target[1]) & not(haveRVC())
+      if bit_to_bool(target[1]) & not(extension("C"))
       then {
         handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
@@ -86,8 +86,18 @@ mapping clause assembly = RISCV_JAL(imm, rd)
   <-> "jal" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_21(imm)
 
 /* ****************************************************************** */
+$[name "jump and link register"]
+/*!
+ * The target address is obtained by adding the sign-extended 12-bit
+ * I-immediate to the register rs1, then setting the
+ * least-significant bit of the result to zero. The address of the
+ * instruction following the jump (pc+4) is written to register rd.
+ * Register x0 can be used as the destination if the result is not
+ * required.
+ */
 union clause ast = RISCV_JALR : (bits(12), regidx, regidx)
 
+$[format I]
 mapping clause encdec = RISCV_JALR(imm, rs1, rd)
   <-> imm @ rs1 @ 0b000 @ rd @ 0b1100111
 
@@ -97,6 +107,24 @@ mapping clause assembly = RISCV_JALR(imm, rs1, rd)
 /* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */
 
 /* ****************************************************************** */
+$[name "conditional branch"]
+/*!
+ * The target address for this branch instruction is determined by combining
+ * the sign-extended 13-bit immediate value with the contents of register rs1.
+ * Additionally, the least-significant bit of the result is set to zero.
+ * The condition for the branch is based on the specified operation (bop),
+ * which can be one of the following mnemonic codes:
+ *   - "beq"   : Branch if equal
+ *   - "bne"   : Branch if not equal
+ *   - "blt"   : Branch if less than (signed)
+ *   - "bge"   : Branch if greater than or equal to (signed)
+ *   - "bltu"  : Branch if less than (unsigned)
+ *   - "bgeu"  : Branch if greater than or equal to (unsigned)
+ *
+ * The branch is taken if the specified condition is true, leading to a jump
+ * to the target address. If the branch is not taken, the execution proceeds
+ * to the next instruction.
+ */
 union clause ast = BTYPE : (bits(13), regidx, regidx, bop)
 
 mapping encdec_bop : bop <-> bits(3) = {
@@ -131,7 +159,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
         RETIRE_FAIL
       },
       Ext_ControlAddr_OK(target) => {
-        if bit_to_bool(target[1]) & not(haveRVC()) then {
+        if bit_to_bool(target[1]) & not(extension("C")) then {
           handle_mem_exception(target, E_Fetch_Addr_Align());
           RETIRE_FAIL;
         } else {
@@ -156,6 +184,22 @@ mapping clause assembly = BTYPE(imm, rs2, rs1, op)
   <-> btype_mnemonic(op) ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_signed_13(imm)
 
 /* ****************************************************************** */
+
+/*!
+ * The ITYPE instruction operates on an immediate value, adding, comparing, or
+ * performing bitwise operations with the contents of register rs1.
+ * The immediate value, rs1, and the operation code (iop) determine the operation.
+ * The result is stored in register rd.
+ * The supported immediate operations (iop) include:
+ *   - "addi"  : Add immediate
+ *   - "slti"  : Set less than immediate (signed)
+ *   - "sltiu" : Set less than immediate (unsigned)
+ *   - "andi"  : AND immediate
+ *   - "ori"   : OR immediate
+ *   - "xori"  : XOR immediate
+ *
+ * Note: The immediate value is sign-extended before performing the operation.
+ */
 union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
 
 mapping encdec_iop : iop <-> bits(3) = {
@@ -186,18 +230,37 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = {
 }
 
 mapping itype_mnemonic : iop <-> string = {
-  RISCV_ADDI  <-> "addi",
-  RISCV_SLTI  <-> "slti",
-  RISCV_SLTIU <-> "sltiu",
-  RISCV_XORI  <-> "xori",
-  RISCV_ORI   <-> "ori",
-  RISCV_ANDI  <-> "andi"
+  $[name "add immediate"]
+    RISCV_ADDI  <-> "addi",
+  $[name "set less than immediate"]
+    RISCV_SLTI  <-> "slti",
+  $[name "set less than immediate unsigned"]
+    RISCV_SLTIU <-> "sltiu",
+  $[name "XOR immediate"]
+    RISCV_XORI  <-> "xori",
+  $[name "OR immediate"]
+    RISCV_ORI   <-> "ori",
+  $[name "AND immediate"]
+    RISCV_ANDI  <-> "andi"
 }
 
 mapping clause assembly = ITYPE(imm, rs1, rd, op)
   <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)
 
 /* ****************************************************************** */
+$[name "Shift Immediate"]
+/*!
+ * The SHIFTIOP (Shift Immediate Operation) instruction format is used for
+ * operations that involve shifting the bits of a register by an immediate
+ * value. The specific operation is determined by the opcode field, and the
+ * shift amount is specified by the immediate value (shamt). The result is
+ * written to the destination register (rd), and the source operand is the
+ * register specified by rs1. The format is common for shift-left logical
+ * immediate (SLLI), shift-right logical immediate (SRLI), and shift-right
+ * arithmetic immediate (SRAI) operations.
+ *
+ * Note: For RV32, the decoder ensures that shamt[5] = 0.
+ */
 union clause ast = SHIFTIOP : (bits(6), regidx, regidx, sop)
 
 mapping encdec_sop : sop <-> bits(3) = {
@@ -238,6 +301,15 @@ mapping clause assembly = SHIFTIOP(shamt, rs1, rd, op)
   <-> shiftiop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt)
 
 /* ****************************************************************** */
+
+/*!
+ * The R-type (Register-type) instruction format is used for operations
+ * that involve three registers. The specific operation is determined
+ * by the opcode and funct7 fields. The result is written to the
+ * destination register (rd), and the source operands are specified
+ * by the source registers (rs1 and rs2). The format is common for
+ * arithmetic, logical, and shift operations.
+ */
 union clause ast = RTYPE : (regidx, regidx, regidx, rop)
 
 mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_ADD)  <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011
@@ -293,6 +365,15 @@ mapping clause assembly = RTYPE(rs2, rs1, rd, op)
   <-> rtype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
+$[name "Load"]
+/*!
+ * The LOAD instruction format is used for loading data from memory into a
+ * register. The specific operation is determined by the word width (size),
+ * whether the load is signed or unsigned (is_unsigned), and memory ordering
+ * semantics (acquire, release). The result is written to the destination
+ * register (rd), and the memory address is computed by adding the immediate
+ * offset (imm) to the value in register rs1.
+ */
 union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, bool)
 
 /* unsigned loads are only present for widths strictly less than xlen,
@@ -364,6 +445,14 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
   <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"
 
 /* ****************************************************************** */
+$[name "Store"]
+/*!
+ * The STORE instruction format is used for storing data from a register into
+ * memory. The specific operation is determined by the word width (size) and
+ * memory ordering semantics (acquire, release). The memory address is computed
+ * by adding the immediate offset (imm) to the value in register rs1, and the
+ * data is taken from register rs2.
+ */
 union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)
 
 mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)              if size_bytes(size) <= sizeof(xlen_bytes)
@@ -409,8 +498,19 @@ mapping clause assembly = STORE(imm, rs2, rs1, size, aq, rl)
   <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_signed_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
 
 /* ****************************************************************** */
+$[name "Add Immediate Word"]
+/*!
+ * The ADDIW instruction involves adding a sign-extended
+ * 12-bit immediate value to the content of register rs1. The result is a 32-bit
+ * value, and overflow is disregarded. The final outcome is the lower 32 bits of
+ * the result, sign-extended to 64 bits. If the immediate value is set to zero
+ * in the ADDIW rd, rs1, 0 operation, the sign-extension of the lower 32 bits
+ * of register rs1 is written to register rd.
+ */
+
 union clause ast = ADDIW : (bits(12), regidx, regidx)
 
+$[format I]
 mapping clause encdec = ADDIW(imm, rs1, rd)
       if sizeof(xlen) == 64
   <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011
@@ -428,6 +528,16 @@ mapping clause assembly = ADDIW(imm, rs1, rd)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
+
+/*!
+ * The RTYPEW instruction set operates on 32-bit values,
+ * and the result is sign-extended to 64 bits. The available operations are
+ * ADDW (addition), SUBW (subtraction), SLLW (logical left shift),
+ * SRLW (logical right shift), and SRAW (arithmetic right shift).
+ * These operations are only applicable when the width of the target
+ * architecture is 64 bits.
+ */
+
 union clause ast = RTYPEW : (regidx, regidx, regidx, ropw)
 
 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW)
@@ -479,6 +589,16 @@ mapping clause assembly = RTYPEW(rs2, rs1, rd, op)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
+$[name "Shift Immediate Word"]
+/*!
+ * The SHIFTIWOP instruction set deals with
+ * immediate shift operations on 32-bit values, with the result sign-extended
+ * to 64 bits. The available operations include SLLIW (left shift logical
+ * immediate word), SRLIW (right shift logical immediate word), and SRAIW
+ * (right shift arithmetic immediate word). These operations are applicable
+ * when the target architecture has a width of 64 bits.
+ */
+
 union clause ast = SHIFTIWOP : (bits(5), regidx, regidx, sopw)
 
 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW)
@@ -517,8 +637,28 @@ mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op)
       if sizeof(xlen) == 64
 
 /* ****************************************************************** */
+$[name "Fence (Memory)"]
+/*!
+ * The FENCE instruction is used to provide memory ordering guarantees.
+ * It specifies ordering constraints on memory operations that precede
+ * and follow it in program order. The FENCE instruction includes two
+ * 4-bit fields, 'pred' and 'succ', which represent the memory ordering
+ * requirements before and after the FENCE instruction, respectively.
+ *
+ * The bits in 'pred' and 'succ' represent the following ordering constraints:
+ * - 'i': instruction stream order
+ * - 'o': outstanding loads
+ * - 'r': read operations
+ * - 'w': write operations
+ *
+ * The FENCE instruction is used to control the visibility of memory
+ * operations, and its behavior is influenced by the 'pred' and 'succ'
+ * fields. The precise semantics of the FENCE instruction depend on the
+ * specific bits set in these fields.
+ */
 union clause ast = FENCE : (bits(4), bits(4))
 
+$[format I]
 mapping clause encdec = FENCE(pred, succ)
   <-> 0b0000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
@@ -583,8 +723,19 @@ mapping clause assembly = FENCE(pred, succ)
   <-> "fence" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)
 
 /* ****************************************************************** */
+$[name "Fence (Total Store Order)"]
+/*!
+ * The FENCE_TSO instruction is a memory
+ * ordering instruction that provides a stronger memory consistency model
+ * compared to the standard FENCE instruction. It ensures that all memory
+ * operations preceding and following the FENCE_TSO instruction are globally
+ * ordered. The FENCE_TSO instruction includes two 4-bit fields, 'pred' and
+ * 'succ', which represent the memory ordering requirements before and after
+ * the FENCE_TSO instruction, respectively.
+ */
 union clause ast = FENCE_TSO : (bits(4), bits(4))
 
+$[format I]
 mapping clause encdec = FENCE_TSO(pred, succ)
   <-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
 
@@ -603,6 +754,14 @@ mapping clause assembly = FENCE_TSO(pred, succ)
   <-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)
 
 /* ****************************************************************** */
+$[name "Fence (Instruction)"]
+/*!
+ * The FENCEI instruction is a memory ordering instruction that
+ * provides a barrier to the instruction stream.
+ * It ensures that all instructions preceding the FENCEI instruction are
+ * globally ordered. The FENCEI instruction has no 'pred' or 'succ' fields,
+ * and it is typically used to control instruction stream visibility.
+ */
 union clause ast = FENCEI : unit
 
 mapping clause encdec = FENCEI()
@@ -614,6 +773,14 @@ function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ RETIRE_SU
 mapping clause assembly = FENCEI() <-> "fence.i"
 
 /* ****************************************************************** */
+$[name "Environment Call"]
+/*!
+ * The ECALL instruction, previously called SCALL is used to make a
+ * request to the supporting execution environment, typically an
+ * operating system. The ABI for the system defines how parameters
+ * for the environment request are passed, often in defined locations
+ * in the integer register file.
+ */
 union clause ast = ECALL : unit
 
 mapping clause encdec = ECALL()
@@ -635,6 +802,12 @@ function clause execute ECALL() = {
 mapping clause assembly = ECALL() <-> "ecall"
 
 /* ****************************************************************** */
+$[name "Machine-level Return"]
+/*!
+ * The MRET instruction is used to return from a machine-level exception,
+ * transferring control back to the instruction following the one that
+ * caused the exception. It is only valid when executed in Machine mode.
+ */
 union clause ast = MRET : unit
 
 mapping clause encdec = MRET()
@@ -654,6 +827,12 @@ function clause execute MRET() = {
 mapping clause assembly = MRET() <-> "mret"
 
 /* ****************************************************************** */
+$[name "Supervisor-level Return"]
+/*!
+ * The SRET instruction is used to return from a supervisor-level exception,
+ * transferring control back to the instruction following the one that
+ * caused the exception. It is only valid when executed in Supervisor mode.
+ */
 union clause ast = SRET : unit
 
 mapping clause encdec = SRET()
@@ -662,8 +841,8 @@ mapping clause encdec = SRET()
 function clause execute SRET() = {
   let sret_illegal : bool = match cur_privilege {
     User       => true,
-    Supervisor => not(haveSupMode ()) | mstatus[TSR] == 0b1,
-    Machine    => not(haveSupMode ())
+    Supervisor => not(extension("S")) | mstatus[TSR] == 0b1,
+    Machine    => not(extension("S"))
   };
   if   sret_illegal
   then { handle_illegal(); RETIRE_FAIL }
@@ -678,6 +857,13 @@ function clause execute SRET() = {
 mapping clause assembly = SRET() <-> "sret"
 
 /* ****************************************************************** */
+$[name "Environment Breakpoint"]
+/*!
+ * The EBREAK instruction, previously called SBREAK is utilized by
+ * debuggers to trigger a breakpoint exception, leading to a transfer
+ * of control back to a debugging environment.
+ * This instruction is commonly employed for debugging purposes.
+ */
 union clause ast = EBREAK : unit
 
 mapping clause encdec = EBREAK()
@@ -691,6 +877,17 @@ function clause execute EBREAK() = {
 mapping clause assembly = EBREAK() <-> "ebreak"
 
 /* ****************************************************************** */
+$[name "Wait For Interrupt"]
+/*!
+ * The WFI (Wait For Interrupt) instruction is used to suspend the execution
+ * pipeline until an interrupt or an event occurs. Its behavior depends on the
+ * current privilege level:
+ * - In Machine mode, it invokes the platform-specific WFI handler.
+ * - In Supervisor mode, it checks the TW (Timer Wait) bit in mstatus. If the
+ *   bit is set, it handles the illegal instruction and returns with RETIRE_FAIL.
+ *   Otherwise, it invokes the platform-specific WFI handler.
+ * - In User mode, it handles the illegal instruction and returns with RETIRE_FAIL.
+ */
 union clause ast = WFI : unit
 
 mapping clause encdec = WFI()
@@ -708,8 +905,21 @@ function clause execute WFI() =
 mapping clause assembly = WFI() <-> "wfi"
 
 /* ****************************************************************** */
+$[name "Store Fence (Virtual Memory Address)"]
+/*!
+ * The SFENCE.VMA instruction is used to synchronize the store queue and flush
+ * TLB entries based on virtual memory address and optional ASID values.
+ * Its behavior depends on the current privilege level:
+ * - In User mode, it handles the illegal instruction and returns with RETIRE_FAIL.
+ * - In Supervisor mode, it checks for illegal instructions and performs TLB
+ *   flushing based on the provided virtual memory address and ASID values.
+ * - In Machine mode, it performs TLB flushing based on the provided virtual
+ *   memory address and ASID values.
+ */
+
 union clause ast = SFENCE_VMA : (regidx, regidx)
 
+$[format R]
 mapping clause encdec = SFENCE_VMA(rs1, rs2)
   <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011
 
diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail
index aeda8fc3f..a081ffbf3 100644
--- a/model/riscv_insts_cdext.sail
+++ b/model/riscv_insts_cdext.sail
@@ -17,9 +17,9 @@
 union clause ast = C_FLDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
   <-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
 
 function clause execute (C_FLDSP(uimm, rd)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -35,9 +35,9 @@ mapping clause assembly = C_FLDSP(uimm, rd)
 union clause ast = C_FSDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
   <-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
 
 function clause execute (C_FSDSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -53,9 +53,9 @@ mapping clause assembly = C_FSDSP(uimm, rs2)
 union clause ast = C_FLD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
   <-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
 
 function clause execute (C_FLD(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -73,9 +73,9 @@ mapping clause assembly = C_FLD(uimm, rsc, rdc)
 union clause ast = C_FSD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
   <-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & extension("C") & extension("D")
 
 function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index b7c63c2a5..25ec038eb 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -17,8 +17,8 @@
 /* ****************************************************************** */
 union clause ast = C_NOP : unit
 
-mapping clause encdec_compressed = C_NOP()
-  <-> 0b000 @ 0b0 @ 0b00000 @ 0b00000 @ 0b01
+mapping clause encdec_compressed = C_NOP() if extension("C")
+  <-> 0b000 @ 0b0 @ 0b00000 @ 0b00000 @ 0b01 if extension("C")
 
 function clause execute C_NOP() = RETIRE_SUCCESS
 
@@ -29,9 +29,9 @@ mapping clause assembly = C_NOP() <-> "c.nop"
 union clause ast = C_ADDI4SPN : (cregidx, bits(8))
 
 mapping clause encdec_compressed = C_ADDI4SPN(rd, nz96 @ nz54 @ nz3 @ nz2)
-      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000
+      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 & extension("C")
   <-> 0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregidx @ 0b00
-      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000
+      if nz96 @ nz54 @ nz3 @ nz2 != 0b00000000 & extension("C")
 
 function clause execute (C_ADDI4SPN(rdc, nzimm)) = {
   let imm : bits(12) = (0b00 @ nzimm @ 0b00);
@@ -47,8 +47,8 @@ mapping clause assembly = C_ADDI4SPN(rdc, nzimm)
 /* ****************************************************************** */
 union clause ast = C_LW : (bits(5), cregidx, cregidx)
 
-mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd)
-  <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
+mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd) if extension("C")
+  <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 if extension("C")
 
 function clause execute (C_LW(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -64,9 +64,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc)
 union clause ast = C_LD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
 
 function clause execute (C_LD(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -83,8 +83,8 @@ mapping clause assembly = C_LD(uimm, rsc, rdc)
 /* ****************************************************************** */
 union clause ast = C_SW : (bits(5), cregidx, cregidx)
 
-mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2)
-  <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
+mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2) if extension("C")
+  <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 if extension("C")
 
 function clause execute (C_SW(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -100,9 +100,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2)
 union clause ast = C_SD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
   <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
 
 function clause execute (C_SD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -120,9 +120,9 @@ mapping clause assembly = C_SD(uimm, rsc1, rsc2)
 union clause ast = C_ADDI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_ADDI(nzi5 @ nzi40, rsd)
-      if nzi5 @ nzi40 != 0b000000 & rsd != zreg
+      if nzi5 @ nzi40 != 0b000000 & rsd != zreg & extension("C")
   <-> 0b000 @ nzi5 : bits(1) @ rsd : regidx @ nzi40 : bits(5) @ 0b01
-      if nzi5 @ nzi40 != 0b000000 & rsd != zreg
+      if nzi5 @ nzi40 != 0b000000 & rsd != zreg & extension("C")
 
 function clause execute (C_ADDI(nzi, rsd)) = {
   let imm : bits(12) = sign_extend(nzi);
@@ -138,9 +138,9 @@ mapping clause assembly = C_ADDI(nzi, rsd)
 union clause ast = C_JAL : (bits(11))
 
 mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31)
-      if sizeof(xlen) == 32
+      if sizeof(xlen) == 32 & extension("C")
   <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01
-      if sizeof(xlen) == 32
+      if sizeof(xlen) == 32 & extension("C")
 
 function clause execute (C_JAL(imm)) =
   execute(RISCV_JAL(sign_extend(imm @ 0b0), ra))
@@ -154,9 +154,9 @@ mapping clause assembly = C_JAL(imm)
 union clause ast = C_ADDIW : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
-      if rsd != zreg & sizeof(xlen) == 64
+      if rsd != zreg & sizeof(xlen) == 64 & extension("C")
   <-> 0b001 @ imm5 : bits(1) @ rsd : regidx @ imm40 : bits(5) @ 0b01
-      if rsd != zreg & sizeof(xlen) == 64
+      if rsd != zreg & sizeof(xlen) == 64 & extension("C")
 
 function clause execute (C_ADDIW(imm, rsd)) =
   execute(ADDIW(sign_extend(imm), rsd, rsd))
@@ -170,9 +170,9 @@ mapping clause assembly = C_ADDIW(imm, rsd)
 union clause ast = C_LI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LI(imm5 @ imm40, rd)
-      if rd != zreg
+      if rd != zreg & extension("C")
   <-> 0b010 @ imm5 : bits(1) @ rd : regidx @ imm40 : bits(5) @ 0b01
-      if rd != zreg
+      if rd != zreg & extension("C")
 
 function clause execute (C_LI(imm, rd)) = {
   let imm : bits(12) = sign_extend(imm);
@@ -188,9 +188,9 @@ mapping clause assembly = C_LI(imm, rd)
 union clause ast = C_ADDI16SP : (bits(6))
 
 mapping clause encdec_compressed = C_ADDI16SP(nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4)
-      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000
+      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 & extension("C")
   <-> 0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01
-      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000
+      if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 & extension("C")
 
 function clause execute (C_ADDI16SP(imm)) = {
   let imm : bits(12) = sign_extend(imm @ 0x0);
@@ -206,9 +206,9 @@ mapping clause assembly = C_ADDI16SP(imm)
 union clause ast = C_LUI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LUI(imm17 @ imm1612, rd)
-      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000
+      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 & extension("C")
   <-> 0b011 @ imm17 : bits(1) @ rd : regidx @ imm1612 : bits(5) @ 0b01
-      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000
+      if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 & extension("C")
 
 function clause execute (C_LUI(imm, rd)) = {
   let res : bits(20) = sign_extend(imm);
@@ -224,9 +224,9 @@ mapping clause assembly = C_LUI(imm, rd)
 union clause ast = C_SRLI : (bits(6), cregidx)
 
 mapping clause encdec_compressed = C_SRLI(nzui5 @ nzui40, rsd)
-      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extension("C")
   <-> 0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
-      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extension("C")
 
 function clause execute (C_SRLI(shamt, rsd)) = {
   let rsd = creg2reg_idx(rsd);
@@ -242,9 +242,9 @@ mapping clause assembly = C_SRLI(shamt, rsd)
 union clause ast = C_SRAI : (bits(6), cregidx)
 
 mapping clause encdec_compressed = C_SRAI(nzui5 @ nzui40, rsd)
-      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extension("C")
   <-> 0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01
-      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extension("C")
 
 function clause execute (C_SRAI(shamt, rsd)) = {
   let rsd = creg2reg_idx(rsd);
@@ -259,8 +259,8 @@ mapping clause assembly = C_SRAI(shamt, rsd)
 /* ****************************************************************** */
 union clause ast = C_ANDI : (bits(6), cregidx)
 
-mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd)
-  <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregidx @ i40 : bits(5) @ 0b01
+mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd) if extension("C")
+  <-> 0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregidx @ i40 : bits(5) @ 0b01 if extension("C")
 
 function clause execute (C_ANDI(imm, rsd)) = {
   let rsd = creg2reg_idx(rsd);
@@ -273,8 +273,8 @@ mapping clause assembly = C_ANDI(imm, rsd)
 /* ****************************************************************** */
 union clause ast = C_SUB : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_SUB(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_SUB(rsd, rs2) if extension("C")
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01 if extension("C")
 
 function clause execute (C_SUB(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -288,8 +288,8 @@ mapping clause assembly = C_SUB(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_XOR : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_XOR(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_XOR(rsd, rs2) if extension("C")
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01 if extension("C")
 
 function clause execute (C_XOR(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -303,8 +303,8 @@ mapping clause assembly = C_XOR(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_OR : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_OR(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_OR(rsd, rs2) if extension("C")
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b10 @ rs2 : cregidx @ 0b01 if extension("C")
 
 function clause execute (C_OR(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -318,8 +318,8 @@ mapping clause assembly = C_OR(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_AND : (cregidx, cregidx)
 
-mapping clause encdec_compressed = C_AND(rsd, rs2)
-  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b11 @ rs2 : cregidx @ 0b01
+mapping clause encdec_compressed = C_AND(rsd, rs2) if extension("C")
+  <-> 0b100 @ 0b0 @ 0b11 @ rsd : cregidx @ 0b11 @ rs2 : cregidx @ 0b01 if extension("C")
 
 function clause execute (C_AND(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -334,9 +334,9 @@ mapping clause assembly = C_AND(rsd, rs2)
 union clause ast = C_SUBW : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_SUBW(rsd, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
 
 function clause execute (C_SUBW(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -353,9 +353,9 @@ mapping clause assembly = C_SUBW(rsd, rs2)
 union clause ast = C_ADDW : (cregidx, cregidx)
 
 mapping clause encdec_compressed = C_ADDW(rsd, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
   <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
 
 function clause execute (C_ADDW(rsd, rs2)) = {
   let rsd = creg2reg_idx(rsd);
@@ -371,8 +371,8 @@ mapping clause assembly = C_ADDW(rsd, rs2)
 /* ****************************************************************** */
 union clause ast = C_J : (bits(11))
 
-mapping clause encdec_compressed = C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31)
-  <-> 0b101 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01
+mapping clause encdec_compressed = C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) if extension("C")
+  <-> 0b101 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 if extension("C")
 
 function clause execute (C_J(imm)) =
   execute(RISCV_JAL(sign_extend(imm @ 0b0), zreg))
@@ -383,8 +383,8 @@ mapping clause assembly = C_J(imm)
 /* ****************************************************************** */
 union clause ast = C_BEQZ : (bits(8), cregidx)
 
-mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs)
-  <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
+mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs) if extension("C")
+  <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 if extension("C")
 
 function clause execute (C_BEQZ(imm, rs)) =
   execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BEQ))
@@ -395,8 +395,8 @@ mapping clause assembly = C_BEQZ(imm, rs)
 /* ****************************************************************** */
 union clause ast = C_BNEZ : (bits(8), cregidx)
 
-mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs)
-  <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01
+mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs) if extension("C")
+  <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 if extension("C")
 
 function clause execute (C_BNEZ(imm, rs)) =
   execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BNE))
@@ -408,9 +408,9 @@ mapping clause assembly = C_BNEZ(imm, rs)
 union clause ast = C_SLLI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd)
-      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extension("C")
   <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10
-      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extension("C")
 
 function clause execute (C_SLLI(shamt, rsd)) =
   execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI))
@@ -424,9 +424,9 @@ mapping clause assembly = C_SLLI(shamt, rsd)
 union clause ast = C_LWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd)
-      if rd != zreg
+      if rd != zreg & extension("C")
   <-> 0b010 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
-      if rd != zreg
+      if rd != zreg & extension("C")
 
 function clause execute (C_LWSP(uimm, rd)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -442,9 +442,9 @@ mapping clause assembly = C_LWSP(uimm, rd)
 union clause ast = C_LDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd)
-      if rd != zreg & sizeof(xlen) == 64
+      if rd != zreg & sizeof(xlen) == 64 & extension("C")
   <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if rd != zreg & sizeof(xlen) == 64
+      if rd != zreg & sizeof(xlen) == 64 & extension("C")
 
 function clause execute (C_LDSP(uimm, rd)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -460,7 +460,9 @@ mapping clause assembly = C_LDSP(uimm, rd)
 union clause ast = C_SWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SWSP(ui76 @ ui52, rs2)
+      if extension("C")
   <-> 0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
+      if extension("C")
 
 function clause execute (C_SWSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -474,9 +476,9 @@ mapping clause assembly = C_SWSP(uimm, rs2)
 union clause ast = C_SDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2)
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
   <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
-      if sizeof(xlen) == 64
+      if sizeof(xlen) == 64 & extension("C")
 
 function clause execute (C_SDSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b000);
@@ -492,9 +494,9 @@ mapping clause assembly = C_SDSP(uimm, rs2)
 union clause ast = C_JR : (regidx)
 
 mapping clause encdec_compressed = C_JR(rs1)
-      if rs1 != zreg
+      if rs1 != zreg & extension("C")
   <-> 0b100 @ 0b0 @ rs1 : regidx @ 0b00000 @ 0b10
-      if rs1 != zreg
+      if rs1 != zreg & extension("C")
 
 function clause execute (C_JR(rs1)) =
   execute(RISCV_JALR(zero_extend(0b0), rs1, zreg))
@@ -508,9 +510,9 @@ mapping clause assembly = C_JR(rs1)
 union clause ast = C_JALR : (regidx)
 
 mapping clause encdec_compressed = C_JALR(rs1)
-      if rs1 != zreg
+      if rs1 != zreg & extension("C")
   <-> 0b100 @ 0b1 @ rs1 : regidx @ 0b00000 @ 0b10
-      if rs1 != zreg
+      if rs1 != zreg & extension("C")
 
 function clause execute (C_JALR(rs1)) =
   execute(RISCV_JALR(zero_extend(0b0), rs1, ra))
@@ -524,9 +526,9 @@ mapping clause assembly = C_JALR(rs1)
 union clause ast = C_MV : (regidx, regidx)
 
 mapping clause encdec_compressed = C_MV(rd, rs2)
-      if rd != zreg & rs2 != zreg
+      if rd != zreg & rs2 != zreg & extension("C")
   <-> 0b100 @ 0b0 @ rd : regidx @ rs2 : regidx @ 0b10
-      if rd != zreg & rs2 != zreg
+      if rd != zreg & rs2 != zreg & extension("C")
 
 function clause execute (C_MV(rd, rs2)) =
   execute(RTYPE(rs2, zreg, rd, RISCV_ADD))
@@ -539,8 +541,8 @@ mapping clause assembly = C_MV(rd, rs2)
 /* ****************************************************************** */
 union clause ast = C_EBREAK : unit
 
-mapping clause encdec_compressed = C_EBREAK()
-  <-> 0b100 @ 0b1 @ 0b00000 @ 0b00000 @ 0b10
+mapping clause encdec_compressed = C_EBREAK() if extension("C")
+  <-> 0b100 @ 0b1 @ 0b00000 @ 0b00000 @ 0b10 if extension("C")
 
 function clause execute C_EBREAK() =
   execute(EBREAK())
@@ -551,9 +553,9 @@ mapping clause assembly = C_EBREAK() <-> "c.ebreak"
 union clause ast = C_ADD : (regidx, regidx)
 
 mapping clause encdec_compressed = C_ADD(rsd, rs2)
-      if rsd != zreg & rs2 != zreg
+      if rsd != zreg & rs2 != zreg & extension("C")
   <-> 0b100 @ 0b1 @ rsd : regidx @ rs2 : regidx @ 0b10
-      if rsd != zreg & rs2 != zreg
+      if rsd != zreg & rs2 != zreg & extension("C")
 
 function clause execute (C_ADD(rsd, rs2)) =
   execute(RTYPE(rs2, rsd, rsd, RISCV_ADD))
diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail
index 71b1e0b25..6bf5cb3a8 100644
--- a/model/riscv_insts_cfext.sail
+++ b/model/riscv_insts_cfext.sail
@@ -17,9 +17,9 @@
 union clause ast = C_FLWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
   <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
 
 function clause execute (C_FLWSP(imm, rd)) = {
   let imm : bits(12) = zero_extend(imm @ 0b00);
@@ -35,9 +35,9 @@ mapping clause assembly = C_FLWSP(imm, rd)
 union clause ast = C_FSWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
   <-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
 
 function clause execute (C_FSWSP(uimm, rs2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -53,9 +53,9 @@ mapping clause assembly = C_FSWSP(uimm, rs2)
 union clause ast = C_FLW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
 
 function clause execute (C_FLW(uimm, rsc, rdc)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
@@ -73,9 +73,9 @@ mapping clause assembly = C_FLW(uimm, rsc, rdc)
 union clause ast = C_FSW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
   <-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
+      if sizeof(xlen) == 32 & extension("C") & extension("F")
 
 function clause execute (C_FSW(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = zero_extend(uimm @ 0b00);
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index 03b582434..dc8120c28 100644
--- a/model/riscv_insts_dext.sail
+++ b/model/riscv_insts_dext.sail
@@ -224,13 +224,13 @@ function fle_D   (v1,       v2,        is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()'                                  */
 
-function haveDoubleFPU() -> bool = haveDExt() | haveZdinx()
+function haveDoubleFPU() -> bool = extension("D") | extension("Zdinx")
 
 /* RV32Zdinx requires even register pairs; can be omitted for code  */
 /* not used for RV32Zdinx (i.e. RV64-only or D-only).               */
 val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, dec, regidx)) -> bool
 function validDoubleRegs(n, regs) = {
-  if haveZdinx() & sizeof(xlen) == 32 then
+  if extension("Zdinx") & sizeof(xlen) == 32 then
     foreach (i from 0 to (n - 1))
       if (regs[i][0] == bitone) then return false;
   true
@@ -902,11 +902,11 @@ mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D)                        if
 
 /* D instructions, RV64 only */
 
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D)                         if haveDExt() & sizeof(xlen) >= 64
-                    <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveDExt() & sizeof(xlen) >= 64
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D)                         if extension("D") & sizeof(xlen) >= 64
+                    <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("D") & sizeof(xlen) >= 64
 
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X)                         if haveDExt() & sizeof(xlen) >= 64
-                    <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveDExt() & sizeof(xlen) >= 64
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X)                         if extension("D") & sizeof(xlen) >= 64
+                    <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("D") & sizeof(xlen) >= 64
 
 /* Execution semantics ================================ */
 
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index 5c89e9188..834aee7bb 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -259,7 +259,7 @@ function fle_S   (v1,       v2,        is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()'                                  */
 
-function haveSingleFPU() -> bool = haveFExt() | haveZfinx()
+function haveSingleFPU() -> bool = extension("F") | extension("Zfinx")
 
 /* ****************************************************************** */
 /* Floating-point loads                                               */
@@ -271,14 +271,14 @@ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = LOAD_FP(imm, rs1, rd, HALF)          if haveZfh()
-                    <-> imm @ rs1 @ 0b001 @ rd @ 0b000_0111  if haveZfh()
+mapping clause encdec = LOAD_FP(imm, rs1, rd, HALF)          if extension("Zfh")
+                    <-> imm @ rs1 @ 0b001 @ rd @ 0b000_0111  if extension("Zfh")
 
-mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD)          if haveFExt()
-                    <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111  if haveFExt()
+mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD)          if extension("F")
+                    <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111  if extension("F")
 
-mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE)        if haveDExt()
-                    <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111  if haveDExt()
+mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE)        if extension("D")
+                    <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111  if extension("D")
 
 /* Execution semantics ================================ */
 
@@ -357,14 +357,14 @@ union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width)
 
 /* AST <-> Binary encoding ================================ */
 
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, HALF)                             if haveZfh()
-                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b001 @ imm5 : bits(5) @ 0b010_0111  if haveZfh()
+mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, HALF)                             if extension("Zfh")
+                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b001 @ imm5 : bits(5) @ 0b010_0111  if extension("Zfh")
 
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD)                             if haveFExt()
-                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111  if haveFExt()
+mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD)                             if extension("F")
+                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111  if extension("F")
 
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)                           if haveDExt()
-                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111  if haveDExt()
+mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)                           if extension("D")
+                    <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111  if extension("D")
 
 /* Execution semantics ================================ */
 
@@ -1024,11 +1024,11 @@ union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S)
 mapping clause encdec = F_UN_TYPE_S(rs1, rd, FCLASS_S)                        if haveSingleFPU()
                     <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveSingleFPU()
 
-mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W)                         if haveFExt()
-                    <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveFExt()
+mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W)                         if extension("F")
+                    <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("F")
 
-mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X)                         if haveFExt()
-                    <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveFExt()
+mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X)                         if extension("F")
+                    <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("F")
 
 /* Execution semantics ================================ */
 
diff --git a/model/riscv_insts_hints.sail b/model/riscv_insts_hints.sail
index ceddcf28a..d4f8b83d5 100644
--- a/model/riscv_insts_hints.sail
+++ b/model/riscv_insts_hints.sail
@@ -20,7 +20,7 @@ mapping clause encdec_compressed = C_NOP_HINT(im5 @ im40)
 
 function clause execute C_NOP_HINT(imm) = RETIRE_SUCCESS
 
-mapping clause assembly = C_NOP_HINT(imm) <-> "c.nop.hint." ^ hex_bits_6(imm)
+mapping clause assembly = C_NOP_HINT(imm) <-> "c.nop.hint." ^ spc() ^ hex_bits_6(imm)
 
 /* ****************************************************************** */
 union clause ast = C_ADDI_HINT : (regidx)
@@ -34,7 +34,7 @@ function clause execute (C_ADDI_HINT(rsd)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_ADDI_HINT(rsd)
       if rsd != zreg
-  <-> "c.addi.hint." ^ reg_name(rsd)
+  <-> "c.addi.hint." ^ spc() ^ reg_name(rsd)
       if rsd != zreg
 
 /* ****************************************************************** */
@@ -46,7 +46,7 @@ mapping clause encdec_compressed = C_LI_HINT(imm5 @ imm40)
 function clause execute (C_LI_HINT(imm)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_LI_HINT(imm)
-  <-> "c.li.hint." ^ hex_bits_6(imm)
+  <-> "c.li.hint." ^ spc() ^ hex_bits_6(imm)
 
 /* ****************************************************************** */
 union clause ast = C_LUI_HINT : (bits(6))
@@ -60,7 +60,7 @@ function clause execute (C_LUI_HINT(imm)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_LUI_HINT(imm)
       if imm != 0b000000
-  <-> "c.lui.hint." ^ hex_bits_6(imm)
+  <-> "c.lui.hint." ^ spc() ^ hex_bits_6(imm)
       if imm != 0b000000
 
 /* ****************************************************************** */
@@ -75,7 +75,7 @@ function clause execute (C_MV_HINT(rs2)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_MV_HINT(rs2)
       if rs2 != zreg
-  <-> "c.mv.hint." ^ reg_name(rs2)
+  <-> "c.mv.hint." ^ spc() ^ reg_name(rs2)
       if rs2 != zreg
 
 /* ****************************************************************** */
@@ -90,7 +90,7 @@ function clause execute (C_ADD_HINT(rs2)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_ADD_HINT(rs2)
       if rs2 != zreg
-  <-> "c.add.hint." ^ reg_name(rs2)
+  <-> "c.add.hint." ^ spc() ^ reg_name(rs2)
       if rs2 != zreg
 
 /* ****************************************************************** */
@@ -105,7 +105,7 @@ function clause execute (C_SLLI_HINT(shamt, rsd)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_SLLI_HINT(shamt, rsd)
       if shamt == 0b000000 | rsd == zreg
-  <-> "c.slli.hint." ^ reg_name(rsd) ^ "." ^ hex_bits_6(shamt)
+  <-> "c.slli.hint." ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(shamt)
       if shamt == 0b000000 | rsd == zreg
 
 /* ****************************************************************** */
@@ -117,7 +117,7 @@ mapping clause encdec_compressed = C_SRLI_HINT(rsd)
 function clause execute (C_SRLI_HINT(rsd)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_SRLI_HINT(rsd)
-  <-> "c.srli.hint." ^ creg_name(rsd)
+  <-> "c.srli.hint." ^ spc() ^ creg_name(rsd)
 
 /* ****************************************************************** */
 union clause ast = C_SRAI_HINT : (cregidx)
@@ -128,7 +128,7 @@ mapping clause encdec_compressed = C_SRAI_HINT(rsd)
 function clause execute (C_SRAI_HINT(rsd)) = RETIRE_SUCCESS
 
 mapping clause assembly = C_SRAI_HINT(rsd)
-  <-> "c.srai.hint." ^ creg_name(rsd)
+  <-> "c.srai.hint." ^ spc() ^ creg_name(rsd)
 
 /* ****************************************************************** */
 /* The reserved fences are not really hints, but for now they
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index cfac3bb31..27483be17 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -20,8 +20,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 extension("M") | extension("Zmmul")
+  <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if extension("M") | extension("Zmmul")
 
 function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
   let rs1_val = X(rs1);
@@ -49,8 +49,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 extension("M")
+  <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if extension("M")
 
 function clause execute (DIV(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1);
@@ -75,8 +75,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 extension("M")
+  <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if extension("M")
 
 function clause execute (REM(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1);
@@ -96,9 +96,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 & (extension("M") | extension("Zmmul"))
   <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-      if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
+      if sizeof(xlen) == 64 & (extension("M") | extension("Zmmul"))
 
 function clause execute (MULW(rs2, rs1, rd)) = {
   let rs1_val = X(rs1)[31..0];
@@ -121,9 +121,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 & extension("M")
   <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
-      if sizeof(xlen) == 64 & haveMulDiv()
+      if sizeof(xlen) == 64 & extension("M")
 
 function clause execute (DIVW(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1)[31..0];
@@ -146,9 +146,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 & extension("M")
   <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
-      if sizeof(xlen) == 64 & haveMulDiv()
+      if sizeof(xlen) == 64 & extension("M")
 
 function clause execute (REMW(rs2, rs1, rd, s)) = {
   let rs1_val = X(rs1)[31..0];
diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail
index dd9197adb..2864081e9 100644
--- a/model/riscv_insts_next.sail
+++ b/model/riscv_insts_next.sail
@@ -15,7 +15,7 @@ mapping clause encdec = URET()
   <-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute URET() = {
-  if   not(haveUsrMode()) | not(sys_enable_next())
+  if   not(extension("U")) | not(sys_enable_next())
   then handle_illegal()
   else if not(ext_check_xret_priv(User))
   then ext_fail_xret_priv()
diff --git a/model/riscv_insts_svinval.sail b/model/riscv_insts_svinval.sail
index 168fb17ff..66eaafe2e 100644
--- a/model/riscv_insts_svinval.sail
+++ b/model/riscv_insts_svinval.sail
@@ -9,8 +9,8 @@
 union clause ast = SINVAL_VMA : (regidx, regidx)
 
 mapping clause encdec =
-      SINVAL_VMA(rs1, rs2)                                                  if haveSvinval()
-  <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+      SINVAL_VMA(rs1, rs2)                                                  if extension("Svinval")
+  <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval")
 
 function clause execute SINVAL_VMA(rs1, rs2) = {
   execute(SFENCE_VMA(rs1, rs2))
@@ -24,8 +24,8 @@ mapping clause assembly = SINVAL_VMA(rs1, rs2)
 union clause ast = SFENCE_W_INVAL : unit
 
 mapping clause encdec =
-      SFENCE_W_INVAL()                                            if haveSvinval()
-  <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+      SFENCE_W_INVAL()                                            if extension("Svinval")
+  <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval")
 
 function clause execute SFENCE_W_INVAL() = {
   if cur_privilege == User
@@ -40,8 +40,8 @@ mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval"
 union clause ast = SFENCE_INVAL_IR : unit
 
 mapping clause encdec =
-      SFENCE_INVAL_IR()                                           if haveSvinval()
-  <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+      SFENCE_INVAL_IR()                                           if extension("Svinval")
+  <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval")
 
 function clause execute SFENCE_INVAL_IR() = {
   if cur_privilege == User
diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail
index 6104e7ee4..e6d26cecc 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 extension("V")
+  <-> encdec_vvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_nvsfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_nvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b1 @ 0b00000 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_nxsfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_nxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vxsgfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_nisfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_nifunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_visgfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b1 @ 0b00000 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b100111 @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_mvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_mvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_wvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_wvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_wmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010010 @ vm @ vs2 @ vext2_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010010 @ vm @ vs2 @ vext4_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010010 @ vm @ vs2 @ vext8_vs1(funct6) @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b010 @ rd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_mvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_mvxmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_wvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_wxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_wmvxfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b110 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b110 @ vd @ 0b1010111 if extension("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..a88f64a97 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 extension("V")
+  <-> encdec_fvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fwvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fwvvmafunct6(funct6) @ vm @ vs1 @ vs2 @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fwvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010010 @ vm @ vs2 @ encdec_vfunary0_vs1(vfunary0) @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010010 @ vm @ vs2 @ encdec_vfwunary0_vs1(vfwunary0) @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010010 @ vm @ vs2 @ encdec_vfnunary0_vs1(vfnunary0) @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010011 @ vm @ vs2 @ encdec_vfunary1_vs1(vfunary1) @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b001 @ rd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fwvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fwvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fwffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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..87b425e63 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 extension("V")
+  <-> encdec_mmfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010000 @ vm @ vs2 @ 0b10000 @ 0b010 @ rd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010000 @ vm @ vs2 @ 0b10001 @ 0b010 @ rd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010100 @ vm @ vs2 @ 0b00001 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010100 @ vm @ vs2 @ 0b00011 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010100 @ vm @ vs2 @ 0b00010 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010100 @ vm @ vs2 @ 0b10000 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> 0b010100 @ vm @ 0b00000 @ 0b10001 @ 0b010 @ vd @ 0b1010111 if extension("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..96ade62b2 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 extension("V")
+  <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b11 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extension("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 extension("V")
+  <-> nf @ 0b0 @ 0b00 @ 0b1 @ 0b01000 @ rs1 @ 0b000 @ vs3 @ 0b0100111 if extension("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 extension("V")
+  <-> 0b000 @ 0b0 @ 0b00 @ 0b1 @ 0b01011 @ rs1 @ 0b000 @ vd_or_vs3 @ encdec_lsop(op) if extension("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..bdeb0f2b3 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 extension("V")
+  <-> encdec_rivvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_rmvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b010 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extension("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..4cb7cc73b 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 extension("V")
+  <-> encdec_vvmfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vvmcfunct6(funct6) @ 0b1 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vvmsfunct6(funct6) @ 0b0 @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vvcmpfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b000 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vxmfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vxmcfunct6(funct6) @ 0b1 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vxmsfunct6(funct6) @ 0b0 @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vxcmpfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b100 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vimfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vimcfunct6(funct6) @ 0b1 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vimsfunct6(funct6) @ 0b0 @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_vicmpfunct6(funct6) @ vm @ vs2 @ simm @ 0b011 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extension("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 extension("V")
+  <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if extension("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..236d1d062 100644
--- a/model/riscv_insts_vext_vset.sail
+++ b/model/riscv_insts_vext_vset.sail
@@ -65,8 +65,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 extension("V")
+  <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if extension("V")
 
 function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
   let LMUL_pow_ori  = get_lmul_pow();
@@ -116,8 +116,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 extension("V")
+  <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if extension("V")
 
 function clause execute VSETVL(rs2, rs1, rd) = {
   let LMUL_pow_ori  = get_lmul_pow();
@@ -167,8 +167,8 @@ mapping clause assembly = VSETVL(rs2, rs1, rd)
 /* ********************************** vsetivli *********************************** */
 union clause ast = VSETIVLI : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx)
 
-mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if haveVExt()
-  <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt()
+mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extension("V")
+  <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if extension("V")
 
 function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
   /* set vtype */
diff --git a/model/riscv_insts_zba.sail b/model/riscv_insts_zba.sail
index 4f078d342..de8ad4544 100644
--- a/model/riscv_insts_zba.sail
+++ b/model/riscv_insts_zba.sail
@@ -9,8 +9,8 @@
 /* ****************************************************************** */
 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 extension("Zba") & sizeof(xlen) == 64
+  <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if extension("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 +25,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 extension("Zba") & sizeof(xlen) == 64
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if extension("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 extension("Zba") & sizeof(xlen) == 64
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if extension("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 extension("Zba") & sizeof(xlen) == 64
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extension("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 extension("Zba") & sizeof(xlen) == 64
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if extension("Zba") & sizeof(xlen) == 64
 
 mapping zba_rtypeuw_mnemonic : bropw_zba <-> string = {
   RISCV_ADDUW    <-> "add.uw",
@@ -64,12 +64,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 extension("Zba")
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if extension("Zba")
+mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH2ADD) if extension("Zba")
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extension("Zba")
+mapping clause encdec = ZBA_RTYPE(rs2, rs1, rd, RISCV_SH3ADD) if extension("Zba")
+  <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extension("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 d39afc00b..9c961665a 100644
--- a/model/riscv_insts_zbb.sail
+++ b/model/riscv_insts_zbb.sail
@@ -9,8 +9,8 @@
 /* ****************************************************************** */
 union clause ast = RISCV_RORIW : (bits(5), regidx, regidx)
 
-mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
-  <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 64
+  <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (extension("Zbb") | extension("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)
@@ -25,8 +25,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() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
-  <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (extension("Zbb") | extension("Zbkb")) & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+  <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (extension("Zbb") | extension("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)
@@ -43,11 +43,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() | haveZbkb()) & sizeof(xlen) == 64
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 64
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 64
 
-mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 64
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 64
 
 mapping zbb_rtypew_mnemonic : bropw_zbb <-> string = {
   RISCV_ROLW <-> "rolw",
@@ -71,32 +71,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() | haveZbkb()
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ANDN) if extension("Zbb") | extension("Zbkb")
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extension("Zbb") | extension("Zbkb")
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if haveZbb() | haveZbkb()
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ORN) if extension("Zbb") | extension("Zbkb")
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extension("Zbb") | extension("Zbkb")
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if haveZbb() | haveZbkb()
-  <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_XNOR) if extension("Zbb") | extension("Zbkb")
+  <-> 0b0100000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extension("Zbb") | extension("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 extension("Zbb")
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 if extension("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 extension("Zbb")
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extension("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 extension("Zbb")
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extension("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 extension("Zbb")
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extension("Zbb")
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if haveZbb() | haveZbkb()
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROL) if extension("Zbb") | extension("Zbkb")
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extension("Zbb") | extension("Zbkb")
 
-mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if haveZbb() | haveZbkb()
-  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbb() | haveZbkb()
+mapping clause encdec = ZBB_RTYPE(rs2, rs1, rd, RISCV_ROR) if extension("Zbb") | extension("Zbkb")
+  <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extension("Zbb") | extension("Zbkb")
 
 mapping zbb_rtype_mnemonic : brop_zbb <-> string = {
   RISCV_ANDN <-> "andn",
@@ -138,17 +138,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 extension("Zbb")
+  <-> 0b0110000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("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 extension("Zbb")
+  <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("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 extension("Zbb") & sizeof(xlen) == 32
+  <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if extension("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 extension("Zbb") & sizeof(xlen) == 64
+  <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if extension("Zbb") & sizeof(xlen) == 64
 
 mapping zbb_extop_mnemonic : extop_zbb <-> string = {
   RISCV_SEXTB <-> "sext.b",
@@ -173,11 +173,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() | haveZbkb()) & sizeof(xlen) == 32
-  <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 32
+mapping clause encdec = RISCV_REV8(rs1, rd) if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 32
+  <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 32
 
-mapping clause encdec = RISCV_REV8(rs1, rd) if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
-  <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (haveZbb() | haveZbkb()) & sizeof(xlen) == 64
+mapping clause encdec = RISCV_REV8(rs1, rd) if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 64
+  <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extension("Zbb") | extension("Zbkb")) & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_REV8(rs1, rd)
   <-> "rev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -194,8 +194,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 extension("Zbb")
+  <-> 0b001010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extension("Zbb")
 
 mapping clause assembly = RISCV_ORCB(rs1, rd)
   <-> "orc.b" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -214,8 +214,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 extension("Zbb")
+  <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zbb")
 
 mapping clause assembly = RISCV_CPOP(rs1, rd)
   <-> "cpop" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -232,8 +232,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 extension("Zbb") & sizeof(xlen) == 64
+  <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if extension("Zbb") & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_CPOPW(rs1, rd)
   <-> "cpopw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -250,8 +250,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 extension("Zbb")
+  <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zbb")
 
 mapping clause assembly = RISCV_CLZ(rs1, rd)
   <-> "clz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -271,8 +271,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 extension("Zbb") & sizeof(xlen) == 64
+  <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if extension("Zbb") & sizeof(xlen) == 64
 
 mapping clause assembly = RISCV_CLZW(rs1, rd)
   <-> "clzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -292,8 +292,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 extension("Zbb")
+  <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zbb")
 
 mapping clause assembly = RISCV_CTZ(rs1, rd)
   <-> "ctz" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -313,8 +313,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 extension("Zbb") & sizeof(xlen) == 64
+  <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if extension("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_zbc.sail b/model/riscv_insts_zbc.sail
index 458b9faf0..ca530000f 100644
--- a/model/riscv_insts_zbc.sail
+++ b/model/riscv_insts_zbc.sail
@@ -9,8 +9,8 @@
 /* ****************************************************************** */
 union clause ast = RISCV_CLMUL : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_CLMUL(rs2, rs1, rd) if haveZbc() | haveZbkc()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbc() | haveZbkc()
+mapping clause encdec = RISCV_CLMUL(rs2, rs1, rd) if extension("Zbc") | extension("Zbkc")
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extension("Zbc") | extension("Zbkc")
 
 mapping clause assembly = RISCV_CLMUL(rs2, rs1, rd)
   <-> "clmul" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
@@ -28,8 +28,8 @@ function clause execute (RISCV_CLMUL(rs2, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CLMULH : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_CLMULH(rs2, rs1, rd) if haveZbc() | haveZbkc()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b0110011 if haveZbc() | haveZbkc()
+mapping clause encdec = RISCV_CLMULH(rs2, rs1, rd) if extension("Zbc") | extension("Zbkc")
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b0110011 if extension("Zbc") | extension("Zbkc")
 
 mapping clause assembly = RISCV_CLMULH(rs2, rs1, rd)
   <-> "clmulh" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
@@ -47,8 +47,8 @@ function clause execute (RISCV_CLMULH(rs2, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_CLMULR : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_CLMULR(rs2, rs1, rd) if haveZbc()
-  <-> 0b0000101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZbc()
+mapping clause encdec = RISCV_CLMULR(rs2, rs1, rd) if extension("Zbc")
+  <-> 0b0000101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if extension("Zbc")
 
 mapping clause assembly = RISCV_CLMULR(rs2, rs1, rd)
   <-> "clmulr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail
index f6246d17a..2919f80d9 100644
--- a/model/riscv_insts_zbkb.sail
+++ b/model/riscv_insts_zbkb.sail
@@ -9,11 +9,11 @@
 /* ****************************************************************** */
 union clause ast = ZBKB_RTYPE : (regidx, regidx, regidx, brop_zbkb)
 
-mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACK) if haveZbkb()
-  <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbkb()
+mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACK) if extension("Zbkb")
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extension("Zbkb")
 
-mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACKH) if haveZbkb()
-  <-> 0b0000100 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZbkb()
+mapping clause encdec = ZBKB_RTYPE(rs2, rs1, rd, RISCV_PACKH) if extension("Zbkb")
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extension("Zbkb")
 
 mapping zbkb_rtype_mnemonic : brop_zbkb <-> string = {
   RISCV_PACK  <-> "pack",
@@ -37,8 +37,8 @@ function clause execute (ZBKB_RTYPE(rs2, rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = ZBKB_PACKW : (regidx, regidx, regidx)
 
-mapping clause encdec = ZBKB_PACKW(rs2, rs1, rd) if haveZbkb() & sizeof(xlen) == 64
-  <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if haveZbkb() & sizeof(xlen) == 64
+mapping clause encdec = ZBKB_PACKW(rs2, rs1, rd) if extension("Zbkb") & sizeof(xlen) == 64
+  <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extension("Zbkb") & sizeof(xlen) == 64
 
 mapping clause assembly = ZBKB_PACKW(rs2, rs1, rd)
   <-> "packw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
@@ -55,8 +55,8 @@ function clause execute (ZBKB_PACKW(rs2, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_ZIP : (regidx, regidx)
 
-mapping clause encdec = RISCV_ZIP(rs1, rd) if haveZbkb() & sizeof(xlen) == 32
-  <-> 0b000010001111 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbkb() & sizeof(xlen) == 32
+mapping clause encdec = RISCV_ZIP(rs1, rd) if extension("Zbkb") & sizeof(xlen) == 32
+  <-> 0b000010001111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zbkb") & sizeof(xlen) == 32
 
 mapping clause assembly = RISCV_ZIP(rs1, rd)
   <-> "zip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -76,8 +76,8 @@ function clause execute (RISCV_ZIP(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_UNZIP : (regidx, regidx)
 
-mapping clause encdec = RISCV_UNZIP(rs1, rd) if haveZbkb() & sizeof(xlen) == 32
-  <-> 0b000010001111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbkb() & sizeof(xlen) == 32
+mapping clause encdec = RISCV_UNZIP(rs1, rd) if extension("Zbkb") & sizeof(xlen) == 32
+  <-> 0b000010001111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extension("Zbkb") & sizeof(xlen) == 32
 
 mapping clause assembly = RISCV_UNZIP(rs1, rd)
   <-> "unzip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -97,8 +97,8 @@ function clause execute (RISCV_UNZIP(rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_BREV8 : (regidx, regidx)
 
-mapping clause encdec = RISCV_BREV8(rs1, rd) if haveZbkb()
-  <-> 0b011010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbkb()
+mapping clause encdec = RISCV_BREV8(rs1, rd) if extension("Zbkb")
+  <-> 0b011010000111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extension("Zbkb")
 
 mapping clause assembly = RISCV_BREV8(rs1, rd)
   <-> "brev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail
index d19a2b15d..e89c0abf3 100644
--- a/model/riscv_insts_zbkx.sail
+++ b/model/riscv_insts_zbkx.sail
@@ -9,8 +9,8 @@
 /* ****************************************************************** */
 union clause ast = RISCV_XPERM8 : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_XPERM8(rs2, rs1, rd) if haveZbkx()
-  <-> 0b0010100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if haveZbkx()
+mapping clause encdec = RISCV_XPERM8(rs2, rs1, rd) if extension("Zbkx")
+  <-> 0b0010100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0110011 if extension("Zbkx")
 
 mapping clause assembly = RISCV_XPERM8(rs2, rs1, rd)
   <-> "xperm8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
@@ -32,8 +32,8 @@ function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = {
 /* ****************************************************************** */
 union clause ast = RISCV_XPERM4 : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_XPERM4(rs2, rs1, rd) if haveZbkx()
-  <-> 0b0010100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if haveZbkx()
+mapping clause encdec = RISCV_XPERM4(rs2, rs1, rd) if extension("Zbkx")
+  <-> 0b0010100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0110011 if extension("Zbkx")
 
 mapping clause assembly = RISCV_XPERM4(rs2, rs1, rd)
   <-> "xperm4" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail
index b535701c8..8c73c62e4 100644
--- a/model/riscv_insts_zbs.sail
+++ b/model/riscv_insts_zbs.sail
@@ -9,17 +9,17 @@
 /* ****************************************************************** */
 union clause ast = ZBS_IOP : (bits(6), regidx, regidx, biop_zbs)
 
-mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
-  <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+  <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
 
-mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
-  <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+  <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
 
-mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
-  <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+  <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
 
-mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
-  <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZbs() & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
+  <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zbs") & (sizeof(xlen) == 64 | shamt[5] == bitzero)
 
 mapping zbs_iop_mnemonic : biop_zbs <-> string = {
   RISCV_BCLRI <-> "bclri",
@@ -49,17 +49,17 @@ function clause execute (ZBS_IOP(shamt, rs1, rd, op)) = {
 /* ****************************************************************** */
 union clause ast = ZBS_RTYPE : (regidx, regidx, regidx, brop_zbs)
 
-mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BCLR) if haveZbs()
-  <-> 0b0100100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs()
+mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BCLR) if extension("Zbs")
+  <-> 0b0100100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extension("Zbs")
 
-mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BEXT) if haveZbs()
-  <-> 0b0100100 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZbs()
+mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BEXT) if extension("Zbs")
+  <-> 0b0100100 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extension("Zbs")
 
-mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BINV) if haveZbs()
-  <-> 0b0110100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs()
+mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BINV) if extension("Zbs")
+  <-> 0b0110100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extension("Zbs")
 
-mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BSET) if haveZbs()
-  <-> 0b0010100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if haveZbs()
+mapping clause encdec = ZBS_RTYPE(rs2, rs1, rd, RISCV_BSET) if extension("Zbs")
+  <-> 0b0010100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0110011 if extension("Zbs")
 
 mapping zbs_rtype_mnemonic : brop_zbs <-> string = {
   RISCV_BCLR    <-> "bclr",
diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail
index 86253bff4..0fac41077 100644
--- a/model/riscv_insts_zcb.sail
+++ b/model/riscv_insts_zcb.sail
@@ -9,8 +9,8 @@
 union clause ast = C_LBU : (bits(2), cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_LBU(uimm1 @ uimm0, rdc, rs1c)                                                           if haveZcb()
-  <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb()
+      C_LBU(uimm1 @ uimm0, rdc, rs1c)                                                           if extension("Zcb")
+  <-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb")
 
 mapping clause assembly = C_LBU(uimm, rdc, rs1c) <->
   "c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
@@ -27,8 +27,8 @@ function clause execute C_LBU(uimm, rdc, rs1c) = {
 union clause ast = C_LHU : (bits(2), cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_LHU(uimm1 @ 0b0, rdc, rs1c)                                                 if haveZcb()
-  <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb()
+      C_LHU(uimm1 @ 0b0, rdc, rs1c)                                                 if extension("Zcb")
+  <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb")
 
 mapping clause assembly = C_LHU(uimm, rdc, rs1c) <->
   "c.lhu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
@@ -45,8 +45,8 @@ function clause execute C_LHU(uimm, rdc, rs1c) = {
 union clause ast = C_LH : (bits(2), cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_LH(uimm1 @ 0b0, rdc, rs1c)                                                  if haveZcb()
-  <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb()
+      C_LH(uimm1 @ 0b0, rdc, rs1c)                                                  if extension("Zcb")
+  <-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb")
 
 mapping clause assembly = C_LH(uimm, rdc, rs1c) <->
   "c.lh" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
@@ -63,8 +63,8 @@ function clause execute C_LH(uimm, rdc, rs1c) = {
 union clause ast = C_SB : (bits(2), cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_SB(uimm1 @ uimm0, rs1c, rs2c)                                                  if haveZcb()
-  <-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if haveZcb()
+      C_SB(uimm1 @ uimm0, rs1c, rs2c)                                                  if extension("Zcb")
+  <-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if extension("Zcb")
 
 mapping clause assembly = C_SB(uimm, rs1c, rs2c) <->
   "c.sb" ^ spc() ^ creg_name(rs2c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
@@ -81,8 +81,8 @@ function clause execute C_SB(uimm, rs1c, rs2c) = {
 union clause ast = C_SH : (bits(2), cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_SH(uimm1 @ 0b0, rs1c, rs2c)                                                  if haveZcb()
-  <-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if haveZcb()
+      C_SH(uimm1 @ 0b0, rs1c, rs2c)                                                  if extension("Zcb")
+  <-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if extension("Zcb")
 
 mapping clause assembly = C_SH(uimm, rs1c, rs2c) <->
   "c.sh" ^ spc() ^ creg_name(rs1c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs2c) ^ opt_spc() ^ ")"
@@ -99,8 +99,8 @@ function clause execute C_SH(uimm, rs1c, rs2c) = {
 union clause ast = C_ZEXT_B : (cregidx)
 
 mapping clause encdec_compressed =
-      C_ZEXT_B(rsdc)                                       if haveZcb()
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if haveZcb()
+      C_ZEXT_B(rsdc)                                       if extension("Zcb")
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if extension("Zcb")
 
 mapping clause assembly = C_ZEXT_B(rsdc) <->
   "c.zext.b" ^ spc() ^ creg_name(rsdc)
@@ -116,8 +116,8 @@ function clause execute C_ZEXT_B(rsdc) = {
 union clause ast = C_SEXT_B : (cregidx)
 
 mapping clause encdec_compressed =
-      C_SEXT_B(rsdc)                                       if haveZcb() & haveZbb()
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if haveZcb() & haveZbb()
+      C_SEXT_B(rsdc)                                       if extension("Zcb") & extension("Zbb")
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if extension("Zcb") & extension("Zbb")
 
 mapping clause assembly = C_SEXT_B(rsdc) <->
   "c.sext.b" ^ spc() ^ creg_name(rsdc)
@@ -132,8 +132,8 @@ function clause execute C_SEXT_B(rsdc) = {
 union clause ast = C_ZEXT_H : (cregidx)
 
 mapping clause encdec_compressed =
-      C_ZEXT_H(rsdc)                                       if haveZcb() & haveZbb()
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if haveZcb() & haveZbb()
+      C_ZEXT_H(rsdc)                                       if extension("Zcb") & extension("Zbb")
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if extension("Zcb") & extension("Zbb")
 
 mapping clause assembly = C_ZEXT_H(rsdc) <->
   "c.zext.h" ^ spc() ^ creg_name(rsdc)
@@ -148,8 +148,8 @@ function clause execute C_ZEXT_H(rsdc) = {
 union clause ast = C_SEXT_H : (cregidx)
 
 mapping clause encdec_compressed =
-      C_SEXT_H(rsdc)                                       if haveZcb() & haveZbb()
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if haveZcb() & haveZbb()
+      C_SEXT_H(rsdc)                                       if extension("Zcb") & extension("Zbb")
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if extension("Zcb") & extension("Zbb")
 
 mapping clause assembly = C_SEXT_H(rsdc) <->
   "c.sext.h" ^ spc() ^ creg_name(rsdc)
@@ -164,8 +164,8 @@ function clause execute C_SEXT_H(rsdc) = {
 union clause ast = C_ZEXT_W : (cregidx)
 
 mapping clause encdec_compressed =
-      C_ZEXT_W(rsdc)                                       if haveZcb() & haveZba() & sizeof(xlen) == 64
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if haveZcb() & haveZba() & sizeof(xlen) == 64
+      C_ZEXT_W(rsdc)                                       if extension("Zcb") & extension("Zba") & sizeof(xlen) == 64
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if extension("Zcb") & extension("Zba") & sizeof(xlen) == 64
 
 mapping clause assembly = C_ZEXT_W(rsdc) <->
   "c.zext.w" ^ spc() ^ creg_name(rsdc)
@@ -180,8 +180,8 @@ function clause execute C_ZEXT_W(rsdc) = {
 union clause ast = C_NOT : (cregidx)
 
 mapping clause encdec_compressed =
-      C_NOT(rsdc)                                          if haveZcb()
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if haveZcb()
+      C_NOT(rsdc)                                          if extension("Zcb")
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if extension("Zcb")
 
 mapping clause assembly = C_NOT(rsdc) <->
   "c.not" ^ spc() ^ creg_name(rsdc)
@@ -197,8 +197,8 @@ function clause execute C_NOT(rsdc) = {
 union clause ast = C_MUL : (cregidx, cregidx)
 
 mapping clause encdec_compressed =
-      C_MUL(rsdc, rs2c)                                             if haveZcb() & (haveMulDiv() | haveZmmul())
-  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (haveMulDiv() | haveZmmul())
+      C_MUL(rsdc, rs2c)                                             if extension("Zcb") & (extension("M") | extension("Zmmul"))
+  <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if extension("Zcb") & (extension("M") | extension("Zmmul"))
 
 mapping clause assembly = C_MUL(rsdc, rs2c) <->
   "c.mul" ^ spc() ^ creg_name(rsdc) ^ sep() ^ creg_name(rs2c)
diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail
index 1443daf3d..f20573250 100644
--- a/model/riscv_insts_zfa.sail
+++ b/model/riscv_insts_zfa.sail
@@ -10,8 +10,8 @@
 
 union clause ast = RISCV_FLI_H : (bits(5), regidx)
 
-mapping clause encdec = RISCV_FLI_H(rs1, rd)                if haveZfh() & haveZfa()
-  <-> 0b111_1010 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfh() & haveZfa()
+mapping clause encdec = RISCV_FLI_H(rs1, rd)                if extension("Zfh") & extension("Zfa")
+  <-> 0b111_1010 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("Zfh") & extension("Zfa")
 
 mapping clause assembly = RISCV_FLI_H(constantidx, rd)
   <-> "fli.h" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx)
@@ -59,8 +59,8 @@ function clause execute (RISCV_FLI_H(constantidx, rd)) = {
 
 union clause ast = RISCV_FLI_S : (bits(5), regidx)
 
-mapping clause encdec = RISCV_FLI_S(rs1, rd)                if haveZfa()
-  <-> 0b111_1000 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfa()
+mapping clause encdec = RISCV_FLI_S(rs1, rd)                if extension("Zfa")
+  <-> 0b111_1000 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("Zfa")
 
 mapping clause assembly = RISCV_FLI_S(constantidx, rd)
   <-> "fli.s" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx)
@@ -108,8 +108,8 @@ function clause execute (RISCV_FLI_S(constantidx, rd)) = {
 
 union clause ast = RISCV_FLI_D : (bits(5), regidx)
 
-mapping clause encdec = RISCV_FLI_D(rs1, rd)                if haveDExt() & haveZfa()
-  <-> 0b111_1001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FLI_D(rs1, rd)                if extension("D") & extension("Zfa")
+  <-> 0b111_1001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FLI_D(constantidx, rd)
   <-> "fli.d" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx)
@@ -157,8 +157,8 @@ function clause execute (RISCV_FLI_D(constantidx, rd)) = {
 
 union clause ast = RISCV_FMINM_H : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FMINM_H(rs2, rs1, rd)     if haveZfh() & haveZfa()
-  <-> 0b001_0110 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveZfh() & haveZfa()
+mapping clause encdec = RISCV_FMINM_H(rs2, rs1, rd)     if extension("Zfh") & extension("Zfa")
+  <-> 0b001_0110 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if extension("Zfh") & extension("Zfa")
 
 mapping clause assembly = RISCV_FMINM_H(rs2, rs1, rd)
   <-> "fminm.h" ^ spc() ^ freg_name(rd)
@@ -187,8 +187,8 @@ function clause execute (RISCV_FMINM_H(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FMAXM_H : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FMAXM_H(rs2, rs1, rd)     if haveZfh() & haveZfa()
-  <-> 0b001_0110 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011  if haveZfh() & haveZfa()
+mapping clause encdec = RISCV_FMAXM_H(rs2, rs1, rd)     if extension("Zfh") & extension("Zfa")
+  <-> 0b001_0110 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011  if extension("Zfh") & extension("Zfa")
 
 mapping clause assembly = RISCV_FMAXM_H(rs2, rs1, rd)
   <-> "fmaxm.h" ^ spc() ^ freg_name(rd)
@@ -217,8 +217,8 @@ function clause execute (RISCV_FMAXM_H(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FMINM_S : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FMINM_S(rs2, rs1, rd)     if haveZfa()
-  <-> 0b001_0100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveZfa()
+mapping clause encdec = RISCV_FMINM_S(rs2, rs1, rd)     if extension("Zfa")
+  <-> 0b001_0100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if extension("Zfa")
 
 mapping clause assembly = RISCV_FMINM_S(rs2, rs1, rd)
   <-> "fminm.s" ^ spc() ^ freg_name(rd)
@@ -247,8 +247,8 @@ function clause execute (RISCV_FMINM_S(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FMAXM_S : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FMAXM_S(rs2, rs1, rd)     if haveZfa()
-  <-> 0b001_0100 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011  if haveZfa()
+mapping clause encdec = RISCV_FMAXM_S(rs2, rs1, rd)     if extension("Zfa")
+  <-> 0b001_0100 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011  if extension("Zfa")
 
 mapping clause assembly = RISCV_FMAXM_S(rs2, rs1, rd)
   <-> "fmaxm.s" ^ spc() ^ freg_name(rd)
@@ -277,8 +277,8 @@ function clause execute (RISCV_FMAXM_S(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FMINM_D : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FMINM_D(rs2, rs1, rd)     if haveDExt() & haveZfa()
-  <-> 0b001_0101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FMINM_D(rs2, rs1, rd)     if extension("D") & extension("Zfa")
+  <-> 0b001_0101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011  if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FMINM_D(rs2, rs1, rd)
   <-> "fminm.d" ^ spc() ^ freg_name(rd)
@@ -307,8 +307,8 @@ function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FMAXM_D : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FMAXM_D(rs2, rs1, rd)     if haveDExt() & haveZfa()
-  <-> 0b001_0101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011  if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FMAXM_D(rs2, rs1, rd)     if extension("D") & extension("Zfa")
+  <-> 0b001_0101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011  if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FMAXM_D(rs2, rs1, rd)
   <-> "fmaxm.d" ^ spc() ^ freg_name(rd)
@@ -337,8 +337,8 @@ function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FROUND_H : (regidx, rounding_mode, regidx)
 
-mapping clause encdec = RISCV_FROUND_H(rs1, rm, rd)                           if haveZfh() & haveZfa()
-  <-> 0b010_0010 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfh() & haveZfa()
+mapping clause encdec = RISCV_FROUND_H(rs1, rm, rd)                           if extension("Zfh") & extension("Zfa")
+  <-> 0b010_0010 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extension("Zfh") & extension("Zfa")
 
 mapping clause assembly = RISCV_FROUND_H(rs1, rm, rd)
   <-> "fround.h" ^ spc() ^ freg_name(rd)
@@ -365,8 +365,8 @@ function clause execute (RISCV_FROUND_H(rs1, rm, rd)) = {
 
 union clause ast = RISCV_FROUNDNX_H : (regidx, rounding_mode, regidx)
 
-mapping clause encdec = RISCV_FROUNDNX_H(rs1, rm, rd)                         if haveZfh() & haveZfa()
-  <-> 0b010_0010 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfh() & haveZfa()
+mapping clause encdec = RISCV_FROUNDNX_H(rs1, rm, rd)                         if extension("Zfh") & extension("Zfa")
+  <-> 0b010_0010 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extension("Zfh") & extension("Zfa")
 
 mapping clause assembly = RISCV_FROUNDNX_H(rs1, rm, rd)
   <-> "froundnx.h" ^ spc() ^ freg_name(rd)
@@ -393,8 +393,8 @@ function clause execute (RISCV_FROUNDNX_H(rs1, rm, rd)) = {
 
 union clause ast = RISCV_FROUND_S : (regidx, rounding_mode, regidx)
 
-mapping clause encdec = RISCV_FROUND_S(rs1, rm, rd)                            if haveZfa()
-  <-> 0b010_0000 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011  if haveZfa()
+mapping clause encdec = RISCV_FROUND_S(rs1, rm, rd)                            if extension("Zfa")
+  <-> 0b010_0000 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011  if extension("Zfa")
 
 mapping clause assembly = RISCV_FROUND_S(rs1, rm, rd)
   <-> "fround.s" ^ spc() ^ freg_name(rd)
@@ -421,8 +421,8 @@ function clause execute (RISCV_FROUND_S(rs1, rm, rd)) = {
 
 union clause ast = RISCV_FROUNDNX_S : (regidx, rounding_mode, regidx)
 
-mapping clause encdec = RISCV_FROUNDNX_S(rs1, rm, rd)                         if haveZfa()
-  <-> 0b010_0000 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfa()
+mapping clause encdec = RISCV_FROUNDNX_S(rs1, rm, rd)                         if extension("Zfa")
+  <-> 0b010_0000 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extension("Zfa")
 
 mapping clause assembly = RISCV_FROUNDNX_S(rs1, rm, rd)
   <-> "froundnx.s" ^ spc() ^ freg_name(rd)
@@ -449,8 +449,8 @@ function clause execute (RISCV_FROUNDNX_S(rs1, rm, rd)) = {
 
 union clause ast = RISCV_FROUND_D : (regidx, rounding_mode, regidx)
 
-mapping clause encdec = RISCV_FROUND_D(rs1, rm, rd)                            if haveDExt() & haveZfa()
-  <-> 0b010_0001 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011  if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FROUND_D(rs1, rm, rd)                            if extension("D") & extension("Zfa")
+  <-> 0b010_0001 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011  if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FROUND_D(rs1, rm, rd)
   <-> "fround.d" ^ spc() ^ freg_name(rd)
@@ -477,8 +477,8 @@ function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = {
 
 union clause ast = RISCV_FROUNDNX_D : (regidx, rounding_mode, regidx)
 
-mapping clause encdec = RISCV_FROUNDNX_D(rs1, rm, rd)                         if haveDExt() & haveZfa()
-  <-> 0b010_0001 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FROUNDNX_D(rs1, rm, rd)                         if extension("D") & extension("Zfa")
+  <-> 0b010_0001 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FROUNDNX_D(rs1, rm, rd)
   <-> "froundnx.d" ^ spc() ^ freg_name(rd)
@@ -505,8 +505,8 @@ function clause execute (RISCV_FROUNDNX_D(rs1, rm, rd)) = {
 
 union clause ast = RISCV_FMVH_X_D : (regidx, regidx)
 
-mapping clause encdec   = RISCV_FMVH_X_D(rs1, rd)           if haveDExt() & haveZfa() & in32BitMode()
-  <-> 0b111_0001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveDExt() & haveZfa() & in32BitMode()
+mapping clause encdec   = RISCV_FMVH_X_D(rs1, rd)           if extension("D") & extension("Zfa") & in32BitMode()
+  <-> 0b111_0001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("D") & extension("Zfa") & in32BitMode()
 
 mapping clause assembly = RISCV_FMVH_X_D(rs1, rd)
   <-> "fmvh.x.d" ^ spc() ^ reg_name(rd)
@@ -523,8 +523,8 @@ function clause execute (RISCV_FMVH_X_D(rs1, rd)) = {
 
 union clause ast = RISCV_FMVP_D_X : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FMVP_D_X(rs2, rs1, rd)        if haveDExt() & haveZfa() & in32BitMode()
-  <-> 0b101_1001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011      if haveDExt() & haveZfa() & in32BitMode()
+mapping clause encdec = RISCV_FMVP_D_X(rs2, rs1, rd)        if extension("D") & extension("Zfa") & in32BitMode()
+  <-> 0b101_1001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011      if extension("D") & extension("Zfa") & in32BitMode()
 
 mapping clause assembly = RISCV_FMVP_D_X(rs2, rs1, rd)
   <-> "fmvp.d.x" ^ spc() ^ freg_name(rd)
@@ -550,8 +550,8 @@ function clause execute (RISCV_FMVP_D_X(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FLEQ_H : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FLEQ_H(rs2, rs1, rd)               if haveZfh() & haveZfa()
-  <-> 0b101_0010 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011           if haveZfh() & haveZfa()
+mapping clause encdec = RISCV_FLEQ_H(rs2, rs1, rd)               if extension("Zfh") & extension("Zfa")
+  <-> 0b101_0010 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011           if extension("Zfh") & extension("Zfa")
 
 mapping clause assembly = RISCV_FLEQ_H(rs2, rs1, rd)
   <-> "fleq.h" ^ spc() ^ freg_name(rd)
@@ -574,8 +574,8 @@ function clause execute(RISCV_FLEQ_H(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FLTQ_H : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FLTQ_H(rs2, rs1, rd)               if haveZfh() & haveZfa()
-  <-> 0b101_0010 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011           if haveZfh() & haveZfa()
+mapping clause encdec = RISCV_FLTQ_H(rs2, rs1, rd)               if extension("Zfh") & extension("Zfa")
+  <-> 0b101_0010 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011           if extension("Zfh") & extension("Zfa")
 
 mapping clause assembly = RISCV_FLTQ_H(rs2, rs1, rd)
   <-> "fltq.h" ^ spc() ^ freg_name(rd)
@@ -598,8 +598,8 @@ function clause execute(RISCV_FLTQ_H(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FLEQ_S : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FLEQ_S(rs2, rs1, rd)               if haveZfa()
-  <-> 0b101_0000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011           if haveZfa()
+mapping clause encdec = RISCV_FLEQ_S(rs2, rs1, rd)               if extension("Zfa")
+  <-> 0b101_0000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011           if extension("Zfa")
 
 mapping clause assembly = RISCV_FLEQ_S(rs2, rs1, rd)
   <-> "fleq.s" ^ spc() ^ freg_name(rd)
@@ -622,8 +622,8 @@ function clause execute(RISCV_FLEQ_S(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FLTQ_S : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FLTQ_S(rs2, rs1, rd)               if haveZfa()
-  <-> 0b101_0000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011           if haveZfa()
+mapping clause encdec = RISCV_FLTQ_S(rs2, rs1, rd)               if extension("Zfa")
+  <-> 0b101_0000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011           if extension("Zfa")
 
 mapping clause assembly = RISCV_FLTQ_S(rs2, rs1, rd)
   <-> "fltq.s" ^ spc() ^ freg_name(rd)
@@ -647,8 +647,8 @@ function clause execute(RISCV_FLTQ_S(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FLEQ_D : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FLEQ_D(rs2, rs1, rd)               if haveDExt() & haveZfa()
-  <-> 0b101_0001 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011           if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FLEQ_D(rs2, rs1, rd)               if extension("D") & extension("Zfa")
+  <-> 0b101_0001 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011           if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FLEQ_D(rs2, rs1, rd)
   <-> "fleq.d" ^ spc() ^ freg_name(rd)
@@ -671,8 +671,8 @@ function clause execute(RISCV_FLEQ_D(rs2, rs1, rd)) = {
 
 union clause ast = RISCV_FLTQ_D : (regidx, regidx, regidx)
 
-mapping clause encdec = RISCV_FLTQ_D(rs2, rs1, rd)               if haveDExt() & haveZfa()
-  <-> 0b101_0001 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011           if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FLTQ_D(rs2, rs1, rd)               if extension("D") & extension("Zfa")
+  <-> 0b101_0001 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011           if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FLTQ_D(rs2, rs1, rd)
   <-> "fltq.d" ^ spc() ^ freg_name(rd)
@@ -759,8 +759,8 @@ function fcvtmod_helper(x64) = {
 union clause ast = RISCV_FCVTMOD_W_D : (regidx, regidx)
 
 /* We need rounding mode to be explicitly specified to RTZ(0b001) */
-mapping clause encdec = RISCV_FCVTMOD_W_D(rs1, rd)          if haveDExt() & haveZfa()
-  <-> 0b110_0001 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveDExt() & haveZfa()
+mapping clause encdec = RISCV_FCVTMOD_W_D(rs1, rd)          if extension("D") & extension("Zfa")
+  <-> 0b110_0001 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if extension("D") & extension("Zfa")
 
 mapping clause assembly = RISCV_FCVTMOD_W_D(rs1, rd)
   <-> "fcvtmod.w.d" ^ spc() ^ reg_name(rd)
diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail
index 5522bad22..840e7619b 100644
--- a/model/riscv_insts_zfh.sail
+++ b/model/riscv_insts_zfh.sail
@@ -162,7 +162,7 @@ function fle_H   (v1,       v2,        is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()'                                  */
 
-function haveHalfFPU() -> bool = haveZfh() | haveZhinx()
+function haveHalfFPU() -> bool = extension("Zfh") | extension("Zhinx")
 
 /* ****************************************************************** */
 /* Floating-point loads                                               */
@@ -881,11 +881,11 @@ union clause ast = F_UN_TYPE_H : (regidx, regidx, f_un_op_H)
 mapping clause encdec = F_UN_TYPE_H(rs1, rd, FCLASS_H)                        if haveHalfFPU()
                     <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011  if haveHalfFPU()
 
-mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_X_H)                         if haveZfh()
-                    <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_X_H)                         if extension("Zfh")
+                    <-> 0b111_0010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("Zfh")
 
-mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_H_X)                         if haveZfh()
-                    <-> 0b111_1010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if haveZfh()
+mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_H_X)                         if extension("Zfh")
+                    <-> 0b111_1010 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011  if extension("Zfh")
 
 /* Execution semantics ================================ */
 
diff --git a/model/riscv_insts_zicond.sail b/model/riscv_insts_zicond.sail
index d51260312..71b71558e 100644
--- a/model/riscv_insts_zicond.sail
+++ b/model/riscv_insts_zicond.sail
@@ -8,10 +8,10 @@
 
 union clause ast = ZICOND_RTYPE : (regidx, regidx, regidx, zicondop)
 
-mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_EQZ) if haveZicond()
-  <-> 0b0000111 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if haveZicond()
-mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_NEZ) if haveZicond()
-  <-> 0b0000111 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if haveZicond()
+mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_EQZ) if extension("Zicond")
+  <-> 0b0000111 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0110011 if extension("Zicond")
+mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_NEZ) if extension("Zicond")
+  <-> 0b0000111 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 if extension("Zicond")
 
 mapping zicond_mnemonic : zicondop <-> string = {
   RISCV_CZERO_EQZ <-> "czero.eqz",
diff --git a/model/riscv_insts_zkn.sail b/model/riscv_insts_zkn.sail
index 8bcd250a7..12623430d 100644
--- a/model/riscv_insts_zkn.sail
+++ b/model/riscv_insts_zkn.sail
@@ -11,22 +11,26 @@
  * ----------------------------------------------------------------------
  */
 
+$[name "SHA2-256 Sigma0"]
 union clause ast = SHA256SIG0 : (regidx, regidx)
+$[name "SHA2-256 Sigma1"]
 union clause ast = SHA256SIG1 : (regidx, regidx)
+$[name "SHA2-256 Sum0"]
 union clause ast = SHA256SUM0 : (regidx, regidx)
+$[name "SHA2-256 Sum1"]
 union clause ast = SHA256SUM1 : (regidx, regidx)
 
-mapping clause encdec = SHA256SUM0 (rs1, rd) if haveZknh()
-  <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh()
+mapping clause encdec = SHA256SUM0 (rs1, rd) if extension("Zknh")
+  <-> 0b00 @ 0b01000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh")
 
-mapping clause encdec = SHA256SUM1 (rs1, rd) if haveZknh()
-  <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh()
+mapping clause encdec = SHA256SUM1 (rs1, rd) if extension("Zknh")
+  <-> 0b00 @ 0b01000 @ 0b00001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh")
 
-mapping clause encdec = SHA256SIG0 (rs1, rd) if haveZknh()
-  <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh()
+mapping clause encdec = SHA256SIG0 (rs1, rd) if extension("Zknh")
+  <-> 0b00 @ 0b01000 @ 0b00010 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh")
 
-mapping clause encdec = SHA256SIG1 (rs1, rd) if haveZknh()
-  <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh()
+mapping clause encdec = SHA256SIG1 (rs1, rd) if extension("Zknh")
+  <-> 0b00 @ 0b01000 @ 0b00011 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh")
 
 mapping clause assembly = SHA256SIG0 (rs1, rd)
   <-> "sha256sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -75,8 +79,8 @@ function clause execute (SHA256SUM1(rs1, rd)) = {
 
 union clause ast = AES32ESMI : (bits(2), regidx, regidx, regidx)
 
-mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 32
-  <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 32
+mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 32
+  <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 32
 
 mapping clause assembly = AES32ESMI (bs, rs2, rs1, rd) <->
     "aes32esmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs)
@@ -93,8 +97,8 @@ function clause execute (AES32ESMI (bs, rs2, rs1, rd)) = {
 
 union clause ast = AES32ESI : (bits(2), regidx, regidx, regidx)
 
-mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 32
-  <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 32
+mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 32
+  <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 32
 
 mapping clause assembly = AES32ESI (bs, rs2, rs1, rd) <->
     "aes32esi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs)
@@ -115,8 +119,8 @@ function clause execute (AES32ESI (bs, rs2, rs1, rd)) = {
 
 union clause ast = AES32DSMI : (bits(2), regidx, regidx, regidx)
 
-mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 32
-  <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 32
+mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 32
+  <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 32
 
 mapping clause assembly = AES32DSMI (bs, rs2, rs1, rd) <->
     "aes32dsmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs)
@@ -133,8 +137,8 @@ function clause execute (AES32DSMI (bs, rs2, rs1, rd)) = {
 
 union clause ast = AES32DSI  : (bits(2), regidx, regidx, regidx)
 
-mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 32
-  <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 32
+mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 32
+  <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 32
 
 mapping clause assembly = AES32DSI (bs, rs2, rs1, rd) <->
     "aes32dsi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs)
@@ -153,30 +157,36 @@ function clause execute (AES32DSI (bs, rs2, rs1, rd)) = {
  * ----------------------------------------------------------------------
  */
 
+$[name "SHA2-512 Sigma0 low"]
 union clause ast = SHA512SIG0L : (regidx, regidx, regidx)
+$[name "SHA2-512 Sigma0 high"]
 union clause ast = SHA512SIG0H : (regidx, regidx, regidx)
+$[name "SHA2-512 Sigma1 low"]
 union clause ast = SHA512SIG1L : (regidx, regidx, regidx)
+$[name "SHA2-512 Sigma1 high"]
 union clause ast = SHA512SIG1H : (regidx, regidx, regidx)
+$[name "SHA2-512 Sum0 (RV32)"]
 union clause ast = SHA512SUM0R : (regidx, regidx, regidx)
+$[name "SHA2-512 Sum1 (RV32)"]
 union clause ast = SHA512SUM1R : (regidx, regidx, regidx)
 
-mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32
-  <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32
+mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32
+  <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32
 
-mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32
-  <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32
+mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32
+  <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32
 
-mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32
-  <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32
+mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32
+  <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32
 
-mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32
-  <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32
+mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32
+  <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32
 
-mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32
-  <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32
+mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32
+  <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32
 
-mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if haveZknh() & sizeof(xlen) == 32
-  <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknh() & sizeof(xlen) == 32
+mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if extension("Zknh") & sizeof(xlen) == 32
+  <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknh") & sizeof(xlen) == 32
 
 mapping clause assembly = SHA512SIG0L (rs2, rs1, rd)
   <-> "sha512sig0l" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
@@ -245,26 +255,26 @@ union clause ast = AES64ES   : (regidx, regidx, regidx)
 union clause ast = AES64DSM  : (regidx, regidx, regidx)
 union clause ast = AES64DS   : (regidx, regidx, regidx)
 
-mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (haveZkne() | haveZknd()) & (sizeof(xlen) == 64) & (rnum <_u 0xB)
-  <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (haveZkne() | haveZknd()) & (sizeof(xlen) == 64) & (rnum <_u 0xB)
+mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (extension("Zkne") | extension("Zknd")) & (sizeof(xlen) == 64) & (rnum <_u 0xB)
+  <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (extension("Zkne") | extension("Zknd")) & (sizeof(xlen) == 64) & (rnum <_u 0xB)
 
-mapping clause encdec = AES64IM (rs1, rd) if haveZknd() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknd() & sizeof(xlen) == 64
+mapping clause encdec = AES64IM (rs1, rd) if extension("Zknd") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknd") & sizeof(xlen) == 64
 
-mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (haveZkne() | haveZknd()) & sizeof(xlen) == 64
-  <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (haveZkne() | haveZknd()) & sizeof(xlen) == 64
+mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (extension("Zkne") | extension("Zknd")) & sizeof(xlen) == 64
+  <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (extension("Zkne") | extension("Zknd")) & sizeof(xlen) == 64
 
-mapping clause encdec = AES64ESM (rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 64
+mapping clause encdec = AES64ESM (rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 64
 
-mapping clause encdec = AES64ES (rs2, rs1, rd) if haveZkne() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZkne() & sizeof(xlen) == 64
+mapping clause encdec = AES64ES (rs2, rs1, rd) if extension("Zkne") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zkne") & sizeof(xlen) == 64
 
-mapping clause encdec = AES64DSM (rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 64
+mapping clause encdec = AES64DSM (rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 64
 
-mapping clause encdec = AES64DS (rs2, rs1, rd) if haveZknd() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZknd() & sizeof(xlen) == 64
+mapping clause encdec = AES64DS (rs2, rs1, rd) if extension("Zknd") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zknd") & sizeof(xlen) == 64
 
 mapping clause assembly = AES64KS1I (rnum, rs1, rd)
   <-> "aes64ks1i" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_4(rnum)
@@ -355,22 +365,26 @@ function clause execute (AES64DS(rs2, rs1, rd)) = {
  * ----------------------------------------------------------------------
  */
 
+$[name "SHA2-512 Sigma0"]
 union clause ast = SHA512SIG0 : (regidx, regidx)
+$[name "SHA2-512 Sigma1"]
 union clause ast = SHA512SIG1 : (regidx, regidx)
+$[name "SHA2-512 Sum0 (RV64)"]
 union clause ast = SHA512SUM0 : (regidx, regidx)
+$[name "SHA2-512 Sum1 (RV64)"]
 union clause ast = SHA512SUM1 : (regidx, regidx)
 
-mapping clause encdec = SHA512SUM0 (rs1, rd) if haveZknh() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64
+mapping clause encdec = SHA512SUM0 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64
 
-mapping clause encdec = SHA512SUM1 (rs1, rd) if haveZknh() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64
+mapping clause encdec = SHA512SUM1 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64
 
-mapping clause encdec = SHA512SIG0 (rs1, rd) if haveZknh() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64
+mapping clause encdec = SHA512SIG0 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64
 
-mapping clause encdec = SHA512SIG1 (rs1, rd) if haveZknh() & sizeof(xlen) == 64
-  <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZknh() & sizeof(xlen) == 64
+mapping clause encdec = SHA512SIG1 (rs1, rd) if extension("Zknh") & sizeof(xlen) == 64
+  <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zknh") & sizeof(xlen) == 64
 
 mapping clause assembly = SHA512SIG0 (rs1, rd)
   <-> "sha512sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
diff --git a/model/riscv_insts_zks.sail b/model/riscv_insts_zks.sail
index 2cb44f181..5ed6aa9bf 100644
--- a/model/riscv_insts_zks.sail
+++ b/model/riscv_insts_zks.sail
@@ -14,11 +14,11 @@
 union clause ast = SM3P0 : (regidx, regidx)
 union clause ast = SM3P1 : (regidx, regidx)
 
-mapping clause encdec = SM3P0 (rs1, rd) if haveZksh()
-  <-> 0b00 @ 0b01000 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZksh()
+mapping clause encdec = SM3P0 (rs1, rd) if extension("Zksh")
+  <-> 0b00 @ 0b01000 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zksh")
 
-mapping clause encdec = SM3P1 (rs1, rd) if haveZksh()
-  <-> 0b00 @ 0b01000 @ 0b01001 @ rs1 @ 0b001 @ rd @ 0b0010011 if haveZksh()
+mapping clause encdec = SM3P1 (rs1, rd) if extension("Zksh")
+  <-> 0b00 @ 0b01000 @ 0b01001 @ rs1 @ 0b001 @ rd @ 0b0010011 if extension("Zksh")
 
 mapping clause assembly = SM3P0 (rs1, rd) <->
   "sm3p0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
@@ -48,11 +48,11 @@ function clause execute (SM3P1(rs1, rd)) = {
 union clause ast = SM4ED : (bits(2), regidx, regidx, regidx)
 union clause ast = SM4KS : (bits(2), regidx, regidx, regidx)
 
-mapping clause encdec = SM4ED (bs, rs2, rs1, rd) if haveZksed()
-  <-> bs @ 0b11000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZksed()
+mapping clause encdec = SM4ED (bs, rs2, rs1, rd) if extension("Zksed")
+  <-> bs @ 0b11000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zksed")
 
-mapping clause encdec = SM4KS (bs, rs2, rs1, rd) if haveZksed()
-  <-> bs @ 0b11010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if haveZksed()
+mapping clause encdec = SM4KS (bs, rs2, rs1, rd) if extension("Zksed")
+  <-> bs @ 0b11010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extension("Zksed")
 
 mapping clause assembly = SM4ED (bs, rs2, rs1, rd) <->
     "sm4ed" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs)
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index 497a44178..6dd32d388 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -24,7 +24,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
     },
     Ext_ControlAddr_OK(addr) => {
       let target = [addr with 0 = bitzero];  /* clear addr[0] */
-      if bit_to_bool(target[1]) & not(haveRVC()) then {
+      if bit_to_bool(target[1]) & not(extension("C")) then {
         handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
       } else {
diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail
index 688d16d72..263850206 100644
--- a/model/riscv_next_control.sail
+++ b/model/riscv_next_control.sail
@@ -8,14 +8,14 @@
 
 /* Functional specification for the 'N' user-level interrupts standard extension. */
 
-function clause ext_is_CSR_defined(0x000, _) = haveUsrMode() & haveNExt() // ustatus
-function clause ext_is_CSR_defined(0x004, _) = haveUsrMode() & haveNExt() // uie
-function clause ext_is_CSR_defined(0x005, _) = haveUsrMode() & haveNExt() // utvec
-function clause ext_is_CSR_defined(0x040, _) = haveUsrMode() & haveNExt() // uscratch
-function clause ext_is_CSR_defined(0x041, _) = haveUsrMode() & haveNExt() // uepc
-function clause ext_is_CSR_defined(0x042, _) = haveUsrMode() & haveNExt() // ucause
-function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() & haveNExt() // utval
-function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() & haveNExt() // uip
+function clause ext_is_CSR_defined(0x000, _) = extension("U") & extension("N") // ustatus
+function clause ext_is_CSR_defined(0x004, _) = extension("U") & extension("N") // uie
+function clause ext_is_CSR_defined(0x005, _) = extension("U") & extension("N") // utvec
+function clause ext_is_CSR_defined(0x040, _) = extension("U") & extension("N") // uscratch
+function clause ext_is_CSR_defined(0x041, _) = extension("U") & extension("N") // uepc
+function clause ext_is_CSR_defined(0x042, _) = extension("U") & extension("N") // ucause
+function clause ext_is_CSR_defined(0x043, _) = extension("U") & extension("N") // utval
+function clause ext_is_CSR_defined(0x044, _) = extension("U") & extension("N") // uip
 
 function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits)
 function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits)
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 5ff7e4bc0..82ed310b8 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -54,7 +54,7 @@ function step(step_no : int) -> bool = {
               print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
             };
             /* check for RVC once here instead of every RVC execute clause. */
-            if haveRVC() then {
+            if extension("C") then {
               nextPC = PC + 2;
               (execute(ast), true)
             } else {
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 1baa33701..a71759cbd 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -25,14 +25,14 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     /* machine mode: trap setup */
     0x300 => p == Machine, // mstatus
     0x301 => p == Machine, // misa
-    0x302 => p == Machine & (haveSupMode() | haveNExt()), // medeleg
-    0x303 => p == Machine & (haveSupMode() | haveNExt()), // mideleg
+    0x302 => p == Machine & (extension("S") | extension("N")), // medeleg
+    0x303 => p == Machine & (extension("S") | extension("N")), // mideleg
     0x304 => p == Machine, // mie
     0x305 => p == Machine, // mtvec
-    0x306 => p == Machine & haveUsrMode(), // mcounteren
-    0x30A => p == Machine & haveUsrMode(), // menvcfg
+    0x306 => p == Machine & extension("U"), // mcounteren
+    0x30A => p == Machine & extension("U"), // menvcfg
     0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush
-    0x31A => p == Machine & haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh
+    0x31A => p == Machine & extension("U") & (sizeof(xlen) == 32), // menvcfgh
     0x320 => p == Machine, // mcountinhibit
     /* machine mode: trap handling */
     0x340 => p == Machine, // mscratch
@@ -59,35 +59,35 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x7a0 => p == Machine,
 
     /* supervisor mode: trap setup */
-    0x100 => haveSupMode() & (p == Machine | p == Supervisor), // sstatus
-    0x102 => haveSupMode() & haveNExt() & (p == Machine | p == Supervisor), // sedeleg
-    0x103 => haveSupMode() & haveNExt() & (p == Machine | p == Supervisor), // sideleg
-    0x104 => haveSupMode() & (p == Machine | p == Supervisor), // sie
-    0x105 => haveSupMode() & (p == Machine | p == Supervisor), // stvec
-    0x106 => haveSupMode() & (p == Machine | p == Supervisor), // scounteren
-    0x10A => haveSupMode() & (p == Machine | p == Supervisor), // senvcfg
+    0x100 => extension("S") & (p == Machine | p == Supervisor), // sstatus
+    0x102 => extension("S") & extension("N") & (p == Machine | p == Supervisor), // sedeleg
+    0x103 => extension("S") & extension("N") & (p == Machine | p == Supervisor), // sideleg
+    0x104 => extension("S") & (p == Machine | p == Supervisor), // sie
+    0x105 => extension("S") & (p == Machine | p == Supervisor), // stvec
+    0x106 => extension("S") & (p == Machine | p == Supervisor), // scounteren
+    0x10A => extension("S") & (p == Machine | p == Supervisor), // senvcfg
 
     /* supervisor mode: trap handling */
-    0x140 => haveSupMode() & (p == Machine | p == Supervisor), // sscratch
-    0x141 => haveSupMode() & (p == Machine | p == Supervisor), // sepc
-    0x142 => haveSupMode() & (p == Machine | p == Supervisor), // scause
-    0x143 => haveSupMode() & (p == Machine | p == Supervisor), // stval
-    0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip
+    0x140 => extension("S") & (p == Machine | p == Supervisor), // sscratch
+    0x141 => extension("S") & (p == Machine | p == Supervisor), // sepc
+    0x142 => extension("S") & (p == Machine | p == Supervisor), // scause
+    0x143 => extension("S") & (p == Machine | p == Supervisor), // stval
+    0x144 => extension("S") & (p == Machine | p == Supervisor), // sip
 
     /* supervisor mode: address translation */
-    0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp
+    0x180 => extension("S") & (p == Machine | p == Supervisor), // satp
 
     /* user mode: counters */
-    0xC00 => haveUsrMode(),    // cycle
-    0xC01 => haveUsrMode(),    // time
-    0xC02 => haveUsrMode(),    // instret
+    0xC00 => extension("U"),    // cycle
+    0xC01 => extension("U"),    // time
+    0xC02 => extension("U"),    // instret
 
-    0xC80 => haveUsrMode() & (sizeof(xlen) == 32),     // cycleh
-    0xC81 => haveUsrMode() & (sizeof(xlen) == 32),     // timeh
-    0xC82 => haveUsrMode() & (sizeof(xlen) == 32),     // instreth
+    0xC80 => extension("U") & (sizeof(xlen) == 32),     // cycleh
+    0xC81 => extension("U") & (sizeof(xlen) == 32),     // timeh
+    0xC82 => extension("U") & (sizeof(xlen) == 32),     // instreth
 
     /* user mode: Zkr */
-    0x015 => haveZkr(),
+    0x015 => extension("Zkr"),
 
     /* check extensions */
     _     => ext_is_CSR_defined(csr, p)
@@ -107,9 +107,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool =
     (0xC01, Supervisor) => mcounteren[TM] == 0b1,
     (0xC02, Supervisor) => mcounteren[IR] == 0b1,
 
-    (0xC00, User) => mcounteren[CY] == 0b1 & (not(haveSupMode()) | scounteren[CY] == 0b1),
-    (0xC01, User) => mcounteren[TM] == 0b1 & (not(haveSupMode()) | scounteren[TM] == 0b1),
-    (0xC02, User) => mcounteren[IR] == 0b1 & (not(haveSupMode()) | scounteren[IR] == 0b1),
+    (0xC00, User) => mcounteren[CY] == 0b1 & (not(extension("S")) | scounteren[CY] == 0b1),
+    (0xC01, User) => mcounteren[TM] == 0b1 & (not(extension("S")) | scounteren[TM] == 0b1),
+    (0xC02, User) => mcounteren[IR] == 0b1 & (not(extension("S")) | scounteren[IR] == 0b1),
 
     (_, _) => /* no HPM counters for now */
               if   0xC03 <=_u csr & csr <=_u 0xC1F
@@ -168,11 +168,11 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
   let idx   = num_of_ExceptionType(e);
   let super = bit_to_bool(medeleg.bits[idx]);
   /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */
-  let user  = if   haveSupMode()
-              then super & haveNExt() & bit_to_bool(sedeleg.bits[idx])
-              else super & haveNExt();
-  let deleg = if      haveUsrMode() & user  then User
-              else if haveSupMode() & super then Supervisor
+  let user  = if   extension("S")
+              then super & extension("N") & bit_to_bool(sedeleg.bits[idx])
+              else super & extension("N");
+  let deleg = if      extension("U") & user  then User
+              else if extension("S") & super then Supervisor
               else                               Machine;
   /* We cannot transition to a less-privileged mode. */
   if   privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
@@ -228,7 +228,7 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits
  * allows for example the M_Timer to be delegated to the U-mode.
  */
 function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
-  assert(haveUsrMode(), "no user mode: M/U or M/S/U system required");
+  assert(extension("U"), "no user mode: M/U or M/S/U system required");
   let effective_pending = mip.bits & mie.bits;
   if  effective_pending == zero_extend(0b0) then None() /* fast path */
   else {
@@ -237,13 +237,13 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
      * considered blocked.
      */
     let mIE = priv != Machine | (priv == Machine & mstatus[MIE] == 0b1);
-    let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1));
-    let uIE = haveNExt() & (priv == User & mstatus[UIE] == 0b1);
+    let sIE = extension("S") & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1));
+    let uIE = extension("N") & (priv == User & mstatus[UIE] == 0b1);
     match processPending(mip, mie, mideleg.bits, mIE) {
       Ints_Empty()      => None(),
       Ints_Pending(p)   => let r = (p, Machine) in Some(r),
       Ints_Delegated(d) =>
-        if not(haveSupMode()) then {
+        if not(extension("S")) then {
           if uIE then let r = (d, User) in Some(r)
           else                             None()
         } else {
@@ -267,7 +267,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
   /* If we don't have different privilege levels, we don't need to check delegation.
    * Absence of U-mode implies absence of S-mode.
    */
-  if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then {
+  if not(extension("U")) | (not(extension("S")) & not(extension("N"))) then {
     assert(priv == Machine, "invalid current privilege");
     let enabled_pending = mip.bits & mie.bits;
     match findPendingInterrupt(enabled_pending) {
@@ -346,7 +346,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
        prepare_trap_vector(del_priv, mcause)
     },
     Supervisor => {
-       assert (haveSupMode(), "no supervisor mode present for delegation");
+       assert (extension("S"), "no supervisor mode present for delegation");
 
        scause[IsInterrupt] = bool_to_bits(intr);
        scause[Cause]       = zero_extend(c);
@@ -371,7 +371,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
        prepare_trap_vector(del_priv, scause)
     },
     User => {
-       assert(haveUsrMode(), "no user mode present for delegation");
+       assert(extension("U"), "no user mode present for delegation");
 
        ucause[IsInterrupt] = bool_to_bits(intr);
        ucause[Cause]       = zero_extend(c);
@@ -408,7 +408,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       mstatus[MIE]  = mstatus[MPIE];
       mstatus[MPIE] = 0b1;
       cur_privilege   = privLevel_of_bits(mstatus[MPP]);
-      mstatus[MPP]  = privLevel_to_bits(if haveUsrMode() then User else Machine);
+      mstatus[MPP]  = privLevel_to_bits(if extension("U") then User else Machine);
       if   cur_privilege != Machine
       then mstatus[MPRV] = 0b0;
 
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 3537abc16..de1db68c6 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -125,49 +125,6 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
   }
 }
 
-/* helpers to check support for various extensions. */
-/* we currently don't model 'E', so always assume 'I'. */
-function haveAtomics() -> bool = misa[A] == 0b1
-function haveRVC()     -> bool = misa[C] == 0b1
-function haveMulDiv()  -> bool = misa[M] == 0b1
-function haveSupMode() -> bool = misa[S] == 0b1
-function haveUsrMode() -> bool = misa[U] == 0b1
-function haveNExt()    -> bool = misa[N] == 0b1
-/* see below for F and D (and Z*inx counterparts) extension tests */
-
-/* BitManip extension support. */
-function haveZba()  -> bool = true
-function haveZbb()  -> bool = true
-function haveZbc()  -> bool = true
-function haveZbs()  -> bool = true
-
-/* Zfa (additional FP) extension */
-function haveZfa()  -> bool = true
-
-/* Scalar Cryptography extensions support. */
-function haveZbkb() -> bool = true
-function haveZbkc() -> bool = true
-function haveZbkx() -> bool = true
-
-/* Cryptography extension support. Note these will need updating once */
-/* Sail can be dynamically configured with different extension support */
-/* and have dynamic changes of XLEN via S/UXL */
-function haveZkr()    -> bool = true
-function haveZksh()   -> bool = true
-function haveZksed()  -> bool = true
-function haveZknh()   -> bool = true
-function haveZkne()   -> bool = true
-function haveZknd()   -> bool = true
-
-function haveZmmul()  -> bool = true
-
-/* A extension sub-extensions */
-function haveZaamo()  -> bool = haveAtomics()
-function haveZalrsc() -> bool = haveAtomics()
-
-/* Zicond extension support */
-function haveZicond() -> bool = true
-
 bitfield Mstatush : bits(32) = {
   MBE  : 5,
   SBE  : 4
@@ -247,6 +204,74 @@ function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = {
   }
 }
 
+val extension : (string) -> bool
+
+/* helper to check support for various extensions. */
+/* we currently don't model 'E', so always assume 'I'. */
+function extension(ext) = {
+  match ext {
+    "A" => misa[A] == 0b1,
+    "C" => misa[C] == 0b1,
+
+    /* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */
+    "D" => (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64,
+    "F" => (misa[F] == 0b1) & (mstatus[FS] != 0b00),
+
+    "M" => misa[M] == 0b1,
+    "N" => misa[N] == 0b1,
+    "U" => misa[U] == 0b1,
+    "S" => misa[S] == 0b1,
+
+    "Svinval" => sys_enable_svinval(),
+
+    /* V extension has to enable both via misa.V as well as mstatus.VS */
+    "V" => (misa[V] == 0b1) & (mstatus[VS] != 0b00),
+
+    "Zaamo" => extension("A"),
+    "Zalrsc" => extension("A"),
+
+    /* BitManip extension support. */
+    "Zba" => true,
+    "Zbb" => true,
+    "Zbc" => true,
+    "Zbs" => true,
+
+    /* Scalar Cryptography extensions support. */
+    "Zbkb" => true,
+    "Zbkc" => true,
+    "Zbkx" => true,
+
+    "Zcb" => sys_enable_zcb(),
+
+    /* Zfa (additional FP) extension */
+    "Zfa" => true,
+
+    /* Zfh (half-precision) extension depends on misa.F and mstatus.FS */
+    "Zfh" => (misa[F] == 0b1) & (mstatus[FS] != 0b00),
+
+    /* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */
+    "Zdinx" => sys_enable_zfinx() & sizeof(flen) >= 64,
+    "Zfinx" => sys_enable_zfinx(),
+    "Zhinx" => sys_enable_zfinx(),
+
+    /* Zicond extension support */
+    "Zicond" => true,
+
+    /* Cryptography extension support. Note these will need updating once */
+    /* Sail can be dynamically configured with different extension support */
+    /* and have dynamic changes of XLEN via S/UXL */
+    "Zkr" => true,
+    "Zksh" => true,
+    "Zksed" => true,
+    "Zknd" => true,
+    "Zkne" => true,
+    "Zknh" => true,
+
+    "Zmmul" => true,
+    _ => false
+  }
+}
+
 function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
   /*
    * Populate all defined fields using the bits of v, stripping anything
@@ -278,13 +303,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
           } else m;
 
   /* Hardwired to zero in the absence of 'U' or 'N'. */
-  let m = if not(haveNExt()) then {
+  let m = if not(extension("N")) then {
              let m = [m with UPIE = 0b0];
              let m = [m with UIE = 0b0];
              m
           } else m;
 
-  if not(haveUsrMode()) then {
+  if not(extension("U")) then {
     let m = [m with MPRV = 0b0];
     m
   } else m
@@ -309,24 +334,6 @@ function in32BitMode() -> bool = {
   cur_Architecture() == RV32
 }
 
-/* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */
-function haveFExt()    -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00)
-function haveDExt()    -> bool = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64
-/* Zfh (half-precision) extension depends on misa.F and mstatus.FS */
-function haveZfh()     -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00)
-/* V extension has to enable both via misa.V as well as mstatus.VS */
-function haveVExt()    -> bool = (misa[V] == 0b1) & (mstatus[VS] != 0b00)
-
-function haveSvinval() -> bool = sys_enable_svinval()
-
-/* Zcb has simple code-size saving instructions. (The Zcb extension depends on the Zca extension.) */
-function haveZcb()     -> bool = sys_enable_zcb()
-
-/* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */
-function haveZhinx()   -> bool = sys_enable_zfinx()
-function haveZfinx()   -> bool = sys_enable_zfinx()
-function haveZdinx()   -> bool = sys_enable_zfinx() & sizeof(flen) >= 64
-
 /* interrupt processing state */
 
 bitfield Minterrupts : xlenbits = {
@@ -351,7 +358,7 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = {
    * extension, the U-mode bits. */
   let v = Mk_Minterrupts(v);
   let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]];
-  if haveUsrMode() & haveNExt() then {
+  if extension("U") & extension("N") then {
     [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]]
   } else m
 }
@@ -367,7 +374,7 @@ function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = {
     SSI = v[SSI]
   ];
   /* The U-mode bits will be modified if we have the 'N' extension. */
-  if haveUsrMode() & haveNExt() then {
+  if extension("U") & extension("N") then {
     [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]]
   } else m
 }
@@ -655,7 +662,7 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
 function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
   let m : Minterrupts = o;
   let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m;
-  if haveNExt() then {
+  if extension("N") then {
     let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m;
     let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m;
     m
@@ -672,7 +679,7 @@ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru
   let m = if d[SEI] == 0b1 then [m with SEI = s[SEI]] else m;
   let m = if d[STI] == 0b1 then [m with STI = s[STI]] else m;
   let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m;
-  if haveNExt() then {
+  if extension("N") then {
     let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m;
     let m = if d[UTI] == 0b1 then [m with UTI = s[UTI]] else m;
     let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m;