diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 78d4e3aae..a3800e993 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -55,7 +55,7 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -64,7 +64,7 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VV_VADD => vs2_val[i] + vs1_val[i], VV_VSUB => vs2_val[i] - vs1_val[i], @@ -191,7 +191,7 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -201,7 +201,7 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { NVS_VNSRL => { let shift_amount = get_shift_amount(vs1_val[i], SEW_widen); @@ -257,7 +257,7 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -267,7 +267,7 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { let shift_amount = get_shift_amount(vs1_val[i], SEW_widen); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); result[i] = match funct6 { @@ -316,7 +316,7 @@ function clause execute(MASKTYPEV(vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, 0b0, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -333,7 +333,7 @@ function clause execute(MASKTYPEV(vs2, vs1, vd)) = { } } else { /* the merge operates on all body elements */ - result[i] = if vm_val[i] then vs1_val[i] else vs2_val[i] + result[i] = if vm_val[i] == bitone then vs1_val[i] else vs2_val[i] } }; @@ -361,7 +361,7 @@ function clause execute(MOVETYPEV(vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -369,7 +369,7 @@ function clause execute(MOVETYPEV(vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then result[i] = vs1_val[i] + if mask[i] == bitone then result[i] = vs1_val[i] }; write_vreg(num_elem, SEW, LMUL_pow, vd, result); @@ -419,8 +419,8 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -428,7 +428,7 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VX_VADD => vs2_val[i] + rs1_val, VX_VSUB => vs2_val[i] - rs1_val, @@ -539,9 +539,9 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); @@ -549,7 +549,7 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { NXS_VNSRL => { let shift_amount = get_shift_amount(rs1_val, SEW_widen); @@ -605,9 +605,9 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); @@ -615,7 +615,7 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { let shift_amount = get_shift_amount(rs1_val, SEW_widen); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); result[i] = match funct6 { @@ -670,8 +670,8 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let rs1_val : nat = unsigned(X(rs1)); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let rs1_val : nat = unsigned(X(rs1)); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -679,7 +679,7 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VX_VSLIDEUP => { if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; @@ -733,8 +733,8 @@ function clause execute(MASKTYPEX(vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let vm_val : bits('n) = read_vmask(num_elem, 0b0, 0b00000); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); var result : vector('n, bits('m)) = vector_init(zeros()); @@ -750,7 +750,7 @@ function clause execute(MASKTYPEX(vs2, rs1, vd)) = { } } else { /* the merge operates on all body elements */ - result[i] = if vm_val[i] then rs1_val else vs2_val[i] + result[i] = if vm_val[i] == bitone then rs1_val else vs2_val[i] } }; @@ -778,15 +778,15 @@ function clause execute(MOVETYPEX(rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let rs1_val : bits('m) = get_scalar(rs1, 'm); - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let rs1_val : bits('m) = get_scalar(rs1, 'm); + let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); 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 + if mask[i] == bitone then result[i] = rs1_val }; write_vreg(num_elem, SEW, LMUL_pow, vd, result); @@ -828,8 +828,8 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let imm_val : bits('m) = sign_extend(simm); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -837,7 +837,7 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VI_VADD => vs2_val[i] + imm_val, VI_VRSUB => imm_val - vs2_val[i], @@ -924,9 +924,9 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let imm_val : bits('m) = sign_extend(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); @@ -934,7 +934,7 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { NIS_VNSRL => { let shift_amount = get_shift_amount(imm_val, SEW_widen); @@ -990,9 +990,9 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let imm_val : bits('m) = sign_extend(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); @@ -1000,7 +1000,7 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { let shift_amount = get_shift_amount(imm_val, SEW_widen); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); result[i] = match funct6 { @@ -1055,8 +1055,8 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let imm_val : nat = unsigned(zero_extend(xlen, simm)); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let imm_val : nat = unsigned(zero_extend(xlen, simm)); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1064,7 +1064,7 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VI_VSLIDEUP => { if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; @@ -1118,8 +1118,8 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); - let imm_val : bits('m) = sign_extend(simm); + let vm_val : bits('n) = read_vmask(num_elem, 0b0, 0b00000); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); var result : vector('n, bits('m)) = vector_init(zeros()); @@ -1135,7 +1135,7 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = { } } else { /* the merge operates on all body elements */ - result[i] = if vm_val[i] then imm_val else vs2_val[i] + result[i] = if vm_val[i] == bitone then imm_val else vs2_val[i] } }; @@ -1163,15 +1163,15 @@ function clause execute(MOVETYPEI(vd, simm)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); - let imm_val : bits('m) = sign_extend(simm); + let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); + let imm_val : bits('m) = sign_extend(simm); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); 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 + if mask[i] == bitone then result[i] = imm_val }; write_vreg(num_elem, SEW, LMUL_pow, vd, result); @@ -1201,7 +1201,7 @@ function clause execute(VMVRTYPE(vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vd); var result : vector('n, bits('m)) = vector_init(zeros()); @@ -1256,7 +1256,7 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1265,7 +1265,7 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { MVV_VAADDU => { let result_add = zero_extend('m + 1, vs2_val[i]) + zero_extend('m + 1, vs1_val[i]); @@ -1364,7 +1364,7 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1373,7 +1373,7 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { MVV_VMACC => get_slice_int(SEW, signed(vs1_val[i]) * signed(vs2_val[i]), 0) + vd_val[i], MVV_VNMSAC => vd_val[i] - get_slice_int(SEW, signed(vs1_val[i]) * signed(vs2_val[i]), 0), @@ -1429,7 +1429,7 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -1438,7 +1438,7 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { WVV_VADD => to_bits(SEW_widen, signed(vs2_val[i]) + signed(vs1_val[i])), WVV_VSUB => to_bits(SEW_widen, signed(vs2_val[i]) - signed(vs1_val[i])), @@ -1497,7 +1497,7 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -1506,7 +1506,7 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { WV_VADD => to_bits(SEW_widen, signed(vs2_val[i]) + signed(vs1_val[i])), WV_VSUB => to_bits(SEW_widen, signed(vs2_val[i]) - signed(vs1_val[i])), @@ -1560,7 +1560,7 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -1569,7 +1569,7 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { WMVV_VWMACC => to_bits(SEW_widen, signed(vs1_val[i]) * signed(vs2_val[i])) + vd_val[i], WMVV_VWMACCU => to_bits(SEW_widen, unsigned(vs1_val[i]) * unsigned(vs2_val[i])) + vd_val[i], @@ -1619,7 +1619,7 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { let 'm = SEW; let 'o = SEW_half; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_half, LMUL_pow_half, vs2); @@ -1627,7 +1627,7 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VEXT2_ZVF2 => zero_extend(vs2_val[i]), VEXT2_SVF2 => sign_extend(vs2_val[i]) @@ -1675,7 +1675,7 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { let 'm = SEW; let 'o = SEW_quart; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_quart, LMUL_pow_quart, vs2); @@ -1683,7 +1683,7 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VEXT4_ZVF4 => zero_extend(vs2_val[i]), VEXT4_SVF4 => sign_extend(vs2_val[i]) @@ -1731,7 +1731,7 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { let 'm = SEW; let 'o = SEW_eighth; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_eighth, LMUL_pow_eighth, vs2); @@ -1740,7 +1740,7 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { assert(SEW > SEW_eighth); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VEXT8_ZVF8 => zero_extend(vs2_val[i]), VEXT8_SVF8 => sign_extend(vs2_val[i]) @@ -1809,7 +1809,7 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vs1_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs1); + let vs1_val : bits('n) = read_vmask(num_elem, 0b0, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); var result : vector('n, bits('m)) = vector_init(zeros()); @@ -1818,7 +1818,7 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { var vd_idx : nat = 0; foreach (i from 0 to (num_elem - 1)) { if i <= end_element then { - if vs1_val[i] then { + if vs1_val[i] == bitone then { let 'p = vd_idx; assert('p < 'n); result['p] = vs2_val[i]; @@ -1879,8 +1879,8 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1888,7 +1888,7 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { MVX_VAADDU => { let result_add = zero_extend('m + 1, vs2_val[i]) + zero_extend('m + 1, rs1_val); @@ -1998,8 +1998,8 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -2007,7 +2007,7 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { MVX_VMACC => get_slice_int(SEW, signed(rs1_val) * signed(vs2_val[i]), 0) + vd_val[i], MVX_VNMSAC => vd_val[i] - get_slice_int(SEW, signed(rs1_val) * signed(vs2_val[i]), 0), @@ -2063,16 +2063,16 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); 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 { + if mask[i] == bitone then { result[i] = match funct6 { WVX_VADD => to_bits(SEW_widen, signed(vs2_val[i]) + signed(rs1_val)), WVX_VSUB => to_bits(SEW_widen, signed(vs2_val[i]) - signed(rs1_val)), @@ -2130,16 +2130,16 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); 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 { + if mask[i] == bitone then { result[i] = match funct6 { WX_VADD => to_bits(SEW_widen, signed(vs2_val[i]) + signed(rs1_val)), WX_VSUB => to_bits(SEW_widen, signed(vs2_val[i]) - signed(rs1_val)), @@ -2193,16 +2193,16 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let rs1_val : bits('m) = get_scalar(rs1, SEW); + let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); 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 { + if mask[i] == bitone then { result[i] = match funct6 { WMVX_VWMACCU => (to_bits(SEW_widen, unsigned(rs1_val) * unsigned(vs2_val[i]) )) + vd_val[i], WMVX_VWMACC => (to_bits(SEW_widen, signed(rs1_val) * signed(vs2_val[i]) )) + vd_val[i], @@ -2243,15 +2243,15 @@ function clause execute(VMVSX(rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); - let rs1_val : bits('m) = get_scalar(rs1, 'm); + let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); + let rs1_val : bits('m) = get_scalar(rs1, 'm); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vd); 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; + if mask[0] == bitone then result[0] = rs1_val; /* others treated as tail elements */ let tail_ag : agtype = get_vtype_vta(); diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index bdfdc10a9..c79218682 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -42,7 +42,7 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -51,7 +51,7 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { FVV_VADD => fp_add(rm_3b, vs2_val[i], vs1_val[i]), FVV_VSUB => fp_sub(rm_3b, vs2_val[i], vs1_val[i]), @@ -116,7 +116,7 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -125,7 +125,7 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { FVV_VMACC => fp_muladd(rm_3b, vs1_val[i], vs2_val[i], vd_val[i]), FVV_VNMACC => fp_nmulsub(rm_3b, vs1_val[i], vs2_val[i], vd_val[i]), @@ -188,7 +188,7 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -197,7 +197,7 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { FWVV_VADD => fp_add(rm_3b, fp_widen(vs2_val[i]), fp_widen(vs1_val[i])), FWVV_VSUB => fp_sub(rm_3b, fp_widen(vs2_val[i]), fp_widen(vs1_val[i])), @@ -252,7 +252,7 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -261,7 +261,7 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { FWVV_VMACC => fp_muladd(rm_3b, fp_widen(vs1_val[i]), fp_widen(vs2_val[i]), vd_val[i]), FWVV_VNMACC => fp_nmulsub(rm_3b, fp_widen(vs1_val[i]), fp_widen(vs2_val[i]), vd_val[i]), @@ -314,7 +314,7 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -323,7 +323,7 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { FWV_VADD => fp_add(rm_3b, vs2_val[i], fp_widen(vs1_val[i])), FWV_VSUB => fp_sub(rm_3b, vs2_val[i], fp_widen(vs1_val[i])) @@ -371,7 +371,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -379,7 +379,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match vfunary0 { FV_CVT_XU_F => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { @@ -489,7 +489,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); @@ -497,7 +497,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match vfwunary0 { FWV_CVT_XU_F => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { @@ -618,7 +618,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -626,7 +626,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match vfnunary0 { FNV_CVT_XU_F => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { @@ -748,7 +748,7 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -756,7 +756,7 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match vfunary1 { FVV_VSQRT => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { @@ -871,8 +871,8 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -880,7 +880,7 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VF_VADD => fp_add(rm_3b, vs2_val[i], rs1_val), VF_VSUB => fp_sub(rm_3b, vs2_val[i], rs1_val), @@ -960,8 +960,8 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -969,7 +969,7 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { VF_VMACC => fp_muladd(rm_3b, rs1_val, vs2_val[i], vd_val[i]), VF_VNMACC => fp_nmulsub(rm_3b, rs1_val, vs2_val[i], vd_val[i]), @@ -1031,16 +1031,16 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); 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 { + if mask[i] == bitone then { result[i] = match funct6 { FWVF_VADD => fp_add(rm_3b, fp_widen(vs2_val[i]), fp_widen(rs1_val)), FWVF_VSUB => fp_sub(rm_3b, fp_widen(vs2_val[i]), fp_widen(rs1_val)), @@ -1094,16 +1094,16 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); 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 { + if mask[i] == bitone then { result[i] = match funct6 { FWVF_VMACC => fp_muladd(rm_3b, fp_widen(rs1_val), fp_widen(vs2_val[i]), vd_val[i]), FWVF_VNMACC => fp_nmulsub(rm_3b, fp_widen(rs1_val), fp_widen(vs2_val[i]), vd_val[i]), @@ -1155,16 +1155,16 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); 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 { + if mask[i] == bitone then { result[i] = match funct6 { FWF_VADD => fp_add(rm_3b, vs2_val[i], fp_widen(rs1_val)), FWF_VSUB => fp_sub(rm_3b, vs2_val[i], fp_widen(rs1_val)) @@ -1207,8 +1207,8 @@ function clause execute(VFMERGE(vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b0, 0b00000); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let vm_val : bits('n) = read_vmask(num_elem, 0b0, 0b00000); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); var result : vector('n, bits('m)) = vector_init(zeros()); @@ -1224,7 +1224,7 @@ function clause execute(VFMERGE(vs2, rs1, vd)) = { } } else { /* the merge operates on all body elements */ - result[i] = if vm_val[i] then rs1_val else vs2_val[i] + result[i] = if vm_val[i] == bitone then rs1_val else vs2_val[i] } }; @@ -1255,15 +1255,15 @@ function clause execute(VFMV(rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); 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 + if mask[i] == bitone then result[i] = rs1_val }; write_vreg(num_elem, SEW, LMUL_pow, vd, result); @@ -1291,15 +1291,15 @@ function clause execute(VFMVSF(rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, 0b1, 0b00000); - let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); + let vm_val : bits('n) = read_vmask(num_elem, 0b1, 0b00000); + let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vd); 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; + if mask[0] == bitone then result[0] = rs1_val; /* others treated as tail elements */ let tail_ag : agtype = get_vtype_vta(); diff --git a/model/riscv_insts_vext_fp_red.sail b/model/riscv_insts_vext_fp_red.sail index 1c4946b49..c4b4930bb 100755 --- a/model/riscv_insts_vext_fp_red.sail +++ b/model/riscv_insts_vext_fp_red.sail @@ -26,7 +26,7 @@ mapping encdec_rfvvfunct6 : rfvvfunct6 <-> bits(6) = { mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if extensionEnabled(Ext_V) <-> encdec_rfvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if extensionEnabled(Ext_V) -val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired +val process_rfvv_single: forall 'n 'm 'p, 'n > 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr[FRM]; let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */ @@ -40,14 +40,14 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po let 'd = num_elem_vd; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { - if mask[i] then { + if mask[i] == bitone then { sum = match funct6 { /* currently ordered/unordered sum reductions do the same operations */ FVV_VFREDOSUM => fp_add(rm_3b, sum, vs2_val[i]), @@ -66,7 +66,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po RETIRE_SUCCESS } -val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired +val process_rfvv_widen: forall 'n 'm 'p, 'n > 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = { let rm_3b = fcsr[FRM]; let SEW_widen = SEW * 2; @@ -83,14 +83,14 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { - if mask[i] then { + if mask[i] == bitone then { /* currently ordered/unordered sum reductions do the same operations */ sum = fp_add(rm_3b, sum, fp_widen(vs2_val[i])) } diff --git a/model/riscv_insts_vext_fp_vm.sail b/model/riscv_insts_vext_fp_vm.sail index 2fb4d3e81..714047837 100755 --- a/model/riscv_insts_vext_fp_vm.sail +++ b/model/riscv_insts_vext_fp_vm.sail @@ -37,23 +37,23 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { FVVM_VMFEQ => fp_eq(vs2_val[i], vs1_val[i]), FVVM_VMFNE => ~(fp_eq(vs2_val[i], vs1_val[i])), FVVM_VMFLE => fp_le(vs2_val[i], vs1_val[i]), FVVM_VMFLT => fp_lt(vs2_val[i], vs1_val[i]) }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -100,16 +100,16 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { VFM_VMFEQ => fp_eq(vs2_val[i], rs1_val), VFM_VMFNE => ~(fp_eq(vs2_val[i], rs1_val)), @@ -118,7 +118,7 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { VFM_VMFGE => fp_ge(vs2_val[i], rs1_val), VFM_VMFGT => fp_gt(vs2_val[i], rs1_val) }; - result[i] = res + result[i] = bool_to_bit(res) } }; diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index ae30bc114..9bc546bd2 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -38,24 +38,24 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vs1_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs1); - let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vs1_val : bits('n) = read_vmask(num_elem, 0b0, vs1); + let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { result[i] = match funct6 { - MM_VMAND => vs2_val[i] & vs1_val[i], - MM_VMNAND => not(vs2_val[i] & vs1_val[i]), - MM_VMANDN => vs2_val[i] & not(vs1_val[i]), - MM_VMXOR => vs2_val[i] != vs1_val[i], - MM_VMOR => vs2_val[i] | vs1_val[i], - MM_VMNOR => not(vs2_val[i] | vs1_val[i]), - MM_VMORN => vs2_val[i] | not(vs1_val[i]), - MM_VMXNOR => vs2_val[i] == vs1_val[i] + MM_VMAND => (vs2_val & vs1_val)[i], + MM_VMNAND => ~(vs2_val & vs1_val)[i], + MM_VMANDN => (vs2_val & ~(vs1_val))[i], + MM_VMXOR => (vs2_val ^ vs1_val)[i], + MM_VMOR => (vs2_val | vs1_val)[i], + MM_VMNOR => (~(vs2_val | vs1_val))[i], + MM_VMORN => (vs2_val | ~(vs1_val))[i], + MM_VMXNOR => (vs2_val & vs1_val)[i] } } }; @@ -95,14 +95,14 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); var count : nat = 0; foreach (i from 0 to (num_elem - 1)) { - if mask[i] & vs2_val[i] then count = count + 1; + if (mask & vs2_val)[i] == bitone then count = count + 1; }; X(rd) = to_bits(xlen, count); @@ -129,15 +129,15 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let (_, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); var index : int = -1; foreach (i from 0 to (num_elem - 1)) { if index == -1 then { - if mask[i] & vs2_val[i] then index = i; + if (mask & vs2_val)[i] == bitone then index = i; }; }; @@ -166,18 +166,18 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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)) { - if mask[i] then { - if vs2_val[i] then found_elem = true; - result[i] = if found_elem then false else true + if mask[i] == bitone then { + if vs2_val[i] == bitone then found_elem = true; + result[i] = bool_to_bit(not(found_elem)) } }; @@ -206,18 +206,18 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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)) { - if mask[i] then { - result[i] = if found_elem then false else true; - if vs2_val[i] then found_elem = true + if mask[i] == bitone then { + result[i] = bool_to_bit(not(found_elem)); + if vs2_val[i] == bitone then found_elem = true } }; @@ -246,21 +246,21 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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)) { - if mask[i] then { - if vs2_val[i] & not(found_elem) then { - result[i] = true; + if mask[i] == bitone then { + if (vs2_val[i] == bitone) & found_elem then { + result[i] = bitone; found_elem = true } else { - result[i] = false + result[i] = bitzero } } }; @@ -290,8 +290,8 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let vs2_val : vector('n, bool) = read_vmask(num_elem, 0b0, vs2); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); + let vs2_val : bits('n) = read_vmask(num_elem, 0b0, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let (initial_result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); @@ -299,9 +299,9 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = { var sum : int = 0; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = to_bits(SEW, sum); - if vs2_val[i] then sum = sum + 1 + if vs2_val[i] == bitone then sum = sum + 1 } }; @@ -329,14 +329,14 @@ function clause execute(VID_V(vm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); 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) + if mask[i] == bitone then result[i] = to_bits(SEW, i) }; write_vreg(num_elem, SEW, LMUL_pow, vd, result); diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index febded099..5e5d8db31 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -67,17 +67,17 @@ union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired +val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { /* active segments */ + if mask[i] == bitone then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; @@ -119,6 +119,8 @@ function clause execute(VLSEGTYPE(nf, vm, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_pow, EEW); /* # of element of each register group */ let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlseg(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) @@ -133,11 +135,11 @@ union clause ast = VLSEGFFTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ vm @ 0b10000 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired +val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let tail_ag : agtype = get_vtype_vta(); @@ -146,7 +148,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) var trimmed : bool = false; foreach (i from 0 to (num_elem - 1)) { if not(trimmed) then { - if mask[i] then { /* active segments */ + if mask[i] == bitone then { /* active segments */ foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { @@ -224,6 +226,8 @@ function clause execute(VLSEGFFTYPE(nf, vm, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlsegff(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) @@ -238,16 +242,16 @@ union clause ast = VSSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b00 @ vm @ 0b00000 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) -val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired +val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); - let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); + let mask : bits('n) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { /* active segments */ + if mask[i] == bitone then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; @@ -293,6 +297,8 @@ function clause execute(VSSEGTYPE(nf, vm, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_store(nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vsseg(nf_int, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) @@ -307,18 +313,18 @@ union clause ast = VLSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired +val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); let rs2_val : int = unsigned(get_scalar(rs2, xlen)); let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { /* active segments */ + if mask[i] == bitone then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; @@ -360,6 +366,8 @@ function clause execute(VLSSEGTYPE(nf, vm, rs2, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_load(vd, vm, nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlsseg(nf_int, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) @@ -374,17 +382,17 @@ union clause ast = VSSSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, reg mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b10 @ vm @ rs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) -val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired +val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let EMUL_reg : int = if EMUL_pow <= 0 then 1 else 2 ^ EMUL_pow; let width_type : word_width = size_bytes(load_width_bytes); - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); let rs2_val : int = unsigned(get_scalar(rs2, xlen)); - let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); + let mask : bits('n) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { /* active segments */ + if mask[i] == bitone then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; @@ -430,6 +438,8 @@ function clause execute(VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_store(nf_int, EEW, EMUL_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vssseg(nf_int, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) @@ -444,11 +454,11 @@ union clause ast = VLUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vd @ 0b0000111 if extensionEnabled(Ext_V) -val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired +val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow; let width_type : word_width = size_bytes(EEW_data_bytes); - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd); let vs2_val : vector('n, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); @@ -456,7 +466,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { /* active segments */ + if mask[i] == bitone then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset : int = unsigned(vs2_val[i]) + j * EEW_data_bytes; @@ -498,6 +508,8 @@ function clause execute(VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_indexed_load(vd, vm, nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlxseg(nf_int, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) @@ -522,6 +534,8 @@ function clause execute(VLOXSEGTYPE(nf, vm, vs2, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_indexed_load(vd, vm, nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vlxseg(nf_int, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) @@ -536,18 +550,18 @@ union clause ast = VSUXSEGTYPE : (bits(3), bits(1), regidx, regidx, vlewidth, re mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if extensionEnabled(Ext_V) <-> nf @ 0b0 @ 0b01 @ vm @ vs2 @ rs1 @ encdec_vlewidth(width) @ vs3 @ 0b0100111 if extensionEnabled(Ext_V) -val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired +val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n > 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else 2 ^ EMUL_data_pow; let width_type : word_width = size_bytes(EEW_data_bytes); - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); let vs2_val : vector('n, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); - let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_data_pow, vm_val); + let mask : bits('n) = init_masked_source(num_elem, EMUL_data_pow, vm_val); /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { /* active segments */ + if mask[i] == bitone then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset : int = unsigned(vs2_val[i]) + j * EEW_data_bytes; @@ -593,6 +607,8 @@ function clause execute(VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); /* number of data and indices are the same */ let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_indexed_store(nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vsxseg(nf_int, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) @@ -617,6 +633,8 @@ function clause execute(VSOXSEGTYPE(nf, vm, vs2, rs1, width, vs3)) = { let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); /* number of data and indices are the same */ let nf_int = nfields_int(nf); + assert(num_elem > 0); + if illegal_indexed_store(nf_int, EEW_index_bytes * 8, EMUL_index_pow, EMUL_data_pow) then { handle_illegal(); return RETIRE_FAIL }; process_vsxseg(nf_int, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 67e34d2c5..cb7d29537 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -39,14 +39,14 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('o)) = read_vreg(num_elem_vd, SEW_widen, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); var sum : bits('o) = read_single_element(SEW_widen, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { - if mask[i] then { + if mask[i] == bitone then { let elem : bits('o) = match funct6 { IVV_VWREDSUMU => to_bits(SEW_widen, unsigned(vs2_val[i])), IVV_VWREDSUM => to_bits(SEW_widen, signed(vs2_val[i])) @@ -101,14 +101,14 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'd = num_elem_vd; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem_vs, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem_vs, vm, 0b00000); let vd_val : vector('d, bits('m)) = read_vreg(num_elem_vd, SEW, 0, vd); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem_vs, SEW, LMUL_pow, vs2); - let mask : vector('n, bool) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); + let mask : bits('n) = init_masked_source(num_elem_vs, LMUL_pow, vm_val); var sum : bits('m) = read_single_element(SEW, 0, vs1); /* vs1 regardless of LMUL setting */ foreach (i from 0 to (num_elem_vs - 1)) { - if mask[i] then { + if mask[i] == bitone then { sum = match funct6 { MVV_VREDSUM => sum + vs2_val[i], MVV_VREDAND => sum & vs2_val[i], diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index d5833f162..6ada9e373 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -199,13 +199,13 @@ 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 & 'm >= 0. (int('n), int('m), int('p), vector('n, bits('m)), vector('n, bool)) -> (vector('n, bits('m)), vector('n, bool)) +val init_masked_result : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), vector('n, bits('m)), bits('n)) -> (vector('n, bits('m)), bits('n)) 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(); let tail_ag : agtype = get_vtype_vta(); let mask_ag : agtype = get_vtype_vma(); - var mask : vector('n, bool) = undefined; + var mask : bits('n) = undefined; var result : vector('n, bits('m)) = undefined; /* Determine the actual number of elements when lmul < 1 */ @@ -216,31 +216,31 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { if i < start_element then { /* Prestart elements defined by vstart */ result[i] = vd_val[i]; - mask[i] = false + mask[i] = bitzero } else if i > end_element then { /* Tail elements defined by vl */ result[i] = match tail_ag { UNDISTURBED => vd_val[i], AGNOSTIC => vd_val[i] /* TODO: configuration support */ }; - mask[i] = false + mask[i] = bitzero } else if i >= real_num_elem then { /* Tail elements defined by lmul < 1 */ result[i] = match tail_ag { UNDISTURBED => vd_val[i], AGNOSTIC => vd_val[i] /* TODO: configuration support */ }; - mask[i] = false - } else if not(vm_val[i]) then { + mask[i] = bitzero + } else if vm_val[i] == bitzero then { /* Inactive body elements defined by vm */ result[i] = match mask_ag { UNDISTURBED => vd_val[i], AGNOSTIC => vd_val[i] /* TODO: configuration support */ }; - mask[i] = false + mask[i] = bitzero } else { /* Active body elements */ - mask[i] = true; + mask[i] = bitone; } }; @@ -252,11 +252,11 @@ function init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { * (vs3 for store and vs2 for reduction). There's no destination register to be masked. * In these cases, this function can be called to simply get the mask vector for vs (without the prepared vd result vector). */ -val init_masked_source : forall 'n 'p, 'n >= 0. (int('n), int('p), vector('n, bool)) -> vector('n, bool) +val init_masked_source : forall 'n 'p, 'n > 0. (int('n), int('p), bits('n)) -> bits('n) function init_masked_source(num_elem, LMUL_pow, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); - var mask : vector('n, bool) = undefined; + var mask : bits('n) = undefined; /* Determine the actual number of elements when lmul < 1 */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow)); @@ -265,19 +265,19 @@ function init_masked_source(num_elem, LMUL_pow, vm_val) = { foreach (i from 0 to (num_elem - 1)) { if i < start_element then { /* Prestart elements defined by vstart */ - mask[i] = false + mask[i] = bitzero } else if i > end_element then { /* Tail elements defined by vl */ - mask[i] = false + mask[i] = bitzero } else if i >= real_num_elem then { /* Tail elements defined by lmul < 1 */ - mask[i] = false - } else if not(vm_val[i]) then { + mask[i] = bitzero + } else if vm_val[i] == bitzero then { /* Inactive body elements defined by vm */ - mask[i] = false + mask[i] = bitzero } else { /* Active body elements */ - mask[i] = true; + mask[i] = bitone; } }; @@ -286,12 +286,12 @@ function init_masked_source(num_elem, LMUL_pow, vm_val) = { /* Mask handling for carry functions that use masks as input/output */ /* Only prestart and tail elements are masked in a mask value */ -val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, bool)) -> (vector('n, bool), vector('n, bool)) +val init_masked_result_carry : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), bits('n)) -> (bits('n), bits('n)) function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { let start_element = get_start_element(); let end_element = get_end_element(); - var mask : vector('n, bool) = undefined; - var result : vector('n, bool) = undefined; + var mask : bits('n) = undefined; + var result : bits('n) = undefined; /* Determine the actual number of elements when lmul < 1 */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow)); @@ -301,20 +301,20 @@ function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { if i < start_element then { /* Prestart elements defined by vstart */ result[i] = vd_val[i]; - mask[i] = false + mask[i] = bitzero } else if i > end_element then { /* Tail elements defined by vl */ /* Mask tail is always agnostic */ result[i] = vd_val[i]; /* TODO: configuration support */ - mask[i] = false + mask[i] = bitzero } else if i >= real_num_elem then { /* Tail elements defined by lmul < 1 */ /* Mask tail is always agnostic */ result[i] = vd_val[i]; /* TODO: configuration support */ - mask[i] = false + mask[i] = bitzero } else { /* Active body elements */ - mask[i] = true + mask[i] = bitone } }; @@ -322,13 +322,13 @@ function init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) = { } /* Mask handling for cmp functions that use masks as output */ -val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), vector('n, bool), vector('n, bool)) -> (vector('n, bool), vector('n, bool)) +val init_masked_result_cmp : forall 'n 'm 'p, 'n >= 0. (int('n), int('m), int('p), bits('n), bits('n)) -> (bits('n), bits('n)) function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { let start_element = get_start_element(); let end_element = get_end_element(); let mask_ag : agtype = get_vtype_vma(); - var mask : vector('n, bool) = undefined; - var result : vector('n, bool) = undefined; + var mask : bits('n) = undefined; + var result : bits('n) = undefined; /* Determine the actual number of elements when lmul < 1 */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (2 ^ (0 - LMUL_pow)); @@ -338,27 +338,27 @@ function init_masked_result_cmp(num_elem, SEW, LMUL_pow, vd_val, vm_val) = { if i < start_element then { /* Prestart elements defined by vstart */ result[i] = vd_val[i]; - mask[i] = false + mask[i] = bitzero } else if i > end_element then { /* Tail elements defined by vl */ /* Mask tail is always agnostic */ result[i] = vd_val[i]; /* TODO: configuration support */ - mask[i] = false + mask[i] = bitzero } else if i >= real_num_elem then { /* Tail elements defined by lmul < 1 */ /* Mask tail is always agnostic */ result[i] = vd_val[i]; /* TODO: configuration support */ - mask[i] = false - } else if not(vm_val[i]) then { + mask[i] = bitzero + } else if vm_val[i] == bitzero then { /* Inactive body elements defined by vm */ result[i] = match mask_ag { UNDISTURBED => vd_val[i], AGNOSTIC => vd_val[i] /* TODO: configuration support */ }; - mask[i] = false + mask[i] = bitzero } else { /* Active body elements */ - mask[i] = true + mask[i] = bitone } }; diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index e6f50cf89..5e5d313f4 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -35,21 +35,21 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : bits('n) = read_vmask_carry(num_elem, 0b0, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { - VVM_VMADC => unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1, - VVM_VMSBC => unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_to_bits(vm_val[i])) < 0 + VVM_VMADC => unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + (if vm_val[i] == bitone then 1 else 0) > 2 ^ SEW - 1, + VVM_VMSBC => unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - (if vm_val[i] == bitone then 1 else 0) < 0 }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -92,18 +92,18 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = { let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { VVMC_VMADC => unsigned(vs2_val[i]) + unsigned(vs1_val[i]) > 2 ^ SEW - 1, VVMC_VMSBC => unsigned(vs2_val[i]) - unsigned(vs1_val[i]) < 0 }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -145,12 +145,9 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - var vec_trues : vector('n, bool) = undefined; - foreach (i from 0 to (num_elem - 1)) { - vec_trues[i] = true - }; + let vec_trues : bits('n) = ones(); - let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : bits('n) = read_vmask_carry(num_elem, 0b0, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -159,10 +156,10 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { - VVMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_to_bits(vm_val[i]))), - VVMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_to_bits(vm_val[i]))) + VVMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + (if vm_val[i] == bitone then 1 else 0)), + VVMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - (if vm_val[i] == bitone then 1 else 0)) } } }; @@ -206,16 +203,16 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { VVCMP_VMSEQ => vs2_val[i] == vs1_val[i], VVCMP_VMSNE => vs2_val[i] != vs1_val[i], @@ -224,7 +221,7 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = { VVCMP_VMSLEU => unsigned(vs2_val[i]) <= unsigned(vs1_val[i]), VVCMP_VMSLE => signed(vs2_val[i]) <= signed(vs1_val[i]) }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -269,21 +266,21 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : bits('n) = read_vmask_carry(num_elem, 0b0, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { - VXM_VMADC => unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1, - VXM_VMSBC => unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_to_bits(vm_val[i])) < 0 + VXM_VMADC => unsigned(vs2_val[i]) + unsigned(rs1_val) + (if vm_val[i] == bitone then 1 else 0) > 2 ^ SEW - 1, + VXM_VMSBC => unsigned(vs2_val[i]) - unsigned(rs1_val) - (if vm_val[i] == bitone then 1 else 0) < 0 }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -326,18 +323,18 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { VXMC_VMADC => unsigned(vs2_val[i]) + unsigned(rs1_val) > 2 ^ SEW - 1, VXMC_VMSBC => unsigned(vs2_val[i]) - unsigned(rs1_val) < 0 }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -379,12 +376,9 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - var vec_trues : vector('n, bool) = undefined; - foreach (i from 0 to (num_elem - 1)) { - vec_trues[i] = true - }; + let vec_trues : bits('n) = ones(); - let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : bits('n) = read_vmask_carry(num_elem, 0b0, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -393,10 +387,10 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { - VXMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_to_bits(vm_val[i]))), - VXMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_to_bits(vm_val[i]))) + VXMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(rs1_val) + (if vm_val[i] == bitone then 1 else 0)), + VXMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(rs1_val) - (if vm_val[i] == bitone then 1 else 0)) } } }; @@ -442,16 +436,16 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { VXCMP_VMSEQ => vs2_val[i] == rs1_val, VXCMP_VMSNE => vs2_val[i] != rs1_val, @@ -462,7 +456,7 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { VXCMP_VMSGTU => unsigned(vs2_val[i]) > unsigned(rs1_val), VXCMP_VMSGT => signed(vs2_val[i]) > signed(rs1_val) }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -508,20 +502,20 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : bits('n) = read_vmask_carry(num_elem, 0b0, 0b00000); let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { - VIM_VMADC => unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1 + VIM_VMADC => unsigned(vs2_val[i]) + unsigned(imm_val) + (if vm_val[i] == bitone then 1 else 0) > 2 ^ SEW - 1 }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -562,17 +556,17 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { VIMC_VMADC => unsigned(vs2_val[i]) + unsigned(imm_val) > 2 ^ SEW - 1 }; - result[i] = res + result[i] = bool_to_bit(res) } }; @@ -612,12 +606,9 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let 'm = SEW; /* for bypassing normal masking in init_masked_result */ - var vec_trues : vector('n, bool) = undefined; - foreach (i from 0 to (num_elem - 1)) { - vec_trues[i] = true - }; + let vec_trues : bits('n) = ones(); - let vm_val : vector('n, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); + let vm_val : bits('n) = read_vmask_carry(num_elem, 0b0, 0b00000); let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -626,9 +617,9 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { var result = initial_result; foreach (i from 0 to (num_elem - 1)) { - if mask[i] then { + if mask[i] == bitone then { result[i] = match funct6 { - VIMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_to_bits(vm_val[i]))) + VIMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(imm_val) + (if vm_val[i] == bitone then 1 else 0)) } } }; @@ -671,16 +662,16 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); + let vm_val : bits('n) = read_vmask(num_elem, vm, 0b00000); let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); - let vd_val : vector('n, bool) = read_vmask(num_elem, 0b0, vd); + let vd_val : bits('n) = read_vmask(num_elem, 0b0, vd); 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 { + if mask[i] == bitone then { let res : bool = match funct6 { VICMP_VMSEQ => vs2_val[i] == imm_val, VICMP_VMSNE => vs2_val[i] != imm_val, @@ -689,7 +680,7 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { VICMP_VMSGTU => unsigned(vs2_val[i]) > unsigned(imm_val), VICMP_VMSGT => signed(vs2_val[i]) > signed(imm_val) }; - result[i] = res + result[i] = bool_to_bit(res) } }; diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 2c913de83..f43014eca 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -222,7 +222,7 @@ function ext_write_vcsr (vxrm_val, vxsat_val) = { } /* num_elem means max(VLMAX,VLEN/SEW)) according to Section 5.4 of RVV spec */ -val get_num_elem : (int, int) -> nat +val get_num_elem : (int, int) -> {'n, 'n > 0. int('n)} function get_num_elem(LMUL_pow, SEW) = { let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow; /* Ignore lmul < 1 so that the entire vreg is read, allowing all masking to @@ -355,43 +355,43 @@ 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, bool) +val read_vmask : forall 'n, 'n > 0. (int('n), bits(1), regidx) -> bits('n) function read_vmask(num_elem, vm, vrid) = { assert(num_elem <= sizeof(vlenmax)); let vreg_val : vregtype = V(vrid); - var result : vector('n, bool) = vector_init(true); + var result : bits('n) = ones(); if vm == 0b1 then { return result }; foreach (i from 0 to (num_elem - 1)) { - result[i] = bit_to_bool(vreg_val[i]) + result[i] = vreg_val[i] }; result } /* 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, bool) +val read_vmask_carry : forall 'n, 'n > 0. (int('n), bits(1), regidx) -> bits('n) function read_vmask_carry(num_elem, vm, vrid) = { assert(num_elem <= sizeof(vlenmax)); let vreg_val : vregtype = V(vrid); - var result : vector('n, bool) = vector_init(false); + var result : bits('n) = zeros(); if vm == 0b1 then { return result }; foreach (i from 0 to (num_elem - 1)) { - result[i] = bit_to_bool(vreg_val[i]) + result[i] = vreg_val[i] }; result } /* Mask register writing operation with num_elem as max(VLMAX,VLEN/SEW)) */ -val write_vmask : forall 'n, 'n >= 0. (int('n), regidx, vector('n, bool)) -> unit +val write_vmask : forall 'n, 'n > 0. (int('n), regidx, bits('n)) -> unit function write_vmask(num_elem, vrid, v) = { assert(0 < VLEN & VLEN <= sizeof(vlenmax)); assert(0 < num_elem & num_elem <= VLEN); @@ -399,7 +399,7 @@ function write_vmask(num_elem, vrid, v) = { var result : vregtype = undefined; foreach (i from 0 to (num_elem - 1)) { - result[i] = bool_to_bit(v[i]) + result[i] = v[i] }; foreach (i from num_elem to (VLEN - 1)) { /* Mask tail is always agnostic */