diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail
index 53340956c..83e2c6dab 100755
--- a/model/riscv_insts_vext_mask.sail
+++ b/model/riscv_insts_vext_mask.sail
@@ -61,7 +61,7 @@ mapping clause encdec = MMTYPE(funct6, vs2, vs1, vd) if haveRVV()
 function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
   let SEW      = get_sew();
   let LMUL_pow = get_lmul_pow();
-  let num_elem = int_power(2, get_vlen_pow());
+  let num_elem = unsigned(vlenb) * 8;
 
   if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL };
 
@@ -119,7 +119,7 @@ mapping clause encdec = VCPOP_M(vm, vs2, rd) if haveRVV()
 function clause execute(VCPOP_M(vm, vs2, rd)) = {
   let SEW      = get_sew();
   let LMUL_pow = get_lmul_pow();
-  let num_elem = int_power(2, get_vlen_pow());
+  let num_elem = unsigned(vlenb) * 8;
 
   if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL };
 
@@ -155,7 +155,7 @@ mapping clause encdec = VFIRST_M(vm, vs2, rd) if haveRVV()
 function clause execute(VFIRST_M(vm, vs2, rd)) = {
   let SEW      = get_sew();
   let LMUL_pow = get_lmul_pow();
-  let num_elem = int_power(2, get_vlen_pow());
+  let num_elem = unsigned(vlenb) * 8;
 
   if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL };
 
@@ -193,7 +193,7 @@ mapping clause encdec = VMSBF_M(vm, vs2, vd) if haveRVV()
 function clause execute(VMSBF_M(vm, vs2, vd)) = {
   let SEW      = get_sew();
   let LMUL_pow = get_lmul_pow();
-  let num_elem = int_power(2, get_vlen_pow());
+  let num_elem = unsigned(vlenb) * 8;
 
   if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
   then { handle_illegal(); return RETIRE_FAIL };
@@ -234,7 +234,7 @@ mapping clause encdec = VMSIF_M(vm, vs2, vd) if haveRVV()
 function clause execute(VMSIF_M(vm, vs2, vd)) = {
   let SEW      = get_sew();
   let LMUL_pow = get_lmul_pow();
-  let num_elem = int_power(2, get_vlen_pow());
+  let num_elem = unsigned(vlenb) * 8;
 
   if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
   then { handle_illegal(); return RETIRE_FAIL };
@@ -275,7 +275,7 @@ mapping clause encdec = VMSOF_M(vm, vs2, vd) if haveRVV()
 function clause execute(VMSOF_M(vm, vs2, vd)) = {
   let SEW      = get_sew();
   let LMUL_pow = get_lmul_pow();
-  let num_elem = int_power(2, get_vlen_pow());
+  let num_elem = unsigned(vlenb) * 8;
 
   if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2
   then { handle_illegal(); return RETIRE_FAIL };
diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail
index 9a1b26752..581953802 100755
--- a/model/riscv_insts_vext_red.sail
+++ b/model/riscv_insts_vext_red.sail
@@ -188,7 +188,7 @@ mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = {
 mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveRVV()
   <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveRVV()
 
-val process_rfvv_single: forall 'n 'm 'p, 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired effect {escape, rreg, undef, wreg}
+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 effect {escape, rreg, undef, wreg}
 function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {
   let rm_3b = fcsr.FRM();
   let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */
@@ -227,7 +227,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
   RETIRE_SUCCESS
 }
 
-val process_rfvv_widen: forall 'n 'm 'p, 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired effect {escape, rreg, undef, wreg}
+val process_rfvv_widen: 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 effect {escape, rreg, undef, wreg}
 function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {
   let rm_3b          = fcsr.FRM();
   let SEW_widen      = SEW * 2;
diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
index 1148ea78e..ba52f0927 100755
--- a/model/riscv_insts_vext_utils.sail
+++ b/model/riscv_insts_vext_utils.sail
@@ -280,7 +280,7 @@ function get_end_element() = unsigned(vl) - 1
  *   vector2 is a "mask" vector that is true for an element if the corresponding element
  *     in the result vector should be updated by the calling instruction
  */
-val init_masked_result : forall 'n 'm 'p. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool)) effect {escape, rreg, undef}
+val init_masked_result : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bits('m)), vector('n, dec, bool)) -> (vector('n, dec, bits('m)), vector('n, dec, bool)) effect {escape, rreg, undef}
 function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = {
   let start_element = get_start_element();
   let end_element   = get_end_element();
@@ -333,7 +333,7 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = {
  * (vs3 for store and vs2 for reduction). There's no destination register to be masked.
  * In these cases, this function can be called to simply get the mask vector for vs (without the prepared vd result vector).
  */
-val init_masked_source : forall 'n 'p. (int('n), int('p), vector('n, dec, bool)) -> vector('n, dec, bool) effect {escape, rreg, undef}
+val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, dec, bool)) -> vector('n, dec, bool) effect {escape, rreg, undef}
 function init_masked_source(num_elem, LMUL_pow, vm_val) = {
   let start_element = get_start_element();
   let end_element   = get_end_element();
@@ -367,7 +367,7 @@ function init_masked_source(num_elem, LMUL_pow, vm_val) = {
 
 /* Mask handling for carry functions that use masks as input/output */
 /* Only prestart and tail elements are masked in a mask value */
-val init_masked_result_carry : forall 'n 'm 'p. (int('n), int('m), int('p), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef}
+val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef}
 function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = {
   let start_element = get_start_element();
   let end_element   = get_end_element();
@@ -403,7 +403,7 @@ function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = {
 }
 
 /* Mask handling for cmp functions that use masks as output */
-val init_masked_result_cmp : forall 'n 'm 'p. (int('n), int('m), int('p), vector('n, dec, bool), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef}
+val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, dec, bool), vector('n, dec, bool)) -> (vector('n, dec, bool), vector('n, dec, bool)) effect {escape, rreg, undef}
 function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = {
   let start_element = get_start_element();
   let end_element   = get_end_element();
@@ -450,7 +450,7 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = {
  *   Read multiple register groups and concatenate them in parallel
  *   The whole segments with the same element index are combined together
  */
-val read_vreg_seg : forall 'n 'm 'p 'q. (int('n), int('m), int('p), int('q), regidx) -> vector('n, dec, bits('q * 'm)) effect {escape, rreg, undef}
+val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'q >= 0. (int('n), int('m), int('p), int('q), regidx) -> vector('n, dec, bits('q * 'm)) effect {escape, rreg, undef}
 function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = {
   assert('q * 'm > 0);
   let LMUL_reg : int = if LMUL_pow <= 0 then 1 else int_power(2, LMUL_pow);
diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail
index 21e23d5df..522e76f70 100644
--- a/model/riscv_vext_regs.sail
+++ b/model/riscv_vext_regs.sail
@@ -264,7 +264,7 @@ function get_num_elem(LMUL_pow, SEW) = {
 }
 
 /* Reads a single vreg into multiple elements */
-val read_single_vreg : forall 'n 'm. (int('n), int('m), regidx) -> vector('n, dec, bits('m)) effect {escape, rreg, undef}
+val read_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx) -> vector('n, dec, bits('m)) effect {escape, rreg, undef}
 function read_single_vreg(num_elem, SEW, vrid) = {
   let bv     : vregtype                  = V(vrid);
   var result : vector('n, dec, bits('m)) = undefined;
@@ -279,7 +279,7 @@ function read_single_vreg(num_elem, SEW, vrid) = {
 }
 
 /* Writes multiple elements into a single vreg */
-val write_single_vreg : forall 'n 'm. (int('n), int('m), regidx, vector('n, dec, bits('m))) -> unit effect {escape, rreg, wreg}
+val write_single_vreg : forall 'n 'm, 'n >= 0. (int('n), int('m), regidx, vector('n, dec, bits('m))) -> unit effect {escape, rreg, wreg}
 function write_single_vreg(num_elem, SEW, vrid, v) = {
   r : vregtype = zeros();
 
@@ -293,7 +293,7 @@ function write_single_vreg(num_elem, SEW, vrid, v) = {
 }
 
 /* The general vreg reading operation with num_elem as max(VLMAX,VLEN/SEW)) */
-val read_vreg : forall 'n 'm 'p. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m)) effect {escape, rreg, undef}
+val read_vreg : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), regidx) -> vector('n, dec, bits('m)) effect {escape, rreg, undef}
 function read_vreg(num_elem, SEW, LMUL_pow, vrid) = {
   var result : vector('n, dec, bits('m)) = undefined;
   let VLEN = unsigned(vlenb) * 8;
@@ -311,6 +311,7 @@ function read_vreg(num_elem, SEW, LMUL_pow, vrid) = {
       result = read_single_vreg('n, SEW, vrid);
     } else {
       let 'num_elem_single : int = VLEN / SEW;
+      assert('num_elem_single >= 0);
       foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) {
         let r_start_i : int = i_lmul * 'num_elem_single;
         let r_end_i   : int = r_start_i + 'num_elem_single - 1;
@@ -335,6 +336,7 @@ function read_single_element(EEW, index, vrid) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(VLEN >= EEW);
   let 'elem_per_reg : int = VLEN / EEW;
+  assert('elem_per_reg >= 0);
   let real_vrid  : regidx = vrid + to_bits(5, index / 'elem_per_reg);
   let real_index : int    = index % 'elem_per_reg;
   let vrid_val : vector('elem_per_reg, dec, bits('m)) = read_single_vreg('elem_per_reg, EEW, real_vrid);
@@ -343,12 +345,13 @@ function read_single_element(EEW, index, vrid) = {
 }
 
 /* The general vreg writing operation with num_elem as max(VLMAX,VLEN/SEW)) */
-val write_vreg : forall 'n 'm 'p. (int('n), int('m), int('p), regidx, vector('n, dec, bits('m))) -> unit effect {escape, rreg, undef, wreg}
+val write_vreg : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), regidx, vector('n, dec, bits('m))) -> unit effect {escape, rreg, undef, wreg}
 function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = {
   let VLEN = unsigned(vlenb) * 8;
   let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
 
   let 'num_elem_single  : int = VLEN / SEW;
+  assert('num_elem_single >= 0);
   foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) {
     var single_vec : vector('num_elem_single, dec, bits('m)) = undefined;
     let vrid_lmul  : regidx = vrid + to_bits(5, i_lmul);
@@ -369,6 +372,7 @@ val write_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regi
 function write_single_element(EEW, index, vrid, value) = {
   let VLEN = unsigned(vlenb) * 8;
   let 'elem_per_reg : int = VLEN / EEW;
+  assert('elem_per_reg >= 0);
   let real_vrid  : regidx = vrid + to_bits(5, index / 'elem_per_reg);
   let real_index : int    = index % 'elem_per_reg;
 
@@ -386,7 +390,7 @@ function write_single_element(EEW, index, vrid, value) = {
 }
 
 /* Mask register reading operation with num_elem as max(VLMAX,VLEN/SEW)) */
-val read_vmask : forall 'n. (int('n), bits(1), regidx) -> vector('n, dec, bool) effect {escape, rreg, undef}
+val read_vmask : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) effect {escape, rreg, undef}
 function read_vmask(num_elem, vm, vrid) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(num_elem <= sizeof(vlenmax));
@@ -405,7 +409,7 @@ function read_vmask(num_elem, vm, vrid) = {
 }
 
 /* This is a special version of read_vmask for carry/borrow instructions, where vm=1 means no carry */
-val read_vmask_carry : forall 'n. (int('n), bits(1), regidx) -> vector('n, dec, bool) effect {escape, rreg, undef}
+val read_vmask_carry : forall 'n, 'n >= 0. (int('n), bits(1), regidx) -> vector('n, dec, bool) effect {escape, rreg, undef}
 function read_vmask_carry(num_elem, vm, vrid) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(0 < num_elem & num_elem <= sizeof(vlenmax));
@@ -424,7 +428,7 @@ function read_vmask_carry(num_elem, vm, vrid) = {
 }
 
 /* Mask register writing operation with num_elem as max(VLMAX,VLEN/SEW)) */
-val write_vmask : forall 'n. (int('n), regidx, vector('n, dec, bool)) -> unit effect {escape, rreg, undef, wreg}
+val write_vmask : forall 'n, 'n >= 0. (int('n), regidx, vector('n, dec, bool)) -> unit effect {escape, rreg, undef, wreg}
 function write_vmask(num_elem, vrid, v) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(0 < VLEN & VLEN <= sizeof(vlenmax));