diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 68a986b3a..915a9fdfa 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -80,7 +80,7 @@ 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_vtype()) | 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; @@ -214,7 +214,7 @@ function clause execute(NVSTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -281,7 +281,7 @@ function clause execute(NVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -344,7 +344,7 @@ 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 not(valid_vtype()) | vd == 0b00000 then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -390,7 +390,7 @@ function clause execute(MOVETYPEV(vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -449,7 +449,7 @@ 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_vtype()) | 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; @@ -567,7 +567,7 @@ function clause execute(NXSTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -634,7 +634,7 @@ function clause execute(NXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -703,7 +703,7 @@ 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_vtype()) | 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; @@ -767,7 +767,7 @@ 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 not(valid_vtype()) | vd == 0b00000 then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -813,7 +813,7 @@ function clause execute(MOVETYPEX(rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -864,7 +864,7 @@ 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_vtype()) | 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; @@ -958,7 +958,7 @@ function clause execute(NISTYPE(funct6, vm, vs2, simm, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -1025,7 +1025,7 @@ function clause execute(NITYPE(funct6, vm, vs2, simm, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -1094,7 +1094,7 @@ 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_vtype()) | 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; @@ -1158,7 +1158,7 @@ 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 not(valid_vtype()) | vd == 0b00000 then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -1204,7 +1204,7 @@ function clause execute(MOVETYPEI(vd, simm)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -1298,7 +1298,7 @@ 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_vtype()) | 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; @@ -1408,7 +1408,7 @@ 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_vtype()) | 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; @@ -1471,7 +1471,7 @@ function clause execute(WVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | 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 }; @@ -1542,7 +1542,7 @@ function clause execute(WVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs1, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; @@ -1606,7 +1606,7 @@ function clause execute(WMVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | 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 }; @@ -1668,7 +1668,7 @@ function clause execute(VEXT2TYPE(funct6, vm, vs2, vd)) = { let SEW_half = SEW / 2; let LMUL_pow_half = LMUL_pow - 1; - if not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | 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 }; @@ -1726,7 +1726,7 @@ function clause execute(VEXT4TYPE(funct6, vm, vs2, vd)) = { let SEW_quart = SEW / 4; let LMUL_pow_quart = LMUL_pow - 2; - if not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | 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 }; @@ -1784,7 +1784,7 @@ function clause execute(VEXT8TYPE(funct6, vm, vs2, vd)) = { let SEW_eighth = SEW / 8; let LMUL_pow_eighth = LMUL_pow - 3; - if not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | 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 }; @@ -1833,7 +1833,7 @@ function clause execute(VMVXS(vs2, rd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; assert(num_elem > 0); let 'n = num_elem; @@ -1865,7 +1865,7 @@ function clause execute(MVVCOMPRESS(vs2, vs1, vd)) = { 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 | not(valid_vtype()) + if start_element != 0 | vs1 == vd | vs2 == vd | illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; @@ -1935,7 +1935,7 @@ 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_vtype()) | 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; @@ -2056,7 +2056,7 @@ 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_vtype()) | 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; @@ -2120,7 +2120,7 @@ function clause execute(WVXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; @@ -2190,7 +2190,7 @@ function clause execute(WXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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; @@ -2254,7 +2254,7 @@ function clause execute(WMVXTYPE(funct6, vm, vs2, rs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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) | not(valid_reg_overlap(vs2, vd, LMUL_pow, LMUL_pow_widen)) then { handle_illegal(); return RETIRE_FAIL }; @@ -2308,7 +2308,7 @@ function clause execute(VMVSX(rs1, vd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; assert(num_elem > 0); let 'n = num_elem; diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 293c606c9..2e0e2570d 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -66,8 +66,7 @@ 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_vtype()) | 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; @@ -142,8 +141,7 @@ 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_vtype()) | 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; @@ -212,8 +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_vtype()) | 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 }; @@ -278,8 +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_vtype()) | 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 }; @@ -343,8 +339,7 @@ function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | 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)) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); @@ -405,8 +400,7 @@ 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_vtype()) | 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; @@ -521,8 +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_vtype()) | 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 >= 8 & SEW_widen <= 64); @@ -652,8 +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_vtype()) | 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_widen, LMUL_pow)) then { handle_illegal(); return RETIRE_FAIL }; @@ -786,8 +778,7 @@ 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_vtype()) | 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; @@ -869,7 +860,7 @@ function clause execute(VFMVFS(vs2, rd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if not(valid_vtype()) | not(valid_fp_op(SEW, rm_3b)) | SEW > sizeof(flen) + if illegal_fp_vd_unmasked(SEW, rm_3b) | SEW > sizeof(flen) then { handle_illegal(); return RETIRE_FAIL }; assert(num_elem > 0 & SEW != 8); @@ -915,8 +906,7 @@ 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_vtype()) | 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; @@ -1006,8 +996,7 @@ 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_vtype()) | 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; @@ -1076,8 +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_vtype()) | 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); @@ -1141,8 +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_vtype()) | 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); @@ -1205,8 +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_vtype()) | 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) then { handle_illegal(); return RETIRE_FAIL }; assert(SEW >= 16 & SEW_widen <= 64); @@ -1261,8 +1247,7 @@ 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 not(valid_vtype()) | vd == 0b00000 | 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; @@ -1311,7 +1296,7 @@ function clause execute(VFMV(rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) | 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; @@ -1348,7 +1333,7 @@ function clause execute(VFMVSF(rs1, vd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if not(valid_vtype()) | 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; diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index bdfe20ae4..5f1be7af6 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -63,7 +63,7 @@ function clause execute(MMTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -122,7 +122,7 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); - if not(valid_vtype()) | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -158,7 +158,7 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); - if not(valid_vtype()) | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -196,7 +196,7 @@ function clause execute(VMSBF_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); - if not(valid_vtype()) | not(assert_vstart(0)) | not(valid_rd_mask(vd, vm)) | vd == vs2 + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; @@ -237,7 +237,7 @@ function clause execute(VMSIF_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); - if not(valid_vtype()) | not(assert_vstart(0)) | not(valid_rd_mask(vd, vm)) | vd == vs2 + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; @@ -278,7 +278,7 @@ function clause execute(VMSOF_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = int_power(2, get_vlen_pow()); - if not(valid_vtype()) | not(assert_vstart(0)) | not(valid_rd_mask(vd, vm)) | vd == vs2 + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; @@ -323,7 +323,7 @@ function clause execute(VIOTA_M(vm, vs2, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) | not(assert_vstart(0)) | not(valid_rd_mask(vd, vm)) | vd == vs2 + if illegal_normal(vd, vm) | not(assert_vstart(0)) | vd == vs2 then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; @@ -364,7 +364,7 @@ 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_vtype()) | 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; diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index a001cfb56..796ea4ad8 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -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_vtype()) | 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) } @@ -230,7 +230,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; process_vse(vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -301,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_vtype()) | 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) } @@ -379,7 +379,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; process_vsse(vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) } @@ -450,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_vtype()) | 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) } @@ -473,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_vtype()) | 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) } @@ -544,7 +544,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + 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) } @@ -567,7 +567,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + 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) } @@ -659,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_vtype()) | 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) } @@ -739,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_vtype()) | 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) } @@ -832,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_vtype()) | 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) } @@ -904,7 +904,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; process_vsseg(nf_int, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) } @@ -970,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_vtype()) | 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) } @@ -1045,7 +1045,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + 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) } @@ -1112,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_vtype()) | 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) } @@ -1136,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_vtype()) | 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) } @@ -1212,7 +1212,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + 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) } @@ -1236,7 +1236,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + 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) } @@ -1520,7 +1520,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + 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); diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail index 714cf805b..afa0b95ea 100755 --- a/model/riscv_insts_vext_red.sail +++ b/model/riscv_insts_vext_red.sail @@ -59,8 +59,7 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = { let SEW_widen = SEW * 2; let LMUL_pow_widen = LMUL_pow + 1; - if not(valid_vtype()) | not(assert_vstart(0)) | 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; @@ -125,7 +124,7 @@ 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_vtype()) | not(assert_vstart(0)) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_reduction() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -191,8 +190,7 @@ 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_vtype()) | not(assert_vstart(0)) | 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; @@ -229,9 +227,7 @@ 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_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) | - not(valid_eew_emul(SEW_widen, LMUL_pow_widen)) - 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; diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index d6afec730..d498cbe01 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -112,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 47af56626..6784ce7e4 100755 --- a/model/riscv_insts_vext_vm.sail +++ b/model/riscv_insts_vext_vm.sail @@ -60,7 +60,7 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -116,7 +116,7 @@ function clause execute(VVMCTYPE(funct6, vs2, vs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -171,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 not(valid_vtype()) | vd == 0b00000 then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -234,7 +234,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -298,7 +298,7 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -354,7 +354,7 @@ function clause execute(VXMCTYPE(funct6, vs2, rs1, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -409,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 not(valid_vtype()) | vd == 0b00000 then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -474,7 +474,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -541,7 +541,7 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -594,7 +594,7 @@ function clause execute(VIMCTYPE(funct6, vs2, simm, vd)) = { let LMUL_pow = get_lmul_pow(); let num_elem = get_num_elem(LMUL_pow, SEW); - if not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -646,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 not(valid_vtype()) | vd == 0b00000 then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_masked(vd) then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -707,7 +707,7 @@ 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 not(valid_vtype()) then { handle_illegal(); return RETIRE_FAIL }; + if illegal_vd_unmasked() then { handle_illegal(); return RETIRE_FAIL }; let 'n = num_elem; let 'm = SEW; @@ -772,7 +772,7 @@ 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_vtype()) | 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; @@ -836,7 +836,7 @@ 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_vtype()) | 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;