From 197d7abd5ac0d20d6f8cb9732b9223caea52c623 Mon Sep 17 00:00:00 2001 From: Xinlai Wan Date: Wed, 22 Nov 2023 20:43:28 +0800 Subject: [PATCH] Fix the encoding and assembly of vsetvl instruction The implementation of vsetvl and vsetvli are rearranged, and some helper functions are added. --- model/riscv_insts_vext_vset.sail | 178 +++++++++++++++++-------------- model/riscv_vreg_type.sail | 1 - 2 files changed, 98 insertions(+), 81 deletions(-) diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 960036237..57fdef0e8 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -71,60 +71,54 @@ mapping maybe_ma_flag : string <-> bits(1) = { sep() ^ "mu" <-> 0b0 } -/* ****************************** vsetvli & vsetvl ******************************* */ -union clause ast = VSET_TYPE : (vsetop, bits(1), bits(1), bits(3), bits(3), regidx, regidx) +val handle_illegal_vtype : unit -> unit effect {rreg} +function handle_illegal_vtype() = { + /* Note: Implementations can set vill or trap if the vtype setting is not supported. + * TODO: configuration support for both solutions + */ + vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vl = zeros(); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vl <- " ^ BitStr(vl)) +} -mapping encdec_vsetop : vsetop <-> bits(4) ={ - VSETVLI <-> 0b0000, - VSETVL <-> 0b1000 +val calculate_new_vl : (int, int) -> xlenbits +function calculate_new_vl(AVL, VLMAX) = { + /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX) + * TODO: configuration support for either using ceil(AVL / 2) or VLMAX + */ + if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) + else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) + else to_bits(sizeof(xlen), VLMAX) } -mapping clause encdec = VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) if haveVExt() - <-> encdec_vsetop(op) @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt() +/* *********************************** vsetvli *********************************** */ +union clause ast = VSETVLI : (bits(1), bits(1), bits(3), bits(3), regidx, regidx) -function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { - let VLEN_pow = get_vlen_pow(); - let ELEN_pow = get_elen_pow(); +mapping clause encdec = VSETVLI(ma, ta, sew, lmul, rs1, rd) if haveVExt() + <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt() + +function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { 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 */ - match op { - VSETVLI => { - vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul - }, - VSETVL => { - let rs2 : regidx = sew[1 .. 0] @ lmul; - vtype->bits() = X(rs2) - } - }; + vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; - /* check legal SEW and LMUL and calculate VLMAX */ + /* check new SEW and LMUL are legal and calculate VLMAX */ + let VLEN_pow = get_vlen_pow(); + let ELEN_pow = get_elen_pow(); let LMUL_pow_new = get_lmul_pow(); let SEW_pow_new = get_sew_pow(); - if SEW_pow_new > LMUL_pow_new + ELEN_pow then { - /* Note: Implementations can set vill or trap if the vtype setting is not supported. - * TODO: configuration support for both solutions - */ - vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - vl = zeros(); - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); - print_reg("CSR vl <- " ^ BitStr(vl)); - return RETIRE_SUCCESS - }; + if SEW_pow_new > LMUL_pow_new + ELEN_pow then { handle_illegal_vtype(); 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 */ let rs1_val = X(rs1); let AVL = unsigned(rs1_val); - vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) - else to_bits(sizeof(xlen), VLMAX); - /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX) - * TODO: configuration support for either using ceil(AVL / 2) or VLMAX - */ + vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); @@ -133,81 +127,105 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { } 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 { - /* Note: Implementations can set vill or trap if the vtype setting is not supported. - * TODO: configuration support for both solutions - */ - vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - vl = zeros(); - } + if (ratio_pow_new != ratio_pow_ori) then { handle_illegal_vtype(); return RETIRE_SUCCESS } }; - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); - print_reg("CSR vl <- " ^ BitStr(vl)); /* reset vstart to 0 */ vstart = zeros(); + + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vl <- " ^ BitStr(vl)); print_reg("CSR vstart <- " ^ BitStr(vstart)); RETIRE_SUCCESS } -mapping vsettype_mnemonic : vsetop <-> string ={ - VSETVLI <-> "vsetvli", - VSETVL <-> "vsetvli" -} +mapping clause assembly = VSETVLI(ma, ta, sew, lmul, rs1, rd) + <-> "vsetvli" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma) -mapping clause assembly = VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) - <-> vsettype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma) +/* *********************************** vsetvl ************************************ */ +union clause ast = VSETVL : (regidx, regidx, regidx) -/* ********************************* vsetivli ************************************ */ -union clause ast = VSETI_TYPE : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx) +mapping clause encdec = VSETVL(rs2, rs1, rd) if haveVExt() + <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt() -mapping clause encdec = VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) if haveVExt() - <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt() - -function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { - let VLEN_pow = get_vlen_pow(); - let ELEN_pow = get_elen_pow(); +function clause execute VSETVL(rs2, rs1, rd) = { 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 */ - vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + vtype->bits() = X(rs2); - /* check legal SEW and LMUL and calculate VLMAX */ + /* check new SEW and LMUL are legal and calculate VLMAX */ + let VLEN_pow = get_vlen_pow(); + let ELEN_pow = get_elen_pow(); let LMUL_pow_new = get_lmul_pow(); let SEW_pow_new = get_sew_pow(); - if SEW_pow_new > LMUL_pow_new + ELEN_pow then { - /* Note: Implementations can set vill or trap if the vtype setting is not supported. - * TODO: configuration support for both solutions - */ - vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - vl = zeros(); - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); - print_reg("CSR vl <- " ^ BitStr(vl)); - return RETIRE_SUCCESS - }; + if SEW_pow_new > LMUL_pow_new + ELEN_pow then { handle_illegal_vtype(); 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) - else to_bits(sizeof(xlen), VLMAX); - /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX) - * TODO: configuration support for either using ceil(AVL / 2) or VLMAX - */ - X(rd) = vl; + if (rs1 != 0b00000) then { /* normal stripmining */ + let rs1_val = X(rs1); + let AVL = unsigned(rs1_val); + vl = calculate_new_vl(AVL, VLMAX); + X(rd) = 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; + } 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 { handle_illegal_vtype(); return RETIRE_SUCCESS } + }; + + /* reset vstart to 0 */ + vstart = zeros(); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); print_reg("CSR vl <- " ^ BitStr(vl)); + print_reg("CSR vstart <- " ^ BitStr(vstart)); + + RETIRE_SUCCESS +} + +mapping clause assembly = VSETVL(rs2, rs1, rd) + <-> "vsetvl" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + +/* ********************************** vsetivli *********************************** */ +union clause ast = VSETIVLI : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx) + +mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if haveVExt() + <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt() + +function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { + /* set vtype */ + vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + + /* check new SEW and LMUL are legal and calculate VLMAX */ + let VLEN_pow = get_vlen_pow(); + let ELEN_pow = get_elen_pow(); + let LMUL_pow_new = get_lmul_pow(); + let SEW_pow_new = get_sew_pow(); + if SEW_pow_new > LMUL_pow_new + ELEN_pow then { handle_illegal_vtype(); return RETIRE_SUCCESS }; + let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new); + + /* set vl according to VLMAX and AVL */ + let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */ + vl = calculate_new_vl(AVL, VLMAX); + X(rd) = vl; /* reset vstart to 0 */ vstart = zeros(); + + print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vl <- " ^ BitStr(vl)); print_reg("CSR vstart <- " ^ BitStr(vstart)); RETIRE_SUCCESS } -mapping clause assembly = VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) +mapping clause assembly = VSETIVLI(ma, ta, sew, lmul, uimm, rd) <-> "vsetivli" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(uimm) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma) diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail index 6f553757b..f8025b4ec 100755 --- a/model/riscv_vreg_type.sail +++ b/model/riscv_vreg_type.sail @@ -44,7 +44,6 @@ type vreglenbits = bits(vlenmax) /* use the largest possible register length */ type vregtype = vreglenbits /* vector instruction types */ -enum vsetop = { VSETVLI, VSETVL } enum vvfunct6 = { VV_VADD, VV_VSUB, VV_VMINU, VV_VMIN, VV_VMAXU, VV_VMAX, VV_VAND, VV_VOR, VV_VXOR, VV_VRGATHER, VV_VRGATHEREI16, VV_VSADDU, VV_VSADD, VV_VSSUBU, VV_VSSUB, VV_VSLL, VV_VSMUL,