aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/prelude.sail4
-rw-r--r--model/riscv_insts_vext_arith.sail152
-rwxr-xr-xmodel/riscv_insts_vext_fp.sail82
-rwxr-xr-xmodel/riscv_insts_vext_fp_vm.sail10
-rwxr-xr-xmodel/riscv_insts_vext_mask.sail40
-rwxr-xr-xmodel/riscv_insts_vext_utils.sail2
-rwxr-xr-xmodel/riscv_insts_vext_vm.sail60
-rw-r--r--model/riscv_vext_regs.sail116
8 files changed, 196 insertions, 270 deletions
diff --git a/model/prelude.sail b/model/prelude.sail
index 34ff30e..67855c5 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -47,6 +47,8 @@ val sub_vec_int = pure {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits(
overload operator - = {sub_vec, sub_vec_int}
+val quot_positive_round_zero = pure {interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : forall 'n 'm, 'n >= 0 & 'm > 0. (int('n), int('m)) -> int(div('n, 'm))
+
val quot_round_zero = pure {interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
val rem_round_zero = pure {interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
@@ -196,7 +198,7 @@ function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = {
overload reverse = {reverse_bits_in_byte}
-overload operator / = {quot_round_zero}
+overload operator / = {quot_positive_round_zero, quot_round_zero}
overload operator * = {mult_atom, mult_int}
/* helper for vector extension
diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail
index b832dcf..1654f65 100644
--- a/model/riscv_insts_vext_arith.sail
+++ b/model/riscv_insts_vext_arith.sail
@@ -59,10 +59,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -196,10 +195,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
assert(SEW_widen <= 64);
foreach (i from 0 to (num_elem - 1)) {
@@ -263,10 +261,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
assert(SEW_widen <= 64);
foreach (i from 0 to (num_elem - 1)) {
@@ -323,7 +320,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);
- var result : vector('n, dec, bits('m)) = undefined;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
let tail_ag : agtype = get_vtype_vta();
foreach (i from 0 to (num_elem - 1)) {
@@ -367,10 +364,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then result[i] = vs1_val[i]
@@ -427,10 +423,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -548,10 +543,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
assert(SEW_widen <= 64);
foreach (i from 0 to (num_elem - 1)) {
@@ -615,10 +609,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
assert(SEW_widen <= 64);
foreach (i from 0 to (num_elem - 1)) {
@@ -681,10 +674,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -745,7 +737,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);
- var result : vector('n, dec, bits('m)) = undefined;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
let tail_ag : agtype = get_vtype_vta();
foreach (i from 0 to (num_elem - 1)) {
@@ -789,10 +781,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then result[i] = rs1_val
@@ -841,10 +832,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -938,10 +928,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
assert(SEW_widen <= 64);
foreach (i from 0 to (num_elem - 1)) {
@@ -1005,10 +994,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
assert(SEW_widen <= 64);
foreach (i from 0 to (num_elem - 1)) {
@@ -1071,10 +1059,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1135,7 +1122,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);
- var result : vector('n, dec, bits('m)) = undefined;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
let tail_ag : agtype = get_vtype_vta();
foreach (i from 0 to (num_elem - 1)) {
@@ -1179,10 +1166,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then result[i] = imm_val
@@ -1218,7 +1204,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);
- var result : vector('n, dec, bits('m)) = undefined;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
foreach (i from 0 to (num_elem - 1)) {
result[i] = if i < start_element then vd_val[i] else vs2_val[i]
@@ -1274,10 +1260,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1383,10 +1368,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1449,10 +1433,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1518,10 +1501,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1582,10 +1564,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1641,12 +1622,10 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
- assert(SEW > SEW_half);
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
result[i] = match funct6 {
@@ -1699,12 +1678,10 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
- assert(SEW > SEW_quart);
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
result[i] = match funct6 {
@@ -1757,10 +1734,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
assert(SEW > SEW_eighth);
foreach (i from 0 to (num_elem - 1)) {
@@ -1836,7 +1812,7 @@ 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);
- var result : vector('n, dec, bits('m)) = undefined;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
/* body elements */
var vd_idx : nat = 0;
@@ -1907,10 +1883,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -2027,10 +2002,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -2093,10 +2067,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -2161,10 +2134,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -2225,10 +2197,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -2275,10 +2246,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
+ var result = initial_result;
/* one body element */
if mask[0] then result[0] = rs1_val;
diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail
index 83006d1..72bdca2 100755
--- a/model/riscv_insts_vext_fp.sail
+++ b/model/riscv_insts_vext_fp.sail
@@ -46,10 +46,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -121,10 +120,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -194,10 +192,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -259,10 +256,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -322,10 +318,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -379,10 +374,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -498,10 +492,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -628,10 +621,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -759,10 +751,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -884,10 +875,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -974,10 +964,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1046,10 +1035,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1110,10 +1098,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1172,10 +1159,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW_widen, LMUL_pow_widen, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -1225,7 +1211,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);
- var result : vector('n, dec, bits('m)) = undefined;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
let tail_ag : agtype = get_vtype_vta();
foreach (i from 0 to (num_elem - 1)) {
@@ -1272,10 +1258,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then result[i] = rs1_val
@@ -1309,10 +1294,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, 0, vd_val, vm_val);
+ var result = initial_result;
/* one body element */
if mask[0] then result[0] = rs1_val;
diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail
index 1914ed7..6d578fa 100755
--- a/model/riscv_insts_vext_fp_vm.sail
+++ b/model/riscv_insts_vext_fp_vm.sail
@@ -41,10 +41,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -105,10 +104,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail
index 9c536bb..432ac81 100755
--- a/model/riscv_insts_vext_mask.sail
+++ b/model/riscv_insts_vext_mask.sail
@@ -41,10 +41,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, 0, vd_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -98,10 +97,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
+ var result = initial_result;
var count : nat = 0;
foreach (i from 0 to (num_elem - 1)) {
@@ -134,10 +132,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val);
+ var result = initial_result;
var index : int = -1;
foreach (i from 0 to (num_elem - 1)) {
@@ -174,10 +171,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+ var result = initial_result;
var found_elem : bool = false;
foreach (i from 0 to (num_elem - 1)) {
@@ -215,10 +211,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+ var result = initial_result;
var found_elem : bool = false;
foreach (i from 0 to (num_elem - 1)) {
@@ -256,10 +251,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val);
+ var result = initial_result;
var found_elem : bool = false;
foreach (i from 0 to (num_elem - 1)) {
@@ -301,10 +295,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
var sum : int = 0;
foreach (i from 0 to (num_elem - 1)) {
@@ -340,10 +333,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then result[i] = to_bits(SEW, i)
diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
index 87cb386..eeec681 100755
--- a/model/riscv_insts_vext_utils.sail
+++ b/model/riscv_insts_vext_utils.sail
@@ -199,7 +199,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))
+val init_masked_result : forall 'n 'm 'p, 'n >= 0 & 'm >= 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();
diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail
index e524b75..93ad7e7 100755
--- a/model/riscv_insts_vext_vm.sail
+++ b/model/riscv_insts_vext_vm.sail
@@ -39,10 +39,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -94,10 +93,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -156,10 +154,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -213,10 +210,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -277,10 +273,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -332,10 +327,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -394,10 +388,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -453,10 +446,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -520,10 +512,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -572,10 +563,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -631,10 +621,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vec_trues);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
@@ -686,10 +675,9 @@ 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);
- 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);
+ let (initial_result, mask) = init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val);
+ var result = initial_result;
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail
index 377d92d..f823155 100644
--- a/model/riscv_vext_regs.sail
+++ b/model/riscv_vext_regs.sail
@@ -87,48 +87,43 @@ function dirty_v_context_if_present() -> unit = {
}
function rV (r : regno) -> vregtype = {
- let zero_vreg : vregtype = zeros();
- let v : vregtype =
- match r {
- 0 => vr0,
- 1 => vr1,
- 2 => vr2,
- 3 => vr3,
- 4 => vr4,
- 5 => vr5,
- 6 => vr6,
- 7 => vr7,
- 8 => vr8,
- 9 => vr9,
- 10 => vr10,
- 11 => vr11,
- 12 => vr12,
- 13 => vr13,
- 14 => vr14,
- 15 => vr15,
- 16 => vr16,
- 17 => vr17,
- 18 => vr18,
- 19 => vr19,
- 20 => vr20,
- 21 => vr21,
- 22 => vr22,
- 23 => vr23,
- 24 => vr24,
- 25 => vr25,
- 26 => vr26,
- 27 => vr27,
- 28 => vr28,
- 29 => vr29,
- 30 => vr30,
- 31 => vr31,
- _ => {assert(false, "invalid vector register number"); zero_vreg}
- };
- v
+ match r {
+ 0 => vr0,
+ 1 => vr1,
+ 2 => vr2,
+ 3 => vr3,
+ 4 => vr4,
+ 5 => vr5,
+ 6 => vr6,
+ 7 => vr7,
+ 8 => vr8,
+ 9 => vr9,
+ 10 => vr10,
+ 11 => vr11,
+ 12 => vr12,
+ 13 => vr13,
+ 14 => vr14,
+ 15 => vr15,
+ 16 => vr16,
+ 17 => vr17,
+ 18 => vr18,
+ 19 => vr19,
+ 20 => vr20,
+ 21 => vr21,
+ 22 => vr22,
+ 23 => vr23,
+ 24 => vr24,
+ 25 => vr25,
+ 26 => vr26,
+ 27 => vr27,
+ 28 => vr28,
+ 29 => vr29,
+ 30 => vr30,
+ 31 => vr31,
+ }
}
-function wV (r : regno, in_v : vregtype) -> unit = {
- let v = in_v;
+function wV (r : regno, v : vregtype) -> unit = {
match r {
0 => vr0 = v,
1 => vr1 = v,
@@ -162,7 +157,6 @@ function wV (r : regno, in_v : vregtype) -> unit = {
29 => vr29 = v,
30 => vr30 = v,
31 => vr31 = v,
- _ => assert(false, "invalid vector register number")
};
dirty_v_context();
@@ -245,10 +239,10 @@ 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))
+val read_single_vreg : forall 'n 'm, 'n >= 0 & 'm >= 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;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
assert(8 <= SEW & SEW <= 64);
foreach (i from 0 to (num_elem - 1)) {
@@ -274,9 +268,9 @@ 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))
+val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 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;
+ var result : vector('n, dec, bits('m)) = vector_init(zeros());
let VLEN = unsigned(vlenb) * 8;
let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
@@ -326,7 +320,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
+val write_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 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;
@@ -334,7 +328,7 @@ function write_vreg(num_elem, SEW, LMUL_pow, vrid, vec) = {
let 'num_elem_single : int = VLEN / SEW;
assert('num_elem_single >= 0);
foreach (i_lmul from 0 to (2 ^ LMUL_pow_reg - 1)) {
- var single_vec : vector('num_elem_single, dec, bits('m)) = undefined;
+ var single_vec : vector('num_elem_single, dec, bits('m)) = vector_init(zeros());
let vrid_lmul : regidx = vrid + to_bits(5, i_lmul);
let r_start_i : int = i_lmul * 'num_elem_single;
let r_end_i : int = r_start_i + 'num_elem_single - 1;
@@ -373,17 +367,16 @@ 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)
function read_vmask(num_elem, vm, vrid) = {
- let VLEN = unsigned(vlenb) * 8;
assert(num_elem <= sizeof(vlenmax));
let vreg_val : vregtype = V(vrid);
- var result : vector('n, dec, bool) = undefined;
+ var result : vector('n, dec, bool) = vector_init(true);
+
+ if vm == 0b1 then {
+ return result
+ };
foreach (i from 0 to (num_elem - 1)) {
- if vm == 0b1 then {
- result[i] = true
- } else {
- result[i] = bit_to_bool(vreg_val[i])
- }
+ result[i] = bit_to_bool(vreg_val[i])
};
result
@@ -392,17 +385,16 @@ 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)
function read_vmask_carry(num_elem, vm, vrid) = {
- let VLEN = unsigned(vlenb) * 8;
- assert(0 < num_elem & num_elem <= sizeof(vlenmax));
+ assert(num_elem <= sizeof(vlenmax));
let vreg_val : vregtype = V(vrid);
- var result : vector('n, dec, bool) = undefined;
+ var result : vector('n, dec, bool) = vector_init(false);
+
+ if vm == 0b1 then {
+ return result
+ };
foreach (i from 0 to (num_elem - 1)) {
- if vm == 0b1 then {
- result[i] = false
- } else {
- result[i] = bit_to_bool(vreg_val[i])
- }
+ result[i] = bit_to_bool(vreg_val[i])
};
result
generated by cgit v1.1 at 2024-10-19 21:22:57 +0000