diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
index 960036237..57fdef0e8 100644
--- a/model/riscv_insts_vext_vset.sail
+++ b/model/riscv_insts_vext_vset.sail
@@ -71,60 +71,54 @@ mapping maybe_ma_flag : string <-> bits(1) = {
   sep() ^ "mu" <-> 0b0
 }
 
-/* ****************************** vsetvli & vsetvl ******************************* */
-union clause ast = VSET_TYPE : (vsetop, bits(1), bits(1), bits(3), bits(3), regidx, regidx)
+val handle_illegal_vtype : unit -> unit effect {rreg}
+function handle_illegal_vtype() = {
+  /* Note: Implementations can set vill or trap if the vtype setting is not supported.
+   * TODO: configuration support for both solutions
+   */
+  vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
+  vl = zeros();
+  print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
+  print_reg("CSR vl <- " ^ BitStr(vl))
+}
 
-mapping encdec_vsetop : vsetop <-> bits(4) ={
-  VSETVLI <-> 0b0000,
-  VSETVL  <-> 0b1000
+val calculate_new_vl : (int, int) -> xlenbits
+function calculate_new_vl(AVL, VLMAX) = {
+  /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
+   * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
+   */
+  if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
+  else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
+  else to_bits(sizeof(xlen), VLMAX)
 }
 
-mapping clause encdec = VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) if haveVExt()
-  <-> encdec_vsetop(op) @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
+/* *********************************** vsetvli *********************************** */
+union clause ast = VSETVLI : (bits(1), bits(1), bits(3), bits(3), regidx, regidx)
 
-function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
-  let VLEN_pow      = get_vlen_pow();
-  let ELEN_pow      = get_elen_pow();
+mapping clause encdec = VSETVLI(ma, ta, sew, lmul, rs1, rd) if haveVExt()
+  <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
+
+function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
   let LMUL_pow_ori  = get_lmul_pow();
   let SEW_pow_ori   = get_sew_pow();
   let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
 
   /* set vtype */
-  match op {
-    VSETVLI => {
-      vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul
-    },
-    VSETVL  => {
-      let rs2 : regidx = sew[1 .. 0] @ lmul;
-      vtype->bits() = X(rs2)
-    }
-  };
+  vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
 
-  /* check legal SEW and LMUL and calculate VLMAX */
+  /* check new SEW and LMUL are legal and calculate VLMAX */
+  let VLEN_pow     = get_vlen_pow();
+  let ELEN_pow     = get_elen_pow();
   let LMUL_pow_new = get_lmul_pow();
   let SEW_pow_new  = get_sew_pow();
-  if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
-    /* Note: Implementations can set vill or trap if the vtype setting is not supported.
-     * TODO: configuration support for both solutions
-     */
-    vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
-    vl = zeros();
-    print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
-    print_reg("CSR vl <- " ^ BitStr(vl));
-    return RETIRE_SUCCESS
-  };
+  if SEW_pow_new > LMUL_pow_new + ELEN_pow then { handle_illegal_vtype(); return RETIRE_SUCCESS };
   let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new);
 
   /* set vl according to VLMAX and AVL */
   if (rs1 != 0b00000) then { /* normal stripmining */
     let rs1_val = X(rs1);
     let AVL = unsigned(rs1_val);
-    vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
-         else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
-         else to_bits(sizeof(xlen), VLMAX);
-    /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
-     * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
-     */
+    vl = calculate_new_vl(AVL, VLMAX);
     X(rd) = vl;
   } else if (rd != 0b00000) then { /* set vl to VLMAX */
     let AVL = unsigned(ones(sizeof(xlen)));
@@ -133,81 +127,105 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
   } else { /* keep existing vl */
     let AVL = unsigned(vl);
     let ratio_pow_new = SEW_pow_new - LMUL_pow_new;
-    if (ratio_pow_new != ratio_pow_ori) then {
-      /* Note: Implementations can set vill or trap if the vtype setting is not supported.
-       * TODO: configuration support for both solutions
-       */
-      vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
-      vl = zeros();
-    }
+    if (ratio_pow_new != ratio_pow_ori) then { handle_illegal_vtype(); return RETIRE_SUCCESS }
   };
-  print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
-  print_reg("CSR vl <- " ^ BitStr(vl));
 
   /* reset vstart to 0 */
   vstart = zeros();
+
+  print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
+  print_reg("CSR vl <- " ^ BitStr(vl));
   print_reg("CSR vstart <- " ^ BitStr(vstart));
 
   RETIRE_SUCCESS
 }
 
-mapping vsettype_mnemonic : vsetop <-> string ={
-  VSETVLI <-> "vsetvli",
-  VSETVL  <-> "vsetvli"
-}
+mapping clause assembly = VSETVLI(ma, ta, sew, lmul, rs1, rd)
+  <-> "vsetvli" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma)
 
-mapping clause assembly = VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd)
-  <-> vsettype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma)
+/* *********************************** vsetvl ************************************ */
+union clause ast = VSETVL : (regidx, regidx, regidx)
 
-/* ********************************* vsetivli ************************************ */
-union clause ast = VSETI_TYPE : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx)
+mapping clause encdec = VSETVL(rs2, rs1, rd) if haveVExt()
+  <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
 
-mapping clause encdec = VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) if haveVExt()
-  <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt()
-
-function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = {
-  let VLEN_pow      = get_vlen_pow();
-  let ELEN_pow      = get_elen_pow();
+function clause execute VSETVL(rs2, rs1, rd) = {
   let LMUL_pow_ori  = get_lmul_pow();
   let SEW_pow_ori   = get_sew_pow();
   let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
 
   /* set vtype */
-  vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+  vtype->bits() = X(rs2);
 
-  /* check legal SEW and LMUL and calculate VLMAX */
+  /* check new SEW and LMUL are legal and calculate VLMAX */
+  let VLEN_pow     = get_vlen_pow();
+  let ELEN_pow     = get_elen_pow();
   let LMUL_pow_new = get_lmul_pow();
   let SEW_pow_new  = get_sew_pow();
-  if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
-    /* Note: Implementations can set vill or trap if the vtype setting is not supported.
-     * TODO: configuration support for both solutions
-     */
-    vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
-    vl = zeros();
-    print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
-    print_reg("CSR vl <- " ^ BitStr(vl));
-    return RETIRE_SUCCESS
-  };
+  if SEW_pow_new > LMUL_pow_new + ELEN_pow then { handle_illegal_vtype(); return RETIRE_SUCCESS };
   let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new);
-  let AVL   = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */
 
   /* set vl according to VLMAX and AVL */
-  vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
-       else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
-       else to_bits(sizeof(xlen), VLMAX);
-  /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
-   * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
-   */
-  X(rd) = vl;
+  if (rs1 != 0b00000) then { /* normal stripmining */
+    let rs1_val = X(rs1);
+    let AVL = unsigned(rs1_val);
+    vl = calculate_new_vl(AVL, VLMAX);
+    X(rd) = vl;
+  } else if (rd != 0b00000) then { /* set vl to VLMAX */
+    let AVL = unsigned(ones(sizeof(xlen)));
+    vl = to_bits(sizeof(xlen), VLMAX);
+    X(rd) = vl;
+  } else { /* keep existing vl */
+    let AVL = unsigned(vl);
+    let ratio_pow_new = SEW_pow_new - LMUL_pow_new;
+    if (ratio_pow_new != ratio_pow_ori) then { handle_illegal_vtype(); return RETIRE_SUCCESS }
+  };
+
+  /* reset vstart to 0 */
+  vstart = zeros();
+
   print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
   print_reg("CSR vl <- " ^ BitStr(vl));
+  print_reg("CSR vstart <- " ^ BitStr(vstart));
+
+  RETIRE_SUCCESS
+}
+
+mapping clause assembly = VSETVL(rs2, rs1, rd)
+  <-> "vsetvl" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+/* ********************************** 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()
+
+function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
+  /* set vtype */
+  vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+
+  /* check new SEW and LMUL are legal and calculate VLMAX */
+  let VLEN_pow     = get_vlen_pow();
+  let ELEN_pow     = get_elen_pow();
+  let LMUL_pow_new = get_lmul_pow();
+  let SEW_pow_new  = get_sew_pow();
+  if SEW_pow_new > LMUL_pow_new + ELEN_pow then { handle_illegal_vtype(); return RETIRE_SUCCESS };
+  let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new);
+
+  /* set vl according to VLMAX and AVL */
+  let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */
+  vl = calculate_new_vl(AVL, VLMAX);
+  X(rd) = vl;
 
   /* reset vstart to 0 */
   vstart = zeros();
+
+  print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
+  print_reg("CSR vl <- " ^ BitStr(vl));
   print_reg("CSR vstart <- " ^ BitStr(vstart));
 
   RETIRE_SUCCESS
 }
 
-mapping clause assembly = VSETI_TYPE(ma, ta, sew, lmul, uimm, rd)
+mapping clause assembly = VSETIVLI(ma, ta, sew, lmul, uimm, rd)
   <-> "vsetivli" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(uimm) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma)
diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail
index 6f553757b..f8025b4ec 100755
--- a/model/riscv_vreg_type.sail
+++ b/model/riscv_vreg_type.sail
@@ -44,7 +44,6 @@ type vreglenbits = bits(vlenmax) /* use the largest possible register length */
 type vregtype = vreglenbits
 
 /* vector instruction types */
-enum vsetop       = { VSETVLI, VSETVL }
 
 enum vvfunct6     = { VV_VADD, VV_VSUB, VV_VMINU, VV_VMIN, VV_VMAXU, VV_VMAX, VV_VAND, VV_VOR, VV_VXOR,
   VV_VRGATHER, VV_VRGATHEREI16, VV_VSADDU, VV_VSADD, VV_VSSUBU, VV_VSSUB, VV_VSLL, VV_VSMUL,