diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 148c72bd4..2cc5cb3ac 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -9,6 +9,7 @@ bool rv_enable_rvc = true; bool rv_enable_next = false; bool rv_enable_writable_misa = true; bool rv_enable_fdext = true; +bool rv_enable_rvv = true; bool rv_enable_dirty_update = false; bool rv_enable_misaligned = false; diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 0035e96c8..f5e73b25a 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -102,17 +102,17 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { VV_VAND => vs2_val[i] & vs1_val[i], VV_VOR => vs2_val[i] | vs1_val[i], VV_VXOR => vs2_val[i] ^ vs1_val[i], - VV_VSADDU => unsigned_saturation('m, EXTZ('m + 1, vs2_val[i]) + EXTZ('m + 1, vs1_val[i])), - VV_VSADD => signed_saturation('m, EXTS('m + 1, vs2_val[i]) + EXTS('m + 1, vs1_val[i])), + VV_VSADDU => unsigned_saturation('m, zero_extend('m + 1, vs2_val[i]) + zero_extend('m + 1, vs1_val[i])), + VV_VSADD => signed_saturation('m, sign_extend('m + 1, vs2_val[i]) + sign_extend('m + 1, vs1_val[i])), VV_VSSUBU => { if unsigned(vs2_val[i]) < unsigned(vs1_val[i]) then zeros() - else unsigned_saturation('m, EXTZ('m + 1, vs2_val[i]) - EXTZ('m + 1, vs1_val[i])) + else unsigned_saturation('m, zero_extend('m + 1, vs2_val[i]) - zero_extend('m + 1, vs1_val[i])) }, - VV_VSSUB => signed_saturation('m, EXTS('m + 1, vs2_val[i]) - EXTS('m + 1, vs1_val[i])), + VV_VSSUB => signed_saturation('m, sign_extend('m + 1, vs2_val[i]) - sign_extend('m + 1, vs1_val[i])), VV_VSMUL => { let result_mul = to_bits('m * 2, signed(vs2_val[i]) * signed(vs1_val[i])); let rounding_incr = get_fixed_rounding_incr(result_mul, 'm - 1); - let result_wide = (result_mul >> ('m - 1)) + EXTZ('m * 2, rounding_incr); + let result_wide = (result_mul >> ('m - 1)) + zero_extend('m * 2, rounding_incr); signed_saturation('m, result_wide['m..0]) }, VV_VSLL => { @@ -125,19 +125,19 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { }, VV_VSRA => { let shift_amount = get_shift_amount(vs1_val[i], SEW); - let v_double : bits('m * 2) = EXTS(vs2_val[i]); + let v_double : bits('m * 2) = sign_extend(vs2_val[i]); slice(v_double >> shift_amount, 0, SEW) }, VV_VSSRL => { let shift_amount = get_shift_amount(vs1_val[i], SEW); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); - (vs2_val[i] >> shift_amount) + EXTZ('m, rounding_incr) + (vs2_val[i] >> shift_amount) + zero_extend('m, rounding_incr) }, VV_VSSRA => { let shift_amount = get_shift_amount(vs1_val[i], SEW); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); - let v_double : bits('m * 2) = EXTS(vs2_val[i]); - slice(v_double >> shift_amount, 0, SEW) + EXTZ('m, rounding_incr) + let v_double : bits('m * 2) = sign_extend(vs2_val[i]); + slice(v_double >> shift_amount, 0, SEW) + zero_extend('m, rounding_incr) }, VV_VMINU => to_bits(SEW, min(unsigned(vs2_val[i]), unsigned(vs1_val[i]))), VV_VMIN => to_bits(SEW, min(signed(vs2_val[i]), signed(vs1_val[i]))), @@ -241,7 +241,7 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { }, NVS_VNSRA => { let shift_amount = get_shift_amount(vs1_val[i], SEW_widen); - let v_double : bits('o * 2) = EXTS(vs2_val[i]); + let v_double : bits('o * 2) = sign_extend(vs2_val[i]); let arith_shifted : bits('o) = slice(v_double >> shift_amount, 0, SEW_widen); slice(arith_shifted, 0, SEW) } @@ -305,12 +305,12 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); result[i] = match funct6 { NV_VNCLIPU => { - let result_wide = (vs2_val[i] >> shift_amount) + EXTZ('o, rounding_incr); + let result_wide = (vs2_val[i] >> shift_amount) + zero_extend('o, rounding_incr); unsigned_saturation('m, result_wide); }, NV_VNCLIP => { - let v_double : bits('m * 4) = EXTS(vs2_val[i]); - let result_wide = slice(v_double >> shift_amount, 0, 'o) + EXTZ('o, rounding_incr); + let v_double : bits('m * 4) = sign_extend(vs2_val[i]); + let result_wide = slice(v_double >> shift_amount, 0, 'o) + zero_extend('o, rounding_incr); signed_saturation('m, result_wide); } } @@ -471,17 +471,17 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { VX_VAND => vs2_val[i] & rs1_val, VX_VOR => vs2_val[i] | rs1_val, VX_VXOR => vs2_val[i] ^ rs1_val, - VX_VSADDU => unsigned_saturation('m, EXTZ('m + 1, vs2_val[i]) + EXTZ('m + 1, rs1_val) ), - VX_VSADD => signed_saturation('m, EXTS('m + 1, vs2_val[i]) + EXTS('m + 1, rs1_val) ), + VX_VSADDU => unsigned_saturation('m, zero_extend('m + 1, vs2_val[i]) + zero_extend('m + 1, rs1_val) ), + VX_VSADD => signed_saturation('m, sign_extend('m + 1, vs2_val[i]) + sign_extend('m + 1, rs1_val) ), VX_VSSUBU => { if unsigned(vs2_val[i]) < unsigned(rs1_val) then zeros() - else unsigned_saturation('m, EXTZ('m + 1, vs2_val[i]) - EXTZ('m + 1, rs1_val) ) + else unsigned_saturation('m, zero_extend('m + 1, vs2_val[i]) - zero_extend('m + 1, rs1_val) ) }, - VX_VSSUB => signed_saturation('m, EXTS('m + 1, vs2_val[i]) - EXTS('m + 1, rs1_val) ), + VX_VSSUB => signed_saturation('m, sign_extend('m + 1, vs2_val[i]) - sign_extend('m + 1, rs1_val) ), VX_VSMUL => { let result_mul = to_bits('m * 2, signed(vs2_val[i]) * signed(rs1_val)); let rounding_incr = get_fixed_rounding_incr(result_mul, 'm - 1); - let result_wide = (result_mul >> ('m - 1)) + EXTZ('m * 2, rounding_incr); + let result_wide = (result_mul >> ('m - 1)) + zero_extend('m * 2, rounding_incr); signed_saturation('m, result_wide['m..0]) }, VX_VSLL => { @@ -494,19 +494,19 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { }, VX_VSRA => { let shift_amount = get_shift_amount(rs1_val, SEW); - let v_double : bits('m * 2) = EXTS(vs2_val[i]); + let v_double : bits('m * 2) = sign_extend(vs2_val[i]); slice(v_double >> shift_amount, 0, SEW) }, VX_VSSRL => { let shift_amount = get_shift_amount(rs1_val, SEW); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); - (vs2_val[i] >> shift_amount) + EXTZ('m, rounding_incr) + (vs2_val[i] >> shift_amount) + zero_extend('m, rounding_incr) }, VX_VSSRA => { let shift_amount = get_shift_amount(rs1_val, SEW); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); - let v_double : bits('m * 2) = EXTS(vs2_val[i]); - slice(v_double >> shift_amount, 0, SEW) + EXTZ('m, rounding_incr) + let v_double : bits('m * 2) = sign_extend(vs2_val[i]); + slice(v_double >> shift_amount, 0, SEW) + zero_extend('m, rounding_incr) }, VX_VMINU => to_bits(SEW, min(unsigned(vs2_val[i]), unsigned(rs1_val))), VX_VMIN => to_bits(SEW, min(signed(vs2_val[i]), signed(rs1_val))), @@ -593,7 +593,7 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { }, NXS_VNSRA => { let shift_amount = get_shift_amount(rs1_val, SEW_widen); - let v_double : bits('o * 2) = EXTS(vs2_val[i]); + let v_double : bits('o * 2) = sign_extend(vs2_val[i]); let arith_shifted : bits('o) = slice(v_double >> shift_amount, 0, SEW_widen); slice(arith_shifted, 0, SEW) } @@ -657,12 +657,12 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); result[i] = match funct6 { NX_VNCLIPU => { - let result_wide = (vs2_val[i] >> shift_amount) + EXTZ('o, rounding_incr); + let result_wide = (vs2_val[i] >> shift_amount) + zero_extend('o, rounding_incr); unsigned_saturation('m, result_wide) }, NX_VNCLIP => { - let v_double : bits('m * 4) = EXTS(vs2_val[i]); - let result_wide = slice(v_double >> shift_amount, 0, 'o) + EXTZ('o, rounding_incr); + let v_double : bits('m * 4) = sign_extend(vs2_val[i]); + let result_wide = slice(v_double >> shift_amount, 0, 'o) + zero_extend('o, rounding_incr); signed_saturation('m, result_wide) } } @@ -868,7 +868,7 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -884,31 +884,31 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { VI_VAND => vs2_val[i] & imm_val, VI_VOR => vs2_val[i] | imm_val, VI_VXOR => vs2_val[i] ^ imm_val, - VI_VSADDU => unsigned_saturation('m, EXTZ('m + 1, vs2_val[i]) + EXTZ('m + 1, imm_val) ), - VI_VSADD => signed_saturation('m, EXTS('m + 1, vs2_val[i]) + EXTS('m + 1, imm_val) ), + VI_VSADDU => unsigned_saturation('m, zero_extend('m + 1, vs2_val[i]) + zero_extend('m + 1, imm_val) ), + VI_VSADD => signed_saturation('m, sign_extend('m + 1, vs2_val[i]) + sign_extend('m + 1, imm_val) ), VI_VSLL => { - let shift_amount = get_shift_amount(sail_zero_extend(simm, SEW), SEW); + let shift_amount = get_shift_amount(zero_extend('m, simm), SEW); vs2_val[i] << shift_amount }, VI_VSRL => { - let shift_amount = get_shift_amount(sail_zero_extend(simm, SEW), SEW); + let shift_amount = get_shift_amount(zero_extend('m, simm), SEW); vs2_val[i] >> shift_amount }, VI_VSRA => { - let shift_amount = get_shift_amount(sail_zero_extend(simm, SEW), SEW); - let v_double : bits('m * 2) = EXTS(vs2_val[i]); + let shift_amount = get_shift_amount(zero_extend('m, simm), SEW); + let v_double : bits('m * 2) = sign_extend(vs2_val[i]); slice(v_double >> shift_amount, 0, SEW) }, VI_VSSRL => { - let shift_amount = get_shift_amount(sail_zero_extend(simm, SEW), SEW); + let shift_amount = get_shift_amount(zero_extend('m, simm), SEW); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); - (vs2_val[i] >> shift_amount) + EXTZ('m, rounding_incr) + (vs2_val[i] >> shift_amount) + zero_extend('m, rounding_incr) }, VI_VSSRA => { - let shift_amount = get_shift_amount(sail_zero_extend(simm, SEW), SEW); + let shift_amount = get_shift_amount(zero_extend('m, simm), SEW); let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); - let v_double : bits('m * 2) = EXTS(vs2_val[i]); - slice(v_double >> shift_amount, 0, SEW) + EXTZ('m, rounding_incr) + let v_double : bits('m * 2) = sign_extend(vs2_val[i]); + slice(v_double >> shift_amount, 0, SEW) + zero_extend('m, rounding_incr) } } } @@ -966,7 +966,7 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); result : vector('n, dec, bits('m)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -983,7 +983,7 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { }, NIS_VNSRA => { let shift_amount = get_shift_amount(imm_val, SEW_widen); - let v_double : bits('o * 2) = EXTS(vs2_val[i]); + let v_double : bits('o * 2) = sign_extend(vs2_val[i]); let arith_shifted : bits('o) = slice(v_double >> shift_amount, 0, SEW_widen); slice(arith_shifted, 0, SEW) } @@ -1033,7 +1033,7 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); result : vector('n, dec, bits('m)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -1047,12 +1047,12 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let rounding_incr = get_fixed_rounding_incr(vs2_val[i], shift_amount); result[i] = match funct6 { NI_VNCLIPU => { - let result_wide = (vs2_val[i] >> shift_amount) + EXTZ('o, rounding_incr); + let result_wide = (vs2_val[i] >> shift_amount) + zero_extend('o, rounding_incr); unsigned_saturation('m, result_wide) }, NI_VNCLIP => { - let v_double : bits('m * 4) = EXTS(vs2_val[i]); - let result_wide = slice(v_double >> shift_amount, 0, 'o) + EXTZ('o, rounding_incr); + let v_double : bits('m * 4) = sign_extend(vs2_val[i]); + let result_wide = slice(v_double >> shift_amount, 0, 'o) + zero_extend('o, rounding_incr); signed_saturation('m, result_wide) } } @@ -1098,7 +1098,7 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let imm_val : nat = unsigned(EXTZ(sizeof(xlen), simm)); + let imm_val : nat = unsigned(zero_extend(sizeof(xlen), simm)); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -1162,7 +1162,7 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = { let 'm = SEW; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -1207,7 +1207,7 @@ function clause execute(MOVETYPEI(vd, simm)) = { let 'm = SEW; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -1235,7 +1235,7 @@ mapping clause encdec = VMVRTYPE(vs2, simm, vd) if haveRVV() function clause execute(VMVRTYPE(vs2, simm, vd)) = { let start_element = get_start_element(); let SEW = get_sew(); - let imm_val = unsigned(EXTZ(sizeof(xlen), simm)); + let imm_val = unsigned(zero_extend(sizeof(xlen), simm)); let EMUL = imm_val + 1; if not(EMUL == 1 | EMUL == 2 | EMUL == 4 | EMUL == 8) then { handle_illegal(); return RETIRE_FAIL }; @@ -1313,24 +1313,24 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { if mask[i] then { result[i] = match funct6 { MVV_VAADDU => { - let result_add = EXTZ('m + 1, vs2_val[i]) + EXTZ('m + 1, vs1_val[i]); + let result_add = zero_extend('m + 1, vs2_val[i]) + zero_extend('m + 1, vs1_val[i]); let rounding_incr = get_fixed_rounding_incr(result_add, 1); - slice(result_add >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_add >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVV_VAADD => { - let result_add = EXTS('m + 1, vs2_val[i]) + EXTS('m + 1, vs1_val[i]); + let result_add = sign_extend('m + 1, vs2_val[i]) + sign_extend('m + 1, vs1_val[i]); let rounding_incr = get_fixed_rounding_incr(result_add, 1); - slice(result_add >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_add >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVV_VASUBU => { - let result_sub = EXTZ('m + 1, vs2_val[i]) - EXTZ('m + 1, vs1_val[i]); + let result_sub = zero_extend('m + 1, vs2_val[i]) - zero_extend('m + 1, vs1_val[i]); let rounding_incr = get_fixed_rounding_incr(result_sub, 1); - slice(result_sub >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_sub >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVV_VASUB => { - let result_sub = EXTS('m + 1, vs2_val[i]) - EXTS('m + 1, vs1_val[i]); + let result_sub = sign_extend('m + 1, vs2_val[i]) - sign_extend('m + 1, vs1_val[i]); let rounding_incr = get_fixed_rounding_incr(result_sub, 1); - slice(result_sub >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_sub >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVV_VMUL => get_slice_int(SEW, signed(vs2_val[i]) * signed(vs1_val[i]), 0), MVV_VMULH => get_slice_int(SEW, signed(vs2_val[i]) * signed(vs1_val[i]), SEW), @@ -1680,8 +1680,8 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { result[i] = match funct6 { - VEXT2_ZVF2 => EXTZ(vs2_val[i]), - VEXT2_SVF2 => EXTS(vs2_val[i]) + VEXT2_ZVF2 => zero_extend(vs2_val[i]), + VEXT2_SVF2 => sign_extend(vs2_val[i]) } } }; @@ -1738,8 +1738,8 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { result[i] = match funct6 { - VEXT4_ZVF4 => EXTZ(vs2_val[i]), - VEXT4_SVF4 => EXTS(vs2_val[i]) + VEXT4_ZVF4 => zero_extend(vs2_val[i]), + VEXT4_SVF4 => sign_extend(vs2_val[i]) } } }; @@ -1796,8 +1796,8 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { foreach (i from 0 to (num_elem - 1)) { if mask[i] then { result[i] = match funct6 { - VEXT8_ZVF8 => EXTZ(vs2_val[i]), - VEXT8_SVF8 => EXTS(vs2_val[i]) + VEXT8_ZVF8 => zero_extend(vs2_val[i]), + VEXT8_SVF8 => sign_extend(vs2_val[i]) } } }; @@ -1833,7 +1833,7 @@ function clause execute(VMVXS(vs2, rd)) = { let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vs2); X(rd) = if sizeof(xlen) < SEW then slice(vs2_val[0], 0, sizeof(xlen)) - else if sizeof(xlen) > SEW then EXTS(vs2_val[0]) + else if sizeof(xlen) > SEW then sign_extend(vs2_val[0]) else vs2_val[0]; vstart = zeros(); @@ -1946,24 +1946,24 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { if mask[i] then { result[i] = match funct6 { MVX_VAADDU => { - let result_add = EXTZ('m + 1, vs2_val[i]) + EXTZ('m + 1, rs1_val); + let result_add = zero_extend('m + 1, vs2_val[i]) + zero_extend('m + 1, rs1_val); let rounding_incr = get_fixed_rounding_incr(result_add, 1); - slice(result_add >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_add >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVX_VAADD => { - let result_add = EXTS('m + 1, vs2_val[i]) + EXTS('m + 1, rs1_val); + let result_add = sign_extend('m + 1, vs2_val[i]) + sign_extend('m + 1, rs1_val); let rounding_incr = get_fixed_rounding_incr(result_add, 1); - slice(result_add >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_add >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVX_VASUBU => { - let result_sub = EXTZ('m + 1, vs2_val[i]) - EXTZ('m + 1, rs1_val); + let result_sub = zero_extend('m + 1, vs2_val[i]) - zero_extend('m + 1, rs1_val); let rounding_incr = get_fixed_rounding_incr(result_sub, 1); - slice(result_sub >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_sub >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVX_VASUB => { - let result_sub = EXTS('m + 1, vs2_val[i]) - EXTS('m + 1, rs1_val); + let result_sub = sign_extend('m + 1, vs2_val[i]) - sign_extend('m + 1, rs1_val); let rounding_incr = get_fixed_rounding_incr(result_sub, 1); - slice(result_sub >> 1, 0, 'm) + EXTZ('m, rounding_incr) + slice(result_sub >> 1, 0, 'm) + zero_extend('m, rounding_incr) }, MVX_VSLIDE1UP => { if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index e103437ea..7b1251c00 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -436,7 +436,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { }, FV_CVT_F_XU => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_ui32ToF16(rm_3b, EXTZ(vs2_val[i])), + 16 => riscv_ui32ToF16(rm_3b, zero_extend(vs2_val[i])), 32 => riscv_ui32ToF32(rm_3b, vs2_val[i]), 64 => riscv_ui64ToF64(rm_3b, vs2_val[i]) }; @@ -445,7 +445,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { }, FV_CVT_F_X => { let (fflags, elem) : (bits_fflags, bits('m)) = match 'm { - 16 => riscv_i32ToF16(rm_3b, EXTS(vs2_val[i])), + 16 => riscv_i32ToF16(rm_3b, sign_extend(vs2_val[i])), 32 => riscv_i32ToF32(rm_3b, vs2_val[i]), 64 => riscv_i64ToF64(rm_3b, vs2_val[i]) }; @@ -555,8 +555,8 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { }, FWV_CVT_F_XU => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { - 8 => riscv_ui32ToF16(rm_3b, EXTZ(vs2_val[i])), - 16 => riscv_ui32ToF32(rm_3b, EXTZ(vs2_val[i])), + 8 => riscv_ui32ToF16(rm_3b, zero_extend(vs2_val[i])), + 16 => riscv_ui32ToF32(rm_3b, zero_extend(vs2_val[i])), 32 => riscv_ui32ToF64(rm_3b, vs2_val[i]) }; write_fflags(fflags); @@ -564,8 +564,8 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { }, FWV_CVT_F_X => { let (fflags, elem) : (bits_fflags, bits('o)) = match 'm { - 8 => riscv_i32ToF16(rm_3b, EXTS(vs2_val[i])), - 16 => riscv_i32ToF32(rm_3b, EXTS(vs2_val[i])), + 8 => riscv_i32ToF16(rm_3b, sign_extend(vs2_val[i])), + 16 => riscv_i32ToF32(rm_3b, sign_extend(vs2_val[i])), 32 => riscv_i32ToF64(rm_3b, vs2_val[i]) }; write_fflags(fflags); diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index cb3e272e1..d832c6cc0 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -249,7 +249,7 @@ function get_scalar(rs1, SEW) = { X(rs1)[SEW - 1 .. 0] } else { /* Sign extend to SEW */ - EXTS(SEW, X(rs1)) + sign_extend(SEW, X(rs1)) } } @@ -462,7 +462,7 @@ function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = { foreach (i from 0 to (num_elem - 1)) { result[i] = zeros('q * 'm); foreach (j from 0 to (nf - 1)) { - result[i] = result[i] | (EXTZ(vreg_list[j][i]) << (j * 'm)) + result[i] = result[i] | (zero_extend(vreg_list[j][i]) << (j * 'm)) } }; result @@ -878,7 +878,7 @@ function fp_class(xf) = { else if f_is_QNaN (xf) then 0b_10_0000_0000 else zeros(); - EXTZ(result_val_10b) + zero_extend(result_val_10b) } val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2) effect {escape, rreg, undef, wreg} @@ -951,9 +951,9 @@ function count_leadingzeros (sig, len) = { val rsqrt7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bool) -> bits_D function rsqrt7 (v, sub) = { let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm { - 16 => (EXTZ(64, v[9 .. 0]), EXTZ(64, v[14 .. 10]), [v[15]], 5, 10), - 32 => (EXTZ(64, v[22 .. 0]), EXTZ(64, v[30 .. 23]), [v[31]], 8, 23), - 64 => (EXTZ(64, v[51 .. 0]), EXTZ(64, v[62 .. 52]), [v[63]], 11, 52) + 16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10), + 32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23), + 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) }; assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); let table : vector(128, dec, int) = [ @@ -978,7 +978,7 @@ function rsqrt7 (v, sub) = { if sub then { let nr_leadingzeros = count_leadingzeros(sig, s); assert(nr_leadingzeros >= 0); - (to_bits(64, (0 - nr_leadingzeros)), EXTZ(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) + (to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) } else { (exp, sig) }; @@ -991,7 +991,7 @@ function rsqrt7 (v, sub) = { assert(idx >= 0 & idx < 128); let out_sig = to_bits(s, table[(127 - idx)]) << (s - 7); let out_exp = to_bits(e, (3 * (2^(e - 1) - 1) - 1 - signed(normalized_exp)) / 2); - EXTZ(64, sign @ out_exp @ out_sig) + zero_extend(64, sign @ out_exp @ out_sig) } val riscv_f16Rsqrte7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg} @@ -1051,9 +1051,9 @@ function riscv_f64Rsqrte7 (rm, v) = { val recip7 : forall 'm, 'm in {16, 32, 64}. (bits('m), bits(3), bool) -> (bool, bits_D) function recip7 (v, rm_3b, sub) = { let (sig, exp, sign, e, s) : (bits(64), bits(64), bits(1), nat, nat) = match 'm { - 16 => (EXTZ(64, v[9 .. 0]), EXTZ(64, v[14 .. 10]), [v[15]], 5, 10), - 32 => (EXTZ(64, v[22 .. 0]), EXTZ(64, v[30 .. 23]), [v[31]], 8, 23), - 64 => (EXTZ(64, v[51 .. 0]), EXTZ(64, v[62 .. 52]), [v[63]], 11, 52) + 16 => (zero_extend(64, v[9 .. 0]), zero_extend(64, v[14 .. 10]), [v[15]], 5, 10), + 32 => (zero_extend(64, v[22 .. 0]), zero_extend(64, v[30 .. 23]), [v[31]], 8, 23), + 64 => (zero_extend(64, v[51 .. 0]), zero_extend(64, v[62 .. 52]), [v[63]], 11, 52) }; assert(s == 10 & e == 5 | s == 23 & e == 8 | s == 52 & e == 11); let table : vector(128, dec, int) = [ @@ -1078,7 +1078,7 @@ function recip7 (v, rm_3b, sub) = { assert(nr_leadingzeros >= 0); let (normalized_exp, normalized_sig) = if sub then { - (to_bits(64, (0 - nr_leadingzeros)), EXTZ(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) + (to_bits(64, (0 - nr_leadingzeros)), zero_extend(64, sig[(s - 1) .. 0] << (1 + nr_leadingzeros))) } else { (exp, sig) }; @@ -1101,10 +1101,10 @@ function recip7 (v, rm_3b, sub) = { if sub & nr_leadingzeros > 1 then { if (rm_3b == 0b001 | rm_3b == 0b010 & sign == 0b0 | rm_3b == 0b011 & sign == 0b1) then { - (true, EXTZ(64, sign @ ones(e - 1) @ 0b0 @ ones(s))) + (true, zero_extend(64, sign @ ones(e - 1) @ 0b0 @ ones(s))) } - else (true, EXTZ(64, sign @ ones(e) @ zeros(s))) - } else (false, EXTZ(64, sign @ out_exp @ out_sig)) + else (true, zero_extend(64, sign @ ones(e) @ zeros(s))) + } else (false, zero_extend(64, sign @ out_exp @ out_sig)) } val riscv_f16Recip7 : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg} diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index a741bbce8..ff1eff994 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -547,7 +547,7 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let 'm = SEW; let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); result : vector('n, dec, bool) = undefined; @@ -599,7 +599,7 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); result : vector('n, dec, bool) = undefined; @@ -658,7 +658,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { }; let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -713,7 +713,7 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); - let imm_val : bits('m) = EXTS(simm); + let imm_val : bits('m) = sign_extend(simm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); result : vector('n, dec, bool) = undefined; diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index a37a65e50..7ad2fbdd6 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -105,7 +105,7 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { let SEW_pow_new = get_sew_pow(); if SEW_pow_new > LMUL_pow_new + ELEN_pow then { vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - vl = EXTZ(0b0); + vl = zeros(); print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); print_reg("CSR vl <- " ^ BitStr(vl)); return RETIRE_SUCCESS @@ -129,7 +129,7 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { let ratio_pow_new = SEW_pow_new - LMUL_pow_new; if (ratio_pow_new != ratio_pow_ori) then { vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - vl = EXTZ(0b0); + vl = zeros(); } }; print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); @@ -171,7 +171,7 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { let SEW_pow_new = get_sew_pow(); if SEW_pow_new > LMUL_pow_new + ELEN_pow then { vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - vl = EXTZ(0b0); + vl = zeros(); print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); print_reg("CSR vl <- " ^ BitStr(vl)); return RETIRE_SUCCESS diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index bb0b3b6c7..1c4ad7142 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -136,10 +136,10 @@ function readCSR csr : csreg -> xlenbits = { (0xB82, 32) => minstret[63 .. 32], /* vector */ - (0x008, _) => EXTZ(vstart), - (0x009, _) => EXTZ(vxsat), - (0x00A, _) => EXTZ(vxrm), - (0x00F, _) => EXTZ(vcsr.bits()), + (0x008, _) => zero_extend(vstart), + (0x009, _) => zero_extend(vxsat), + (0x00A, _) => zero_extend(vxrm), + (0x00F, _) => zero_extend(vcsr.bits()), (0xC20, _) => vl, (0xC21, _) => vtype.bits(), (0xC22, _) => vlenb, @@ -253,10 +253,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x015, _) => write_seed_csr(), /* vector */ - (0x008, _) => { let vstart_length = get_vlen_pow(); vstart = EXTZ(16, value[(vstart_length - 1) .. 0]); Some(EXTZ(vstart)) }, - (0x009, _) => { vxsat = value[0 .. 0]; Some(EXTZ(vxsat)) }, - (0x00A, _) => { vxrm = value[1 .. 0]; Some(EXTZ(vxrm)) }, - (0x00F, _) => { vcsr->bits() = value[2 ..0]; Some(EXTZ(vcsr.bits())) }, + (0x008, _) => { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); Some(zero_extend(vstart)) }, + (0x009, _) => { vxsat = value[0 .. 0]; Some(zero_extend(vxsat)) }, + (0x00A, _) => { vxrm = value[1 .. 0]; Some(zero_extend(vxrm)) }, + (0x00F, _) => { vcsr->bits() = value[2 ..0]; Some(zero_extend(vcsr.bits())) }, (0xC20, _) => { vl = value; Some(vl) }, (0xC21, _) => { vtype->bits() = value; Some(vtype.bits()) }, (0xC22, _) => { vlenb = value; Some(vlenb) }, diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 26cfbe3e9..789b9822f 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -600,19 +600,19 @@ function init_sys() -> unit = { minstret_increment = true; /* initialize vector csrs */ - vstart = EXTZ(0b0); + vstart = zero_extend(0b0); vxsat = 0b0; vxrm = 0b00; vcsr->vxrm() = vxrm; vcsr->vxsat() = vxsat; - vl = EXTZ(0b0); + vl = zero_extend(0b0); vtype->vill() = 0b1; - vtype->reserved() = EXTZ(0b0); + vtype->reserved() = zero_extend(0b0); vtype->vma() = 0b0; vtype->vta() = 0b0; vtype->vsew() = 0b000; vtype->vlmul() = 0b000; - vlenb = EXTZ(0b0); + vlenb = zero_extend(0b0); init_pmp(); diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index 9e47e9dc9..0fc1660e9 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -45,14 +45,14 @@ function clause ext_is_CSR_defined (0x009, _) = true function clause ext_is_CSR_defined (0x00A, _) = true function clause ext_is_CSR_defined (0x00F, _) = true -function clause ext_read_CSR (0x009) = Some (EXTZ (vcsr.vxsat())) -function clause ext_read_CSR (0x00A) = Some (EXTZ (vcsr.vxrm())) -function clause ext_read_CSR (0x00F) = Some (EXTZ (vcsr.bits())) +function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat())) +function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm())) +function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits())) -function clause ext_read_CSR (0x009) = Some (EXTZ (vcsr.vxsat())) -function clause ext_read_CSR (0x00A) = Some (EXTZ (vcsr.vxrm())) -function clause ext_read_CSR (0x00F) = Some (EXTZ (vcsr.bits())) +function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat())) +function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm())) +function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits())) -function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr.vxrm(), value[0 .. 0]); Some(EXTZ(vcsr.vxsat())) } -function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr.vxsat()); Some(EXTZ(vcsr.vxrm())) } -function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(EXTZ(vcsr.bits())) } +function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr.vxrm(), value[0 .. 0]); Some(zero_extend(vcsr.vxsat())) } +function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr.vxsat()); Some(zero_extend(vcsr.vxrm())) } +function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits())) } diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 3abaa25ff..338bffae6 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -108,7 +108,7 @@ mapping vreg_name = { val rV : forall 'n, 0 <= 'n < 32. regno('n) -> vregtype effect {rreg, escape} function rV r = { - let zero_vreg : vregtype = EXTZ(0x0); + let zero_vreg : vregtype = zeros(); let v : vregtype = match r { 0 => vr0, @@ -203,7 +203,7 @@ overload V = {rV_bits, wV_bits, rV, wV} val init_vregs : unit -> unit effect {wreg} function init_vregs () = { - let zero_vreg : vregtype = EXTZ(0x0); + let zero_vreg : vregtype = zeros(); vr0 = zero_vreg; vr1 = zero_vreg; vr2 = zero_vreg; @@ -286,7 +286,7 @@ function write_single_vreg(num_elem, SEW, vrid, v) = { assert(8 <= SEW & SEW <= 64); foreach (i from (num_elem - 1) downto 0) { r = r << SEW; - r = r | EXTZ(v[i]); + r = r | zero_extend(v[i]); }; V(vrid) = r @@ -377,9 +377,9 @@ function write_single_element(EEW, index, vrid, value) = { foreach (i from ('elem_per_reg - 1) downto 0) { r = r << EEW; if i == real_index then { - r = r | EXTZ(value); + r = r | zero_extend(value); } else { - r = r | EXTZ(vrid_val[i]); + r = r | zero_extend(vrid_val[i]); } }; V(real_vrid) = r;