diff --git a/Makefile b/Makefile
index 13e55a720..8cda2816b 100644
--- a/Makefile
+++ b/Makefile
@@ -129,6 +129,7 @@ SAIL_COQ_SRCS  = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SA
 
 PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml)
 
+SAIL_FLAGS += --strict-var
 SAIL_FLAGS += -dno_cast
 SAIL_DOC_FLAGS ?= -doc_embed plain
 
diff --git a/model/prelude.sail b/model/prelude.sail
index 3555296b3..c924a2f53 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -198,7 +198,7 @@ overload operator >>> = {rotate_bits_right, rotater}
 overload operator <<< = {rotate_bits_left, rotatel}
 
 function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = {
-  ys : bits(8) = zeros();
+  var ys : bits(8) = zeros();
   foreach (i from 0 to 7)
     ys[i] = xs[7-i];
   ys
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index 480f47e2e..170c38712 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -35,7 +35,7 @@ function fetch() -> FetchResult =
               then F_RVC(ilo)
               else {
                 /* fetch PC check for the next instruction granule */
-                PC_hi : xlenbits = PC + 2;
+                let PC_hi = PC + 2;
                 match ext_fetch_check_pc(PC, PC_hi) {
                   Ext_FetchAddr_Error(e)      => F_Ext_Error(e),
                   Ext_FetchAddr_OK(use_pc_hi) => {
diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail
index 14700ca34..b832dcf49 100644
--- a/model/riscv_insts_vext_arith.sail
+++ b/model/riscv_insts_vext_arith.sail
@@ -59,8 +59,8 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -196,8 +196,8 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -263,8 +263,8 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -323,7 +323,7 @@ function clause execute(MASKTYPEV(vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -367,8 +367,8 @@ function clause execute(MOVETYPEV(vs1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -427,8 +427,8 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -548,8 +548,8 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -615,8 +615,8 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -681,8 +681,8 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : nat                       = unsigned(X(rs1));
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -745,7 +745,7 @@ function clause execute(MASKTYPEX(vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -789,8 +789,8 @@ function clause execute(MOVETYPEX(rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, 'm);
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -841,8 +841,8 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -938,8 +938,8 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1005,8 +1005,8 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = {
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1071,8 +1071,8 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = {
   let imm_val : nat                       = unsigned(zero_extend(sizeof(xlen), simm));
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1135,7 +1135,7 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -1179,8 +1179,8 @@ function clause execute(MOVETYPEI(vd, simm)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let imm_val : bits('m)                  = sign_extend(simm);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1218,7 +1218,7 @@ function clause execute(VMVRTYPE(vs2, simm, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
 
   foreach (i from 0 to (num_elem - 1)) {
     result[i] = if i < start_element then vd_val[i] else vs2_val[i]
@@ -1274,8 +1274,8 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1383,8 +1383,8 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1449,8 +1449,8 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -1518,8 +1518,8 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -1582,8 +1582,8 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -1641,8 +1641,8 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_half, LMUL_pow_half, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1699,8 +1699,8 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_quart, LMUL_pow_quart, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1757,8 +1757,8 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_eighth, LMUL_pow_eighth, vs2);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1836,10 +1836,10 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
 
   /* body elements */
-  vd_idx : nat = 0;
+  var vd_idx : nat = 0;
   foreach (i from 0 to (num_elem - 1)) {
     if i <= end_element then {
       if vs1_val[i] then {
@@ -1907,8 +1907,8 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -2027,8 +2027,8 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -2093,8 +2093,8 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -2161,8 +2161,8 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -2225,8 +2225,8 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -2275,8 +2275,8 @@ function clause execute(VMVSX(rs1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let rs1_val : bits('m)                  = get_scalar(rs1, 'm);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
 
diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail
index 945199da8..83006d1ef 100755
--- a/model/riscv_insts_vext_fp.sail
+++ b/model/riscv_insts_vext_fp.sail
@@ -46,8 +46,8 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -121,8 +121,8 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -194,8 +194,8 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -259,8 +259,8 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -322,8 +322,8 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -379,8 +379,8 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -498,8 +498,8 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -628,8 +628,8 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -759,8 +759,8 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -884,8 +884,8 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -974,8 +974,8 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1046,8 +1046,8 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -1110,8 +1110,8 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -1172,8 +1172,8 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = {
   let vd_val  : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2);
-  result      : vector('n, dec, bits('o)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('o)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
 
@@ -1225,7 +1225,7 @@ function clause execute(VFMERGE(vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
 
   let tail_ag : agtype = get_vtype_vta();
   foreach (i from 0 to (num_elem - 1)) {
@@ -1272,8 +1272,8 @@ function clause execute(VFMV(rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -1309,8 +1309,8 @@ function clause execute(VFMVSF(rs1, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b1, 0b00000);
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
 
diff --git a/model/riscv_insts_vext_fp_red.sail b/model/riscv_insts_vext_fp_red.sail
index 9d4220da1..28f28ca00 100755
--- a/model/riscv_insts_vext_fp_red.sail
+++ b/model/riscv_insts_vext_fp_red.sail
@@ -45,7 +45,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
   let mask    : vector('n, dec, bool)     = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
 
-  sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
+  var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
   foreach (i from 0 to (num_elem_vs - 1)) {
     if mask[i] then {
       sum = match funct6 {
@@ -88,7 +88,7 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
   let mask    : vector('n, dec, bool)     = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
 
-  sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
+  var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
   foreach (i from 0 to (num_elem_vs - 1)) {
     if mask[i] then {
       /* currently ordered/unordered sum reductions do the same operations */
diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail
index 55592c4a8..1914ed74b 100755
--- a/model/riscv_insts_vext_fp_vm.sail
+++ b/model/riscv_insts_vext_fp_vm.sail
@@ -41,8 +41,8 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -105,8 +105,8 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar_fp(rs1, 'm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail
index 241e210fd..9c536bb0a 100755
--- a/model/riscv_insts_vext_mask.sail
+++ b/model/riscv_insts_vext_mask.sail
@@ -41,8 +41,8 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs1);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool) = undefined;
-  mask        : vector('n, dec, bool) = undefined;
+  var result  : vector('n, dec, bool) = undefined;
+  var mask    : vector('n, dec, bool) = undefined;
 
   (result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val);
 
@@ -98,12 +98,12 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = {
 
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
-  result      : vector('n, dec, bool) = undefined;
-  mask        : vector('n, dec, bool) = undefined;
+  var result  : vector('n, dec, bool) = undefined;
+  var mask    : vector('n, dec, bool) = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
 
-  count : nat = 0;
+  var count : nat = 0;
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] & vs2_val[i] then count = count + 1;
   };
@@ -134,12 +134,12 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = {
 
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
-  result      : vector('n, dec, bool) = undefined;
-  mask        : vector('n, dec, bool) = undefined;
+  var result  : vector('n, dec, bool) = undefined;
+  var mask    : vector('n, dec, bool) = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
 
-  index : int = -1;
+  var index : int = -1;
   foreach (i from 0 to (num_elem - 1)) {
     if index == -1 then {
       if mask[i] & vs2_val[i] then index = i;
@@ -174,12 +174,12 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool) = undefined;
-  mask        : vector('n, dec, bool) = undefined;
+  var result  : vector('n, dec, bool) = undefined;
+  var mask    : vector('n, dec, bool) = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
 
-  found_elem : bool = false;
+  var found_elem : bool = false;
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
       if vs2_val[i] then found_elem = true;
@@ -215,12 +215,12 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool) = undefined;
-  mask        : vector('n, dec, bool) = undefined;
+  var result  : vector('n, dec, bool) = undefined;
+  var mask    : vector('n, dec, bool) = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
 
-  found_elem : bool = false;
+  var found_elem : bool = false;
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
       result[i] = if found_elem then false else true;
@@ -256,12 +256,12 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool) = undefined;
-  mask        : vector('n, dec, bool) = undefined;
+  var result  : vector('n, dec, bool) = undefined;
+  var mask    : vector('n, dec, bool) = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
 
-  found_elem : bool = false;
+  var found_elem : bool = false;
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
       if vs2_val[i] & not(found_elem) then {
@@ -301,12 +301,12 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = {
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vs2_val : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
-  sum : int = 0;
+  var sum : int = 0;
   foreach (i from 0 to (num_elem - 1)) {
     if mask[i] then {
       result[i] = to_bits(SEW, sum);
@@ -340,8 +340,8 @@ function clause execute(VID_V(vm, vd)) = {
 
   let vm_val  : vector('n, dec, bool)     = read_vmask(num_elem, vm, 0b00000);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
index 449d600a9..b2fcc8c57 100644
--- a/model/riscv_insts_vext_mem.sail
+++ b/model/riscv_insts_vext_mem.sail
@@ -143,7 +143,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
 
   let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val);
 
-  trimmed : bool = false;
+  var trimmed : bool = false;
   foreach (i from 0 to (num_elem - 1)) {
     if not(trimmed) then {
       if vm_val[i] then { /* active segments */
@@ -637,8 +637,8 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
   let start_element = get_start_element();
   if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */
   let elem_to_align : int = start_element % elem_per_reg;
-  cur_field : int = start_element / elem_per_reg;
-  cur_elem  : int = start_element;
+  var cur_field : int = start_element / elem_per_reg;
+  var cur_elem  : int = start_element;
 
   if elem_to_align > 0 then {
     foreach (i from elem_to_align to (elem_per_reg - 1)) {
@@ -719,8 +719,8 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
   let start_element = get_start_element();
   if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */
   let elem_to_align : int = start_element % elem_per_reg;
-  cur_field : int = start_element / elem_per_reg;
-  cur_elem  : int = start_element;
+  var cur_field : int = start_element / elem_per_reg;
+  var cur_elem  : int = start_element;
 
   if elem_to_align > 0 then {
     foreach (i from elem_to_align to (elem_per_reg - 1)) {
diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail
index 2ce2f2c47..d01dc0d4f 100755
--- a/model/riscv_insts_vext_red.sail
+++ b/model/riscv_insts_vext_red.sail
@@ -44,7 +44,7 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
   let mask    : vector('n, dec, bool)     = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
 
-  sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
+  var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */
   foreach (i from 0 to (num_elem_vs - 1)) {
     if mask[i] then {
       let elem : bits('o) = match funct6 {
@@ -106,7 +106,7 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2);
   let mask    : vector('n, dec, bool)     = init_masked_source(num_elem_vs, LMUL_pow, vm_val);
 
-  sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
+  var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */
   foreach (i from 0 to (num_elem_vs - 1)) {
     if mask[i] then {
       sum = match funct6 {
diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
index 4bf570671..87cb38677 100755
--- a/model/riscv_insts_vext_utils.sail
+++ b/model/riscv_insts_vext_utils.sail
@@ -205,8 +205,8 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = {
   let end_element   = get_end_element();
   let tail_ag : agtype = get_vtype_vta();
   let mask_ag : agtype = get_vtype_vma();
-  mask : vector('n, dec, bool) = undefined;
-  result : vector('n, dec, bits('m)) = undefined;
+  var mask : vector('n, dec, bool) = undefined;
+  var result : vector('n, dec, bits('m)) = undefined;
 
   /* Determine the actual number of elements when lmul < 1 */
   let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow));
@@ -256,7 +256,7 @@ val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, de
 function init_masked_source(num_elem, LMUL_pow, vm_val) = {
   let start_element = get_start_element();
   let end_element   = get_end_element();
-  mask : vector('n, dec, bool) = undefined;
+  var mask : vector('n, dec, bool) = undefined;
 
   /* Determine the actual number of elements when lmul < 1 */
   let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow));
@@ -290,8 +290,8 @@ val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int(
 function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = {
   let start_element = get_start_element();
   let end_element   = get_end_element();
-  mask : vector('n, dec, bool) = undefined;
-  result : vector('n, dec, bool) = undefined;
+  var mask : vector('n, dec, bool) = undefined;
+  var result : vector('n, dec, bool) = undefined;
 
   /* Determine the actual number of elements when lmul < 1 */
   let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow));
@@ -327,8 +327,8 @@ 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();
   let mask_ag : agtype = get_vtype_vma();
-  mask : vector('n, dec, bool) = undefined;
-  result : vector('n, dec, bool) = undefined;
+  var mask : vector('n, dec, bool) = undefined;
+  var result : vector('n, dec, bool) = undefined;
 
   /* Determine the actual number of elements when lmul < 1 */
   let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow));
@@ -373,8 +373,8 @@ val read_vreg_seg : forall 'n 'm 'p 'q, 'n >= 0 & 'q >= 0. (int('n), int('m), in
 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 2 ^ (LMUL_pow);
-  vreg_list : vector('q, dec, vector('n, dec, bits('m))) = undefined;
-  result : vector('n, dec, bits('q * 'm)) = undefined;
+  var vreg_list : vector('q, dec, vector('n, dec, bits('m))) = undefined;
+  var result : vector('n, dec, bits('q * 'm)) = undefined;
   foreach (j from 0 to (nf - 1)) {
     vreg_list[j] = read_vreg(num_elem, SEW, LMUL_pow, vrid + to_bits(5, j * LMUL_reg));
   };
@@ -441,7 +441,7 @@ function signed_saturation(len, elem) = {
 
 val count_leadingzeros : (bits(64), int) -> int
 function count_leadingzeros (sig, len) = {
-  idx : int = -1;
+  var idx : int = -1;
   assert(len == 10 | len == 23 | len == 52);
   foreach (i from 0 to (len - 1)) {
     if sig[i] == bitone then idx = i;
diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail
index 91ce3f361..e524b75bc 100755
--- a/model/riscv_insts_vext_vm.sail
+++ b/model/riscv_insts_vext_vm.sail
@@ -39,8 +39,8 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
 
@@ -94,8 +94,8 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
 
@@ -147,7 +147,7 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = {
   let 'm = SEW;
 
   /* for bypassing normal masking in init_masked_result */
-  vec_trues : vector('n, dec, bool) = undefined;
+  var vec_trues : vector('n, dec, bool) = undefined;
   foreach (i from 0 to (num_elem - 1)) {
     vec_trues[i] = true
   };
@@ -156,8 +156,8 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
 
@@ -213,8 +213,8 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = {
   let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -277,8 +277,8 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
 
@@ -332,8 +332,8 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
 
@@ -385,7 +385,7 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = {
   let 'm = SEW;
 
   /* for bypassing normal masking in init_masked_result */
-  vec_trues : vector('n, dec, bool) = undefined;
+  var vec_trues : vector('n, dec, bool) = undefined;
   foreach (i from 0 to (num_elem - 1)) {
     vec_trues[i] = true
   };
@@ -394,8 +394,8 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
 
@@ -453,8 +453,8 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = {
   let rs1_val : bits('m)                  = get_scalar(rs1, SEW);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
@@ -520,8 +520,8 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
 
@@ -572,8 +572,8 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
 
@@ -622,7 +622,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = {
   let 'm = SEW;
 
   /* for bypassing normal masking in init_masked_result */
-  vec_trues : vector('n, dec, bool) = undefined;
+  var vec_trues : vector('n, dec, bool) = undefined;
   foreach (i from 0 to (num_elem - 1)) {
     vec_trues[i] = true
   };
@@ -631,8 +631,8 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd);
-  result      : vector('n, dec, bits('m)) = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bits('m)) = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
 
@@ -686,8 +686,8 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = {
   let imm_val : bits('m)                  = sign_extend(simm);
   let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2);
   let vd_val  : vector('n, dec, bool)     = read_vmask(num_elem, 0b0, vd);
-  result      : vector('n, dec, bool)     = undefined;
-  mask        : vector('n, dec, bool)     = undefined;
+  var result  : vector('n, dec, bool)     = undefined;
+  var mask    : vector('n, dec, bool)     = undefined;
 
   (result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
 
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 8e8e47816..21bd82e47 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -93,8 +93,8 @@ function step(step_no : int) -> bool = {
 
 function loop () : unit -> unit = {
   let insns_per_tick = plat_insns_per_tick();
-  i : int = 0;
-  step_no : int = 0;
+  var i : int = 0;
+  var step_no : int = 0;
   while not(htif_done) do {
     let stepped = step(step_no);
     if stepped then {
diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail
index 511e2aca1..377d92d51 100644
--- a/model/riscv_vext_regs.sail
+++ b/model/riscv_vext_regs.sail
@@ -262,7 +262,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
 function write_single_vreg(num_elem, SEW, vrid, v) = {
-  r : vregtype = zeros();
+  var r : vregtype = zeros();
 
   assert(8 <= SEW & SEW <= 64);
   foreach (i from (num_elem - 1) downto 0) {
@@ -358,7 +358,7 @@ function write_single_element(EEW, index, vrid, value) = {
   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);
-  r : vregtype = zeros();
+  var r : vregtype = zeros();
   foreach (i from ('elem_per_reg - 1) downto 0) {
     r = r << EEW;
     if i == real_index then {