From f139c0d45e0874a8535f126ac281868bcfa8ae59 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 20 Sep 2024 04:18:40 +0100 Subject: [PATCH] Vector: Remove now unnecessary uses of undefined Sail 0.18 contains the vector_init primitive, to make initialising vectors with defined values easier. We can use this in some places where the vector code was creating an uninitalised vector, only to then initialize it later. Second, we can remove some uses of undefined by refactoring slightly how init_masked_result is used, which has the added benefit of making mask immutable. Some additional constraints need to be added to use the vector_init primitive. Sail's pattern completeness checker is now smarter than before, so some wildcard cases can also be safely removed. --- model/prelude.sail | 4 +- model/riscv_insts_vext_arith.sail | 152 ++++++++++++------------------ model/riscv_insts_vext_fp.sail | 82 +++++++--------- model/riscv_insts_vext_fp_vm.sail | 10 +- model/riscv_insts_vext_mask.sail | 40 ++++---- model/riscv_insts_vext_utils.sail | 2 +- model/riscv_insts_vext_vm.sail | 60 +++++------- model/riscv_vext_regs.sail | 116 +++++++++++------------ 8 files changed, 196 insertions(+), 270 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index 34ff30e5a..67855c5e9 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 b832dcf49..1654f65f0 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 83006d1ef..72bdca226 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 1914ed74b..6d578fad7 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 9c536bb0a..432ac81bc 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 87cb38677..eeec68124 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 e524b75bc..93ad7e7d2 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 377d92d51..f823155cc 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