Skip to content

Commit

Permalink
Rewrite the implementation of vsetvli and vsetvl instructions to fix #…
Browse files Browse the repository at this point in the history 
…337

The issue shows that the encoding and assembly definitions of vsetvl and vsetvli are incorrectly mixed together,
but they actually differ a lot and therefore cannot have a unified definition as the old implementation did,
so this section has been rewritten to split their definitions and executions.
And because these instructions have similar functional behavior after the decoding stage,
some common code is further extracted to be helper functions in this commit.
  • Loading branch information
@XinlaiWan
XinlaiWan committed Nov 28, 2023
1 parent 9f4cad6 commit 9692f84
Show file tree
Hide file tree
Showing 2 changed files with 98 additions and 81 deletions.
178 changes: 98 additions & 80 deletions model/riscv_insts_vext_vset.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)));
Expand All @@ -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)
1 change: 0 additions & 1 deletion model/riscv_vreg_type.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down

0 comments on commit 9692f84

Please sign in to comment.