diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 2d3a3ecc3..915a9fdfa 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -80,12 +80,12 @@ function clause execute(VVTYPE(funct6, vm, vs2, vs1, vd)) = { let VLEN_pow = get_vlen_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -214,15 +214,15 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + 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 vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -281,15 +281,15 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + 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 vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -298,9 +298,10 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { if mask[i] then { - let shift_amount = get_shift_amount(vs1_val[i], SEW); + 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 { NV_VNCLIPU => { @@ -343,12 +344,12 @@ function clause execute(MASKTYPEV(vs2, vs1, vd)) = { let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if vd == vreg_name("v0") then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -389,10 +390,12 @@ function clause execute(MOVETYPEV(vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -446,12 +449,12 @@ function clause execute(VXTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -564,15 +567,15 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + 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 rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -631,15 +634,15 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + 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 rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -648,9 +651,10 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { if mask[i] then { - let shift_amount = get_shift_amount(rs1_val, SEW); + 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 { NX_VNCLIPU => { @@ -699,12 +703,12 @@ function clause execute(VXSG(funct6, vm, vs2, rs1, vd)) = { let VLEN_pow = get_vlen_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : nat = unsigned(X(rs1)); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -763,12 +767,12 @@ function clause execute(MASKTYPEX(vs2, rs1, vd)) = { let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if vd == vreg_name("v0") then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -809,11 +813,13 @@ function clause execute(MOVETYPEX(rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; let rs1_val : bits('m) = get_scalar(rs1, 'm); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -858,12 +864,12 @@ function clause execute(VITYPE(funct6, vm, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let imm_val : bits('m) = EXTS(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); @@ -952,15 +958,15 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + 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 vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -1019,15 +1025,15 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + 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 vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -1036,9 +1042,10 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); + assert(SEW_widen <= 64); foreach (i from 0 to (num_elem - 1)) { if mask[i] then { - let shift_amount = get_shift_amount(imm_val, SEW); + 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 { NI_VNCLIPU => { @@ -1087,12 +1094,12 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let VLEN_pow = get_vlen_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let imm_val : nat = unsigned(EXTZ(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); @@ -1151,12 +1158,12 @@ function clause execute(MASKTYPEI(vs2, simm, vd)) = { let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if vd == vreg_name("v0") then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); let imm_val : bits('m) = EXTS(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); @@ -1197,10 +1204,12 @@ function clause execute(MOVETYPEI(vd, simm)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let imm_val : bits('m) = EXTS(simm); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -1239,7 +1248,7 @@ function clause execute(VMVRTYPE(vs2, simm, vd)) = { let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, EMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -1289,12 +1298,12 @@ function clause execute(MVVTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1399,12 +1408,12 @@ function clause execute(MVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let VLEN = int_power(2, get_vlen_pow()); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1462,15 +1471,16 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | - not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | + not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -1532,15 +1542,15 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -1596,15 +1606,16 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | - not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | + not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -1657,15 +1668,15 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { let SEW_half = SEW / 2; let LMUL_pow_half = LMUL_pow - 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_half, LMUL_pow)) | - not(valid_eew_emul(SEW_half, LMUL_pow_half)) + if illegal_variable_width(vd, vm, SEW_half, LMUL_pow_half) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_half, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_half; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_half, LMUL_pow_half, vs2); result : vector('n, dec, bits('m)) = undefined; @@ -1715,15 +1726,15 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { let SEW_quart = SEW / 4; let LMUL_pow_quart = LMUL_pow - 2; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_quart, LMUL_pow)) | - not(valid_eew_emul(SEW_quart, LMUL_pow_quart)) + if illegal_variable_width(vd, vm, SEW_quart, LMUL_pow_quart) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_quart, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_quart; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_quart, LMUL_pow_quart, vs2); result : vector('n, dec, bits('m)) = undefined; @@ -1773,15 +1784,15 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { let SEW_eighth = SEW / 8; let LMUL_pow_eighth = LMUL_pow - 3; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow_eighth, LMUL_pow)) | - not(valid_eew_emul(SEW_eighth, LMUL_pow_eighth)) + if illegal_variable_width(vd, vm, SEW_eighth, LMUL_pow_eighth) | + not(valid_reg_overlap(vs2, vd, LMUL_pow_eighth, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_eighth; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_eighth, LMUL_pow_eighth, vs2); result : vector('n, dec, bits('m)) = undefined; @@ -1822,6 +1833,8 @@ function clause execute(VMVXS(vs2, rd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + assert(num_elem > 0); let 'n = num_elem; let 'm = SEW; @@ -1847,14 +1860,14 @@ mapping clause encdec = MVVCOMPRESS(vs2, vs1, vd) if haveRVV() function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { let start_element = get_start_element(); let end_element = get_end_element(); - - /* vcompress should always be executed with a vstart of 0 */ - if (start_element != 0 | vs1 == vd | vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; - let SEW = get_sew(); let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + /* vcompress should always be executed with a vstart of 0 */ + if start_element != 0 | vs1 == vd | vs2 == vd | illegal_vd_unmasked() + then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; @@ -1922,12 +1935,12 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1964,7 +1977,6 @@ function clause execute(MVXTYPE(funct6, vm, vs2, rs1, vd)) = { if i == 0 then rs1_val else vs2_val[i - 1] }, MVX_VSLIDE1DOWN => { - if (vs2 == vd) then { handle_illegal(); return RETIRE_FAIL }; let last_elem = get_end_element(); assert(last_elem < num_elem); if i < last_elem then vs2_val[i + 1] else rs1_val @@ -2044,12 +2056,12 @@ function clause execute(MVXMATYPE(funct6, vm, vs2, rs1, vd)) = { let VLEN = int_power(2, get_vlen_pow()); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -2108,15 +2120,15 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -2178,14 +2190,14 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -2242,15 +2254,15 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) + if illegal_variable_width(vd, vm, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -2296,11 +2308,13 @@ function clause execute(VMVSX(rs1, vd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + assert(num_elem > 0); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, 'm); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vd); result : vector('n, dec, bits('m)) = undefined; diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 5830fcf20..2e0e2570d 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -66,13 +66,13 @@ function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -141,13 +141,13 @@ function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -210,7 +210,7 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; @@ -220,7 +220,7 @@ function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -275,7 +275,7 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; @@ -285,7 +285,7 @@ function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -339,8 +339,8 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | not(valid_fp_op(SEW, rm_3b)) + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | + not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); @@ -348,7 +348,7 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -400,12 +400,12 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -515,7 +515,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 8 & SEW_widen <= 64); @@ -524,7 +524,7 @@ function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); result : vector('n, dec, bits('o)) = undefined; @@ -645,7 +645,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -653,7 +653,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -778,12 +778,12 @@ function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; @@ -860,7 +860,8 @@ function clause execute(VFMVFS(vs2, rd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if not(valid_fp_op(SEW, rm_3b)) | SEW > sizeof(flen) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) | SEW > sizeof(flen) + then { handle_illegal(); return RETIRE_FAIL }; assert(num_elem > 0 & SEW != 8); let 'n = num_elem; @@ -905,13 +906,13 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -939,7 +940,6 @@ function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = { if i == 0 then rs1_val else vs2_val[i - 1] }, VF_VSLIDE1DOWN => { - if vs2 == vd then { handle_illegal(); return RETIRE_FAIL }; let last_elem = get_end_element(); assert(last_elem < num_elem); if i < last_elem then vs2_val[i + 1] else rs1_val @@ -996,13 +996,13 @@ function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1065,7 +1065,7 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); @@ -1074,7 +1074,7 @@ function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -1129,7 +1129,7 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); @@ -1138,7 +1138,7 @@ function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); @@ -1192,7 +1192,7 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_rd_mask(vd, vm)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | not(valid_fp_op(SEW, rm_3b)) + if illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); @@ -1200,7 +1200,7 @@ function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = { let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vs2); @@ -1247,13 +1247,13 @@ function clause execute(VFMERGE(vs2, rs1, vd)) = { let num_elem = get_num_elem(LMUL_pow, SEW); /* max(VLMAX,VLEN/SEW)) */ let real_num_elem = if LMUL_pow >= 0 then num_elem else num_elem / (0 - LMUL_pow); /* VLMAX */ - if vd == vreg_name("v0") | not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_masked(vd, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, 0b00000); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1296,14 +1296,14 @@ function clause execute(VFMV(rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -1333,13 +1333,13 @@ function clause execute(VFMVSF(rs1, vd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(num_elem > 0 & SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, 0b1, 0b00000); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vd); result : vector('n, dec, bits('m)) = undefined; diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index 587fbdd63..5f1be7af6 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -63,6 +63,8 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; @@ -120,17 +122,16 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); + if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2); result : vector('n, dec, bool) = undefined; mask : vector('n, dec, bool) = undefined; - /* Value of vstart must be 0 */ - if not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; - (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); count : nat = 0; @@ -157,17 +158,16 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); + if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2); result : vector('n, dec, bool) = undefined; mask : vector('n, dec, bool) = undefined; - /* Value of vstart must be 0 */ - if not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; - (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vs2_val, vm_val); index : int = -1; @@ -196,24 +196,18 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 + then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); result : vector('n, dec, bool) = undefined; mask : vector('n, dec, bool) = undefined; - /* Value of vstart must be 0 */ - if not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; - - /* If masking is enabled, then dest reg cannot be v0 */ - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; - - /* Dest reg cannot be the same as source reg */ - if vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; - (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); found_elem : bool = false; @@ -243,24 +237,18 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 + then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); result : vector('n, dec, bool) = undefined; mask : vector('n, dec, bool) = undefined; - /* Value of vstart must be 0 */ - if not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; - - /* If masking is enabled, then dest reg cannot be v0 */ - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; - - /* Dest reg cannot be the same as source reg */ - if vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; - (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); found_elem : bool = false; @@ -290,24 +278,18 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 + then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); result : vector('n, dec, bool) = undefined; mask : vector('n, dec, bool) = undefined; - /* Value of vstart must be 0 */ - if not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; - - /* If masking is enabled, then dest reg cannot be v0 */ - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; - - /* Dest reg cannot be the same as source reg */ - if vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; - (result, mask) = init_masked_result_cmp(num_elem, SEW, 0, vd_val, vm_val); found_elem : bool = false; @@ -341,24 +323,18 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 + then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs2_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); result : vector('n, dec, bits('m)) = undefined; mask : vector('n, dec, bool) = undefined; - /* Value of vstart must be 0 */ - if not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; - - /* If masking is enabled, then dest reg cannot be v0 */ - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; - - /* Dest reg cannot be the same as source reg */ - if vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; - (result, mask) = init_masked_result(num_elem, SEW, LMUL_pow, vd_val, vm_val); sum : int = 0; @@ -388,12 +364,12 @@ function clause execute(VID_V(vm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + 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); result : vector('n, dec, bits('m)) = undefined; mask : vector('n, dec, bool) = undefined; diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index c38d1a7dd..796ea4ad8 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -107,7 +107,7 @@ mapping clause encdec = VLETYPE(vm, rs1, width, vd) if haveRVV() val process_vle : forall 'b 'n 'p, ('b in {1, 2, 4, 8}) & ('n >= 0). (bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vle (vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); total : vector('n, dec, bits('b * 8)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -153,7 +153,7 @@ function clause execute(VLETYPE(vm, rs1, width, vd)) = { let EMUL_pow = EEW_pow - SEW_pow + LMUL_pow; let num_elem = get_num_elem(EMUL_pow, EEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vle(vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -177,7 +177,7 @@ mapping clause encdec = VSETYPE(vm, rs1, width, vs3) if haveRVV() val process_vse : forall 'b 'n 'p, ('b in {1, 2, 4, 8}) & ('n >= 0). (bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vse (vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vs3); total : vector('n, dec, bits('b * 8)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -230,6 +230,8 @@ function clause execute(VSETYPE(vm, rs1, width, vs3)) = { let EMUL_pow = EEW_pow - SEW_pow + LMUL_pow; let num_elem = get_num_elem(EMUL_pow, EEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + process_vse(vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -252,7 +254,7 @@ mapping clause encdec = VLSETYPE(vm, rs2, rs1, width, vd) if haveRVV() val process_vlse : forall 'b 'n 'p, ('b in {1, 2, 4, 8}) & ('n >= 0). (bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vlse (vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); total : vector('n, dec, bits('b * 8)) = undefined; @@ -299,7 +301,7 @@ function clause execute(VLSETYPE(vm, rs2, rs1, width, vd)) = { let EMUL_pow = EEW_pow - SEW_pow + LMUL_pow; let num_elem = get_num_elem(EMUL_pow, EEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vlse(vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -323,7 +325,7 @@ mapping clause encdec = VSSETYPE(vm, rs2, rs1, width, vs3) if haveRVV() val process_vsse : forall 'b 'n 'p, ('b in {1, 2, 4, 8}) & ('n >= 0). (bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vsse (vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vs3); let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); total : vector('n, dec, bits('b * 8)) = undefined; @@ -377,6 +379,8 @@ function clause execute(VSSETYPE(vm, rs2, rs1, width, vs3)) = { let EMUL_pow = EEW_pow - SEW_pow + LMUL_pow; let num_elem = get_num_elem(EMUL_pow, EEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + process_vsse(vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -399,7 +403,7 @@ mapping clause encdec = VLUXEITYPE(vm, vs2, rs1, width, vd) if haveRVV() val process_vlxei : forall 'ib 'db 'ip 'dp 'n, ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vlxei (vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let width_type : word_width = bytes_wordwidth(EEW_data_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); total : vector('n, dec, bits('db * 8)) = undefined; @@ -446,7 +450,7 @@ function clause execute(VLUXEITYPE(vm, vs2, rs1, width, vd)) = { let EMUL_index_pow = EEW_index_pow - EEW_data_pow + EMUL_data_pow; let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vlxei(vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) } @@ -469,7 +473,7 @@ function clause execute(VLOXEITYPE(vm, vs2, rs1, width, vd)) = { let EMUL_index_pow = EEW_index_pow - EEW_data_pow + EMUL_data_pow; let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vlxei(vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) } @@ -486,7 +490,7 @@ mapping clause encdec = VSUXEITYPE(vm, vs2, rs1, width, vs3) if haveRVV() val process_vsxei : forall 'ib 'db 'ip 'dp 'n, ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired effect {eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vsxei (vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = { let width_type : word_width = bytes_wordwidth(EEW_data_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vs3); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); total : vector('n, dec, bits('db * 8)) = undefined; /* just used to generate mask */ @@ -540,6 +544,8 @@ function clause execute(VSUXEITYPE(vm, vs2, rs1, width, vs3)) = { let EMUL_index_pow = EEW_index_pow - EEW_data_pow + EMUL_data_pow; let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); /* number of data and indices are the same */ + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + process_vsxei(vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 1) } @@ -561,6 +567,8 @@ function clause execute(VSOXEITYPE(vm, vs2, rs1, width, vs3)) = { let EMUL_index_pow = EEW_index_pow - EEW_data_pow + EMUL_data_pow; let num_elem = get_num_elem(EMUL_data_pow, EEW_data_bytes * 8); /* number of data and indices are the same */ + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + process_vsxei(vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, 3) } @@ -576,7 +584,7 @@ mapping clause encdec = VLEFFTYPE(vm, rs1, width, vd) if haveRVV() val process_vleff : forall 'b 'n 'p, ('b in {1, 2, 4, 8}) & ('n >= 0). (bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired effect {escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg} function process_vleff (vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = { let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); total : vector('n, dec, bits('b * 8)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -651,7 +659,7 @@ function clause execute(VLEFFTYPE(vm, rs1, width, vd)) = { let EMUL_pow = EEW_pow - SEW_pow + LMUL_pow; let num_elem = get_num_elem(EMUL_pow, EEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vleff(vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -676,7 +684,7 @@ val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8} 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); status : Retired = RETIRE_SUCCESS; vd_a = vd; vd_t = vd; @@ -731,7 +739,7 @@ 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); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vlseg(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -750,7 +758,7 @@ 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); let start_element = get_start_element(); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); status : Retired = RETIRE_SUCCESS; if start_element >= num_elem then return status; @@ -824,7 +832,7 @@ function clause execute(VLSEGFFTYPE(nf, vm, rs1, width, vd)) = { let num_elem = get_num_elem(EMUL_pow, EEW); let nf_int = nfields_int(nf); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vlsegff(nf_int, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -843,7 +851,7 @@ 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); let start_element = get_start_element(); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); status : Retired = RETIRE_SUCCESS; if start_element >= num_elem then return status; @@ -896,6 +904,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); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + process_vsseg(nf_int, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -912,7 +922,7 @@ val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vd); /* only to generate mask */ result : vector('n, dec, bits('b * 8)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -960,7 +970,7 @@ 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); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL }; process_vlsseg(nf_int, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -978,7 +988,7 @@ val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8 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 int_power(2, EMUL_pow); let width_type : word_width = bytes_wordwidth(load_width_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('b * 8)) = read_vreg(num_elem, load_width_bytes * 8, EMUL_pow, vs3); /* only to generate mask */ result : vector('n, dec, bits('b * 8)) = undefined; mask : vector('n, dec, bool) = undefined; @@ -1035,6 +1045,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); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + process_vssseg(nf_int, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -1051,7 +1063,7 @@ val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in 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 int_power(2, EMUL_data_pow); let width_type : word_width = bytes_wordwidth(EEW_data_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vd); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); total : vector('n, dec, bits('db * 8)) = undefined; @@ -1100,7 +1112,7 @@ 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); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) 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) } @@ -1124,7 +1136,7 @@ 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); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_normal(vd, vm) 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) } @@ -1142,7 +1154,7 @@ val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in 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 int_power(2, EMUL_data_pow); let width_type : word_width = bytes_wordwidth(EEW_data_bytes); - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_val : vector('n, dec, bits('db * 8)) = read_vreg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, vs3); let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); total : vector('n, dec, bits('db * 8)) = undefined; @@ -1200,6 +1212,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); + if illegal_vd_unmasked() 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) } @@ -1222,6 +1236,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); + if illegal_vd_unmasked() 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) } @@ -1504,6 +1520,8 @@ function clause execute(VMTYPE(rs1, vd_or_vs3, op)) = { let tmp = unsigned(vl); let num_elem : int = if tmp % 8 == 0 then tmp / 8 else tmp / 8 + 1; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + /* unmask vle8 except that the effective vector length is evl=ceil(vl/8) */ assert(num_elem >= 0); process_vm(vd_or_vs3, rs1, EMUL_pow, num_elem, op) diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 362fcb5d7..afa0b95ea 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -59,13 +59,13 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_reduction_widen(SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); result : vector('n, dec, bits('o)) = undefined; @@ -124,12 +124,12 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_rd_mask(vd, vm)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_reduction() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); result : vector('n, dec, bits('m)) = undefined; @@ -190,13 +190,13 @@ mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveRVV() val process_rfvv_single: forall 'n 'm 'p, 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired effect {escape, rreg, undef, wreg} function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) = { let rm_3b = fcsr.FRM(); - if not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_reduction(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); result : vector('n, dec, bits('m)) = undefined; @@ -227,15 +227,14 @@ function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem, SEW, LMUL_pow) = let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) | not(valid_fp_op(SEW, rm_3b)) - then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); let 'n = num_elem; let 'm = SEW; let 'o = SEW_widen; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vd_val : vector('n, dec, bits('o)) = read_vreg(num_elem, SEW_widen, LMUL_pow_widen, vd); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); result : vector('n, dec, bits('o)) = undefined; diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index a5c28916c..d498cbe01 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -53,6 +53,15 @@ function valid_eew_emul(EEW, EMUL_pow) = { EEW >= 8 & EEW <= ELEN & EMUL_pow >= -3 & EMUL_pow <= 3 } +/* Check for valid vtype setting + * 1. If the vill bit is set, then any attempt to execute a vector instruction that depends upon vtype will raise an illegal instruction exception. + * 2. vset{i}vl{i} and whole-register loads, stores, and moves do not depend upon vtype. + */ +val valid_vtype : unit -> bool effect {rreg} +function valid_vtype() = { + vtype.vill() == 0b0 +} + /* Check for vstart value */ val assert_vstart : int -> bool effect {rreg} function assert_vstart(i) = { @@ -79,7 +88,7 @@ function valid_fp_op(SEW, rm_3b) = { */ val valid_rd_mask : (regidx, bits(1)) -> bool function valid_rd_mask(rd, vm) = { - vm != 0b0 | rd != vreg_name("v0") + vm != 0b0 | rd != 0b00000 } /* Check for valid register overlap in vector widening/narrowing instructions: @@ -103,6 +112,96 @@ function valid_reg_overlap(rs, rd, EMUL_pow_rs, EMUL_pow_rd) = { is_valid } +/* ******************************************************************************* */ +/* The following functions summarize patterns of illegal instruction check. */ +/* ******************************************************************************* */ + +/* a. Normal check including vtype.vill field and vd/v0 overlap if vm = 0 */ +val illegal_normal : (regidx, bits(1)) -> bool +function illegal_normal(vd, vm) = { + not(valid_vtype()) | not(valid_rd_mask(vd, vm)) +} + +/* b. Masked check for instructions encoded with vm = 0 */ +val illegal_vd_masked : regidx -> bool +function illegal_vd_masked(vd) = { + not(valid_vtype()) | vd == 0b00000 +} + +/* c. Unmasked check for: + * 1. instructions encoded with vm = 1 + * 2. instructions with scalar rd: vcpop.m, vfirst.m + * 3. instructions with vs3 rather than vd: vector stores + * 4. vd as mask register (eew = 1): + * vmadc.vvm/vxm/vim, vmsbc.vvm/vxm, mask logical, integer compare, vlm.v, vsm.v + */ +val illegal_vd_unmasked : unit -> bool +function illegal_vd_unmasked() = { + not(valid_vtype()) +} + +/* d. Variable width check for: + * 1. integer/fixed-point widening/narrowing instructions + * 2. vector integer extension: vzext, vsext + */ +val illegal_variable_width : (regidx, bits(1), int, int) -> bool +function illegal_variable_width(vd, vm, SEW_new, LMUL_pow_new) = { + not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_eew_emul(SEW_new, LMUL_pow_new)) +} + +/* e. Normal check for reduction instructions: + * The destination vector register can overlap the source operands, including the mask register. + * Vector reduction operations raise an illegal instruction exception if vstart is non-zero. + */ +val illegal_reduction : unit -> bool +function illegal_reduction() = { + not(valid_vtype()) | not(assert_vstart(0)) +} + +/* f. Variable width check for widening reduction instructions */ +val illegal_reduction_widen : (int, int) -> bool +function illegal_reduction_widen(SEW_widen, LMUL_pow_widen) = { + not(valid_vtype()) | not(assert_vstart(0)) | not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) +} + +/* g. Normal check for floating-point instructions */ +val illegal_fp_normal : (regidx, bits(1), {|8, 16, 32, 64|}, bits(3)) -> bool +function illegal_fp_normal(vd, vm, SEW, rm_3b) = { + not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) +} + +/* h. Masked check for floating-point instructions encoded with vm = 0 */ +val illegal_fp_vd_masked : (regidx, {|8, 16, 32, 64|}, bits(3)) -> bool +function illegal_fp_vd_masked(vd, SEW, rm_3b) = { + not(valid_vtype()) | vd == 0b00000 | not(valid_fp_op(SEW, rm_3b)) +} + +/* i. Unmasked check for floating-point instructions encoded with vm = 1 */ +val illegal_fp_vd_unmasked : ({|8, 16, 32, 64|}, bits(3)) -> bool +function illegal_fp_vd_unmasked(SEW, rm_3b) = { + not(valid_vtype()) | not(valid_fp_op(SEW, rm_3b)) +} + +/* j. Variable width check for floating-point widening/narrowing instructions */ +val illegal_fp_variable_width : (regidx, bits(1), {|8, 16, 32, 64|}, bits(3), int, int) -> bool +function illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_new, LMUL_pow_new) = { + not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) | + not(valid_eew_emul(SEW_new, LMUL_pow_new)) +} + +/* k. Normal check for floating-point reduction instructions */ +val illegal_fp_reduction : ({|8, 16, 32, 64|}, bits(3)) -> bool +function illegal_fp_reduction(SEW, rm_3b) = { + not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) +} + +/* l. Variable width check for floating-point widening reduction instructions */ +val illegal_fp_reduction_widen : ({|8, 16, 32, 64|}, bits(3), int, int) -> bool +function illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) = { + not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) | + not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) +} + /* Scalar register shaping */ val get_scalar : forall 'n, 'n >= 8. (regidx, int('n)) -> bits('n) effect {escape, rreg} function get_scalar(rs1, SEW) = { diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail index aa681152f..6784ce7e4 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -60,10 +60,12 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); @@ -114,6 +116,8 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; @@ -167,7 +171,7 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if vd == vreg_name("v0") then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -178,7 +182,7 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = { vec_trues[i] = true }; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -230,10 +234,12 @@ function clause execute(VVCMPTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); @@ -292,10 +298,12 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); @@ -346,6 +354,8 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; @@ -399,7 +409,7 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if vd == vreg_name("v0") then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -410,7 +420,7 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = { vec_trues[i] = true }; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -464,10 +474,12 @@ function clause execute(VXCMPTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar(rs1, SEW); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); @@ -529,10 +541,12 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); let imm_val : bits('m) = EXTS(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); @@ -580,6 +594,8 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; @@ -630,7 +646,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if vd == vreg_name("v0") then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -641,7 +657,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = { vec_trues[i] = true }; - let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask_carry(num_elem, 0b0, 0b00000); let imm_val : bits('m) = EXTS(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); @@ -691,10 +707,12 @@ function clause execute(VICMPTYPE(funct6, vm, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; + let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let imm_val : bits('m) = EXTS(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); @@ -754,13 +772,13 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let vs1_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs1); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); @@ -818,13 +836,13 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_fp_op(SEW, rm_3b)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_fp_vd_unmasked(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW != 8); let 'n = num_elem; let 'm = SEW; - let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, vreg_name("v0")); + let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000); let rs1_val : bits('m) = get_scalar_fp(rs1, 'm); let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, dec, bool) = read_vmask(num_elem, 0b0, vd); diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 072fad38b..d84adc62d 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -88,11 +88,12 @@ mapping clause encdec = VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) if haveRVV() function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { let VLEN_pow = get_vlen_pow(); + let ELEN_pow = get_elen_pow(); let LMUL_pow_ori = get_lmul_pow(); let SEW_pow_ori = get_sew_pow(); let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; - /* set vtype and calculate VLMAX */ + /* set vtype */ match op { VSETVLI => { vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul @@ -102,10 +103,18 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { vtype->bits() = X(rs2) } }; - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + + /* check legal SEW and LMUL and calculate VLMAX */ let LMUL_pow_new = get_lmul_pow(); let SEW_pow_new = get_sew_pow(); - let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new); + if SEW_pow_new > LMUL_pow_new + ELEN_pow then { + vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vl = EXTZ(0b0); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vl <- " ^ BitStr(vl)); + return RETIRE_SUCCESS + }; + let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new); /* set vl according to VLMAX and AVL */ if (rs1 != 0b00000) then { /* normal stripmining */ @@ -115,20 +124,20 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) /* ceil(AVL / 2) ≤ vl ≤ VLMAX */ else to_bits(sizeof(xlen), VLMAX); X(rd) = vl; - print_reg("CSR vl <- " ^ BitStr(vl)) } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); vl = to_bits(sizeof(xlen), VLMAX); X(rd) = vl; - print_reg("CSR vl <- " ^ BitStr(vl)) } else { /* keep existing vl */ let AVL = unsigned(vl); 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 */ - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + vl = EXTZ(0b0); } }; + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vl <- " ^ BitStr(vl)); /* reset vstart to 0 */ vstart = EXTZ(0b0); @@ -153,24 +162,33 @@ mapping clause encdec = VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) if haveRVV() function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { let VLEN_pow = get_vlen_pow(); + let ELEN_pow = get_elen_pow(); let LMUL_pow_ori = get_lmul_pow(); let SEW_pow_ori = get_sew_pow(); let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; - /* set vtype and calculate VLMAX */ + /* set vtype */ vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + /* check legal SEW and LMUL and calculate VLMAX */ let LMUL_pow_new = get_lmul_pow(); let SEW_pow_new = get_sew_pow(); - let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new); - let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */ + if SEW_pow_new > LMUL_pow_new + ELEN_pow then { + vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vl = EXTZ(0b0); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vl <- " ^ BitStr(vl)); + return RETIRE_SUCCESS + }; + let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new); + let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */ /* set vl according to VLMAX and AVL */ vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) /* ceil(AVL / 2) ≤ vl ≤ VLMAX */ else to_bits(sizeof(xlen), VLMAX); X(rd) = vl; + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); print_reg("CSR vl <- " ^ BitStr(vl)); /* reset vstart to 0 */ diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6f95e9c5e..7e3bff11b 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -603,8 +603,8 @@ function init_sys() -> unit = { vxrm = 0b00; vcsr->vxrm() = vxrm; vcsr->vxsat() = vxsat; - vl = EXTZ(0b10000); /* the default value is 16 */ - vtype->vill() = 0b0; + vl = EXTZ(0b0); + vtype->vill() = 0b1; vtype->reserved() = EXTZ(0b0); vtype->vma() = 0b0; vtype->vta() = 0b0; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index a96a9e3f8..5169e73f9 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -849,7 +849,6 @@ register vtype : Vtype /* this returns the power of 2 for SEW */ val get_sew_pow : unit -> {|3, 4, 5, 6|} effect {escape, rreg} function get_sew_pow() = { - let ELEN_pow = get_elen_pow(); let SEW_pow : {|3, 4, 5, 6|} = match vtype.vsew() { 0b000 => 3, 0b001 => 4, @@ -857,7 +856,6 @@ function get_sew_pow() = { 0b011 => 6, _ => {assert(false, "invalid vsew field in vtype"); 0} }; - assert(SEW_pow <= ELEN_pow); SEW_pow } /* this returns the actual value of SEW */