Remove effect annotations from vector extension

6 files changed, 79 insertions, 79 deletions

diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
index 292d98f..85adcfd 100644
--- a/model/riscv_insts_vext_mem.sail
+++ b/model/riscv_insts_vext_mem.sail
@@ -104,7 +104,7 @@ 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()
 
-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 effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
   let width_type : word_width = bytes_wordwidth(load_width_bytes);
@@ -170,7 +170,7 @@ 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()
 
-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 effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
   let width_type : word_width = bytes_wordwidth(load_width_bytes);
@@ -275,7 +275,7 @@ 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()
 
-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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
   let width_type : word_width = bytes_wordwidth(load_width_bytes);
@@ -344,7 +344,7 @@ union clause ast = VLSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg
 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()
 
-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 effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
   let width_type : word_width = bytes_wordwidth(load_width_bytes);
@@ -411,7 +411,7 @@ union clause ast = VSSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg
 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()
 
-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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
   let width_type : word_width = bytes_wordwidth(load_width_bytes);
@@ -481,7 +481,7 @@ union clause ast = VLUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re
 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()
 
-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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else int_power(2, EMUL_data_pow);
   let width_type : word_width = bytes_wordwidth(EEW_data_bytes);
@@ -573,7 +573,7 @@ union clause ast = VSUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re
 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()
 
-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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else int_power(2, EMUL_data_pow);
   let width_type : word_width = bytes_wordwidth(EEW_data_bytes);
@@ -668,7 +668,7 @@ 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()
 
-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 effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let width_type : word_width = bytes_wordwidth(load_width_bytes);
   let start_element = get_start_element();
@@ -750,7 +750,7 @@ 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()
 
-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 effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let width_type : word_width = BYTE;
   let start_element = get_start_element();
@@ -855,7 +855,7 @@ mapping encdec_lsop : vmlsop <-> bits(7) = {
 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()
 
-val process_vm : forall 'n 'l, ('n >= 0 & 'l >= 0). (regidx, regidx, int('n), int('l), vmlsop) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
+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) = {
   let width_type : word_width = BYTE;
   let start_element = get_start_element();
diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail
index 6b756f1..be6afc3 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 haveVExt()
   <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
-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}
+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) = {
   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, '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}
+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
 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 bef5b51..061da54 100755
--- a/model/riscv_insts_vext_utils.sail
+++ b/model/riscv_insts_vext_utils.sail
@@ -51,7 +51,7 @@ mapping maybe_vmask : string <-> bits(1) = {
  *  1. vector widening/narrowing instructions
  *  2. vector load/store instructions
  */
-val valid_eew_emul : (int, int) -> bool effect {rreg}
+val valid_eew_emul : (int, int) -> bool
 function valid_eew_emul(EEW, EMUL_pow) = {
   let ELEN = int_power(2, get_elen_pow());
   EEW >= 8 & EEW <= ELEN & EMUL_pow >= -3 & EMUL_pow <= 3
@@ -61,13 +61,13 @@ function valid_eew_emul(EEW, EMUL_pow) = {
  *  1. If the vill bit is set, then any attempt to execute a vector instruction that depends upon vtype will raise an illegal instruction exception.
  *  2. vset{i}vl{i} and whole-register loads, stores, and moves do not depend upon vtype.
  */
-val valid_vtype : unit -> bool effect {rreg}
+val valid_vtype : unit -> bool
 function valid_vtype() = {
   vtype.vill() == 0b0
 }
 
 /* Check for vstart value */
-val assert_vstart : int -> bool effect {rreg}
+val assert_vstart : int -> bool
 function assert_vstart(i) = {
   unsigned(vstart) == i
 }
@@ -242,7 +242,7 @@ function illegal_indexed_store(nf, EEW_index, EMUL_pow_index, EMUL_pow_data) = {
 }
 
 /* Scalar register shaping */
-val get_scalar : forall 'm, 'm >= 8. (regidx, int('m)) -> bits('m) effect {escape, rreg}
+val get_scalar : forall 'm, 'm >= 8. (regidx, int('m)) -> bits('m)
 function get_scalar(rs1, SEW) = {
   if SEW <= sizeof(xlen) then {
     /* Least significant SEW bits */
@@ -254,7 +254,7 @@ function get_scalar(rs1, SEW) = {
 }
 
 /* Get the starting element index from csr vtype */
-val get_start_element : unit -> nat effect {escape, rreg, wreg}
+val get_start_element : unit -> nat
 function get_start_element() = {
   let start_element = unsigned(vstart);
   let VLEN_pow = get_vlen_pow();
@@ -269,7 +269,7 @@ function get_start_element() = {
 }
 
 /* Get the ending element index from csr vl */
-val get_end_element : unit -> int effect {escape, rreg, wreg}
+val get_end_element : unit -> int
 function get_end_element() = unsigned(vl) - 1
 
 /* Mask handling; creates a pre-masked result vector for vstart, vl, vta/vma, and vm */
@@ -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, '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}
+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))
 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, 'n >= 0. (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)
 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, 'n >= 0. (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))
 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, '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}
+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))
 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, 'n >= 0 & 'q >= 0. (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))
 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);
@@ -579,7 +579,7 @@ function f_is_NaN(xf) = {
 }
 
 /* Scalar register shaping for floating point operations */
-val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) effect {escape, rreg}
+val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n)
 function get_scalar_fp(rs1, SEW) = {
   assert(sizeof(flen) >= SEW, "invalid vector floating-point type width: FLEN < SEW");
   match SEW {
@@ -590,7 +590,7 @@ function get_scalar_fp(rs1, SEW) = {
 }
 
 /* Shift amounts */
-val get_shift_amount : forall 'n 'm, 0 <= 'n & 'm in {8, 16, 32, 64}. (bits('n), int('m)) -> nat effect {escape}
+val get_shift_amount : forall 'n 'm, 0 <= 'n & 'm in {8, 16, 32, 64}. (bits('n), int('m)) -> nat
 function get_shift_amount(bit_val, SEW) = {
   let lowlog2bits = log2(SEW);
   assert(0 < lowlog2bits & lowlog2bits < 'n);
@@ -598,7 +598,7 @@ function get_shift_amount(bit_val, SEW) = {
 }
 
 /* Fixed point rounding increment */
-val get_fixed_rounding_incr : forall ('m 'n : Int), ('m > 0 & 'n >= 0). (bits('m), int('n)) -> bits(1) effect {rreg, undef}
+val get_fixed_rounding_incr : forall ('m 'n : Int), ('m > 0 & 'n >= 0). (bits('m), int('n)) -> bits(1)
 function get_fixed_rounding_incr(vec_elem, shift_amount) = {
   if shift_amount == 0 then 0b0
   else {
@@ -615,7 +615,7 @@ function get_fixed_rounding_incr(vec_elem, shift_amount) = {
 }
 
 /* Fixed point unsigned saturation */
-val unsigned_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m) effect {escape, rreg, undef, wreg}
+val unsigned_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m)
 function unsigned_saturation(len, elem) = {
   if unsigned(elem) > unsigned(ones('m)) then {
     vxsat = 0b1;
@@ -627,7 +627,7 @@ function unsigned_saturation(len, elem) = {
 }
 
 /* Fixed point signed saturation */
-val signed_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m) effect {escape, rreg, undef, wreg}
+val signed_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m)
 function signed_saturation(len, elem) = {
   if signed(elem) > signed(0b0 @ ones('m - 1)) then {
     vxsat = 0b1;
@@ -642,7 +642,7 @@ function signed_saturation(len, elem) = {
 }
 
 /* Get the floating point rounding mode from csr fcsr */
-val get_fp_rounding_mode : unit -> rounding_mode effect {rreg}
+val get_fp_rounding_mode : unit -> rounding_mode
 function get_fp_rounding_mode() = encdec_rounding_mode(fcsr.FRM())
 
 /* Negate a floating point number */
@@ -656,7 +656,7 @@ function negate_fp(xf) = {
 }
 
 /* Floating point functions using softfloat interface */
-val fp_add: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_add: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m)
 function fp_add(rm_3b, op1, op2) = {
   let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm {
     16  => riscv_f16Add(rm_3b, op1, op2),
@@ -667,7 +667,7 @@ function fp_add(rm_3b, op1, op2) = {
   result_val
 }
 
-val fp_sub: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_sub: forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m)
 function fp_sub(rm_3b, op1, op2) = {
   let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm {
     16  => riscv_f16Sub(rm_3b, op1, op2),
@@ -678,7 +678,7 @@ function fp_sub(rm_3b, op1, op2) = {
   result_val
 }
 
-val fp_min : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_min : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m)
 function fp_min(op1, op2) = {
   let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm {
     16  => riscv_f16Lt_quiet(op1, op2),
@@ -697,7 +697,7 @@ function fp_min(op1, op2) = {
   result_val
 }
 
-val fp_max : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_max : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bits('m)
 function fp_max(op1, op2) = {
   let (fflags, op1_lt_op2) : (bits_fflags, bool) = match 'm {
     16  => riscv_f16Lt_quiet(op1, op2),
@@ -716,7 +716,7 @@ function fp_max(op1, op2) = {
   result_val
 }
 
-val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg}
+val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
 function fp_eq(op1, op2) = {
   let (fflags, result_val) : (bits_fflags, bool) = match 'm {
     16  => riscv_f16Eq(op1, op2),
@@ -727,7 +727,7 @@ function fp_eq(op1, op2) = {
   result_val
 }
 
-val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg}
+val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
 function fp_gt(op1, op2) = {
   let (fflags, temp_val) : (bits_fflags, bool) = match 'm {
     16  => riscv_f16Le(op1, op2),
@@ -739,7 +739,7 @@ function fp_gt(op1, op2) = {
   result_val
 }
 
-val fp_ge : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg}
+val fp_ge : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
 function fp_ge(op1, op2) = {
   let (fflags, temp_val) : (bits_fflags, bool) = match 'm {
     16  => riscv_f16Lt(op1, op2),
@@ -751,7 +751,7 @@ function fp_ge(op1, op2) = {
   result_val
 }
 
-val fp_lt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg}
+val fp_lt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
 function fp_lt(op1, op2) = {
   let (fflags, result_val) : (bits_fflags, bool) = match 'm {
     16  => riscv_f16Lt(op1, op2),
@@ -762,7 +762,7 @@ function fp_lt(op1, op2) = {
   result_val
 }
 
-val fp_le : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool effect {escape, rreg, undef, wreg}
+val fp_le : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
 function fp_le(op1, op2) = {
   let (fflags, result_val) : (bits_fflags, bool) = match 'm {
     16  => riscv_f16Le(op1, op2),
@@ -773,7 +773,7 @@ function fp_le(op1, op2) = {
   result_val
 }
 
-val fp_mul : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_mul : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m)
 function fp_mul(rm_3b, op1, op2) = {
   let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm {
     16  => riscv_f16Mul(rm_3b, op1, op2),
@@ -784,7 +784,7 @@ function fp_mul(rm_3b, op1, op2) = {
   result_val
 }
 
-val fp_div : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_div : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m)) -> bits('m)
 function fp_div(rm_3b, op1, op2) = {
   let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm {
     16  => riscv_f16Div(rm_3b, op1, op2),
@@ -795,7 +795,7 @@ function fp_div(rm_3b, op1, op2) = {
   result_val
 }
 
-val fp_muladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_muladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m)
 function fp_muladd(rm_3b, op1, op2, opadd) = {
   let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm {
     16  => riscv_f16MulAdd(rm_3b, op1, op2, opadd),
@@ -806,7 +806,7 @@ function fp_muladd(rm_3b, op1, op2, opadd) = {
   result_val
 }
 
-val fp_nmuladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_nmuladd : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m)
 function fp_nmuladd(rm_3b, op1, op2, opadd) = {
   let op1 = negate_fp(op1);
   let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm {
@@ -818,7 +818,7 @@ function fp_nmuladd(rm_3b, op1, op2, opadd) = {
   result_val
 }
 
-val fp_mulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_mulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m)
 function fp_mulsub(rm_3b, op1, op2, opsub) = {
   let opsub = negate_fp(opsub);
   let (fflags, result_val) : (bits_fflags, bits('m)) = match 'm {
@@ -830,7 +830,7 @@ function fp_mulsub(rm_3b, op1, op2, opsub) = {
   result_val
 }
 
-val fp_nmulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m) effect {escape, rreg, undef, wreg}
+val fp_nmulsub : forall 'm, 'm in {16, 32, 64}. (bits(3), bits('m), bits('m), bits('m)) -> bits('m)
 function fp_nmulsub(rm_3b, op1, op2, opsub) = {
   let opsub = negate_fp(opsub);
   let op1 = negate_fp(op1);
@@ -861,7 +861,7 @@ function fp_class(xf) = {
   zero_extend(result_val_10b)
 }
 
-val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) effect {escape, rreg, undef, wreg}
+val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2)
 function fp_widen(nval) = {
   let rm_3b = fcsr.FRM();
   let (fflags, wval) : (bits_fflags, bits('m * 2)) = match 'm {
@@ -873,7 +873,7 @@ function fp_widen(nval) = {
 }
 
 /* Floating point functions without softfloat support */
-val riscv_f16ToI16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) effect {rreg}
+val riscv_f16ToI16 : (bits_rm, bits_H) -> (bits_fflags, bits(16))
 function riscv_f16ToI16 (rm, v) = {
   let (_, sig32) = riscv_f16ToI32(rm, v);
   if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15))
@@ -881,7 +881,7 @@ function riscv_f16ToI16 (rm, v) = {
   else (zeros(5), sig32[15 .. 0]);
 }
 
-val riscv_f16ToI8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) effect {rreg}
+val riscv_f16ToI8 : (bits_rm, bits_H) -> (bits_fflags, bits(8))
 function riscv_f16ToI8 (rm, v) = {
   let (_, sig32) = riscv_f16ToI32(rm, v);
   if signed(sig32) > signed(0b0 @ ones(7)) then (nvFlag(), 0b0 @ ones(7))
@@ -889,7 +889,7 @@ function riscv_f16ToI8 (rm, v) = {
   else (zeros(5), sig32[7 .. 0]);
 }
 
-val riscv_f32ToI16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) effect {rreg}
+val riscv_f32ToI16 : (bits_rm, bits_S) -> (bits_fflags, bits(16))
 function riscv_f32ToI16 (rm, v) = {
   let (_, sig32) = riscv_f32ToI32(rm, v);
   if signed(sig32) > signed(0b0 @ ones(15)) then (nvFlag(), 0b0 @ ones(15))
@@ -897,21 +897,21 @@ function riscv_f32ToI16 (rm, v) = {
   else (zeros(5), sig32[15 .. 0]);
 }
 
-val riscv_f16ToUi16 : (bits_rm, bits_H) -> (bits_fflags, bits(16)) effect {rreg}
+val riscv_f16ToUi16 : (bits_rm, bits_H) -> (bits_fflags, bits(16))
 function riscv_f16ToUi16 (rm, v) = {
   let (_, sig32) = riscv_f16ToUi32(rm, v);
   if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16))
   else (zeros(5), sig32[15 .. 0]);
 }
 
-val riscv_f16ToUi8 : (bits_rm, bits_H) -> (bits_fflags, bits(8)) effect {rreg}
+val riscv_f16ToUi8 : (bits_rm, bits_H) -> (bits_fflags, bits(8))
 function riscv_f16ToUi8 (rm, v) = {
   let (_, sig32) = riscv_f16ToUi32(rm, v);
   if unsigned(sig32) > unsigned(ones(8)) then (nvFlag(), ones(8))
   else (zeros(5), sig32[7 .. 0]);
 }
 
-val riscv_f32ToUi16 : (bits_rm, bits_S) -> (bits_fflags, bits(16)) effect {rreg}
+val riscv_f32ToUi16 : (bits_rm, bits_S) -> (bits_fflags, bits(16))
 function riscv_f32ToUi16 (rm, v) = {
   let (_, sig32) = riscv_f32ToUi32(rm, v);
   if unsigned(sig32) > unsigned(ones(16)) then (nvFlag(), ones(16))
@@ -974,7 +974,7 @@ function rsqrt7 (v, sub) = {
   zero_extend(64, sign @ out_exp @ out_sig)
 }
 
-val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Rsqrte7 (rm, v) = {
   let class = fp_class(v);
   let (fflags, result) : (bits_fflags, bits_H)= match class {
@@ -992,7 +992,7 @@ function riscv_f16Rsqrte7 (rm, v) = {
   (fflags, result)
 }
 
-val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val riscv_f32Rsqrte7 : (bits_rm, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Rsqrte7 (rm, v) = {
   let class = fp_class(v);
   let (fflags, result) : (bits_fflags, bits_S)= match class[15 .. 0] {
@@ -1010,7 +1010,7 @@ function riscv_f32Rsqrte7 (rm, v) = {
   (fflags, result)
 }
 
-val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val riscv_f64Rsqrte7 : (bits_rm, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Rsqrte7 (rm, v) = {
   let class = fp_class(v);
   let (fflags, result) : (bits_fflags, bits_D)= match class[15 .. 0] {
@@ -1087,7 +1087,7 @@ function recip7 (v, rm_3b, sub) = {
     } else (false, zero_extend(64, sign @ out_exp @ out_sig))
 }
 
-val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Recip7 (rm, v) = {
   let class = fp_class(v);
   let (round_abnormal_true, res_true) = recip7(v, rm, true);
@@ -1106,7 +1106,7 @@ function riscv_f16Recip7 (rm, v) = {
   (fflags, result)
 }
 
-val riscv_f32Recip7 : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val riscv_f32Recip7 : (bits_rm, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Recip7 (rm, v) = {
   let class = fp_class(v);
   let (round_abnormal_true, res_true) = recip7(v, rm, true);
@@ -1125,7 +1125,7 @@ function riscv_f32Recip7 (rm, v) = {
   (fflags, result)
 }
 
-val riscv_f64Recip7 : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val riscv_f64Recip7 : (bits_rm, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Recip7 (rm, v) = {
   let class = fp_class(v);
   let (round_abnormal_true, res_true) = recip7(v, rm, true);
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index f472ca2..84f708e 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -901,7 +901,7 @@ register vtype : Vtype
 
 /* the dynamic selected element width (SEW) */
 /* this returns the power of 2 for SEW */
-val get_sew_pow : unit -> {|3, 4, 5, 6|} effect {escape, rreg}
+val get_sew_pow : unit -> {|3, 4, 5, 6|}
 function get_sew_pow() = {
   let SEW_pow : {|3, 4, 5, 6|} = match vtype.vsew() {
     0b000 => 3,
@@ -913,7 +913,7 @@ function get_sew_pow() = {
   SEW_pow
 }
 /* this returns the actual value of SEW */
-val get_sew : unit -> {|8, 16, 32, 64|} effect {escape, rreg}
+val get_sew : unit -> {|8, 16, 32, 64|}
 function get_sew() = {
   match get_sew_pow() {
     3 => 8,
@@ -923,7 +923,7 @@ function get_sew() = {
   }
 }
 /* this returns the value of SEW in bytes */
-val get_sew_bytes : unit -> {|1, 2, 4, 8|} effect {escape, rreg}
+val get_sew_bytes : unit -> {|1, 2, 4, 8|}
 function get_sew_bytes() = {
   match get_sew_pow() {
     3 => 1,
@@ -935,7 +935,7 @@ function get_sew_bytes() = {
 
 /* the vector register group multiplier (LMUL) */
 /* this returns the power of 2 for LMUL */
-val get_lmul_pow : unit -> {|-3, -2, -1, 0, 1, 2, 3|} effect {escape, rreg}
+val get_lmul_pow : unit -> {|-3, -2, -1, 0, 1, 2, 3|}
 function get_lmul_pow() = {
   match vtype.vlmul() {
     0b101 => -3,
@@ -959,8 +959,8 @@ function decode_agtype(ag) = {
   }
 }
 
-val get_vtype_vma : unit -> agtype effect {rreg}
+val get_vtype_vma : unit -> agtype
 function get_vtype_vma() = decode_agtype(vtype.vma())
 
-val get_vtype_vta : unit -> agtype effect {rreg}
+val get_vtype_vta : unit -> agtype
 function get_vtype_vta() = decode_agtype(vtype.vta())
diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail
index 9b5d6e9..7faa50b 100644
--- a/model/riscv_vext_regs.sail
+++ b/model/riscv_vext_regs.sail
@@ -116,7 +116,7 @@ function dirty_v_context_if_present() -> unit = {
   if sys_enable_vext() then dirty_v_context()
 }
 
-val rV : forall 'n, 0 <= 'n < 32. regno('n) -> vregtype effect {rreg, escape}
+val rV : forall 'n, 0 <= 'n < 32. regno('n) -> vregtype
 function rV r = {
   let zero_vreg : vregtype = zeros();
   let v : vregtype =
@@ -158,7 +158,7 @@ function rV r = {
     v
 }
 
-val wV : forall 'n, 0 <= 'n < 32. (regno('n), vregtype) -> unit effect {rreg, wreg, escape}
+val wV : forall 'n, 0 <= 'n < 32. (regno('n), vregtype) -> unit
 function wV (r, in_v) = {
   let v = in_v;
   match r {
@@ -213,7 +213,7 @@ function wV_bits(i: bits(5), data: vregtype) -> unit = {
 
 overload V = {rV_bits, wV_bits, rV, wV}
 
-val init_vregs : unit -> unit effect {wreg}
+val init_vregs : unit -> unit
 function init_vregs () = {
   let zero_vreg : vregtype = zeros();
   vr0  = zero_vreg;
@@ -257,7 +257,7 @@ bitfield Vcsr : bits(3) = {
 }
 register vcsr : Vcsr
 
-val ext_write_vcsr : (bits(2), bits(1)) -> unit effect {rreg, wreg}
+val ext_write_vcsr : (bits(2), bits(1)) -> unit
 function ext_write_vcsr (vxrm_val, vxsat_val) = {
   vcsr->vxrm()  = vxrm_val; /* Note: frm can be an illegal value, 101, 110, 111 */
   vcsr->vxsat() = vxsat_val;
@@ -265,7 +265,7 @@ function ext_write_vcsr (vxrm_val, vxsat_val) = {
 }
 
 /* num_elem means max(VLMAX,VLEN/SEW)) according to Section 5.4 of RVV spec */
-val get_num_elem : (int, int) -> nat effect {escape, rreg}
+val get_num_elem : (int, int) -> nat
 function get_num_elem(LMUL_pow, SEW) = {
   let VLEN = unsigned(vlenb) * 8;
   let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
@@ -277,7 +277,7 @@ function get_num_elem(LMUL_pow, SEW) = {
 }
 
 /* Reads a single vreg into multiple elements */
-val read_single_vreg : forall 'n 'm, 'n >= 0. (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))
 function read_single_vreg(num_elem, SEW, vrid) = {
   let bv     : vregtype                  = V(vrid);
   var result : vector('n, dec, bits('m)) = undefined;
@@ -292,7 +292,7 @@ function read_single_vreg(num_elem, SEW, vrid) = {
 }
 
 /* Writes multiple elements into a single vreg */
-val write_single_vreg : forall 'n 'm, 'n >= 0. (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
 function write_single_vreg(num_elem, SEW, vrid, v) = {
   r : vregtype = zeros();
 
@@ -306,7 +306,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, 'n >= 0. (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))
 function read_vreg(num_elem, SEW, LMUL_pow, vrid) = {
   var result : vector('n, dec, bits('m)) = undefined;
   let VLEN = unsigned(vlenb) * 8;
@@ -344,7 +344,7 @@ function read_vreg(num_elem, SEW, LMUL_pow, vrid) = {
 }
 
 /* Single element reading operation */
-val read_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx) -> bits('m) effect {escape, rreg, undef}
+val read_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx) -> bits('m)
 function read_single_element(EEW, index, vrid) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(VLEN >= EEW);
@@ -358,7 +358,7 @@ 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, 'n >= 0. (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
 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;
@@ -381,7 +381,7 @@ function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = {
 }
 
 /* Single element writing operation */
-val write_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx, bits('m)) -> unit effect {escape, rreg, undef, wreg}
+val write_single_element : forall 'm 'x, 8 <= 'm <= 128. (int('m), int('x), regidx, bits('m)) -> unit
 function write_single_element(EEW, index, vrid, value) = {
   let VLEN = unsigned(vlenb) * 8;
   let 'elem_per_reg : int = VLEN / EEW;
@@ -403,7 +403,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, 'n >= 0. (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)
 function read_vmask(num_elem, vm, vrid) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(num_elem <= sizeof(vlenmax));
@@ -422,7 +422,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, 'n >= 0. (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)
 function read_vmask_carry(num_elem, vm, vrid) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(0 < num_elem & num_elem <= sizeof(vlenmax));
@@ -441,7 +441,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, 'n >= 0. (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
 function write_vmask(num_elem, vrid, v) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(0 < VLEN & VLEN <= sizeof(vlenmax));
diff --git a/model/riscv_vlen.sail b/model/riscv_vlen.sail
index 5e9b375..cd631ba 100644
--- a/model/riscv_vlen.sail
+++ b/model/riscv_vlen.sail
@@ -38,7 +38,7 @@
 
 register elen : bits(1)
 
-val get_elen_pow : unit -> {|5, 6|} effect {rreg}
+val get_elen_pow : unit -> {|5, 6|}
 
 function get_elen_pow() = match elen {
     0b0 => 5,
@@ -51,7 +51,7 @@ function get_elen_pow() = match elen {
 
 register vlen : bits(4)
 
-val get_vlen_pow : unit -> {|5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16|} effect {rreg}
+val get_vlen_pow : unit -> {|5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16|}
 
 function get_vlen_pow() = match vlen {
     0b0000 => 5,