Skip to content

Commit

Permalink
Merge pull request #359 from XinlaiWan/master
Browse files Browse the repository at this point in the history 
Fix the encoding and assembly of `vsetvl` instruction
  • Loading branch information
@billmcspadden-riscv
billmcspadden-riscv authored May 16, 2024
2 parents be1e04c + 8ab3ca8 commit 3688e5b
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 @@ -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
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

0 comments on commit 3688e5b

Please sign in to comment.