Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix the encoding and assembly of vsetvl instruction #359

Merged
merged 3 commits into from
May 16, 2024
Merged

Fix the encoding and assembly of vsetvl instruction #359

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9692f84
Rewrite the implementation of vsetvli and vsetvl instructions to fix …
XinlaiWan Nov 22, 2023
6605792
Merge branch 'master' into master
XinlaiWan Apr 17, 2024
8ab3ca8
Merge branch 'master' into master
billmcspadden-riscv May 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
178 changes: 98 additions & 80 deletions model/riscv_insts_vext_vset.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,60 +41,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 @@ -103,81 +97,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
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,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
Loading