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