aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_insts_vext_vset.sail
diff options
context:
space:
mode:
Diffstat (limited to 'model/riscv_insts_vext_vset.sail')
-rw-r--r--model/riscv_insts_vext_vset.sail178
1 files changed, 98 insertions, 80 deletions
diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
index abd5587..000b2f3 100644
--- a/model/riscv_insts_vext_vset.sail
+++ b/model/riscv_insts_vext_vset.sail
@@ -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)));
@@ -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)
generated by cgit v1.1 at 2024-11-05 13:24:19 +0000