aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--model/riscv_ext_regs.sail2
-rw-r--r--model/riscv_insts_mext.sail54
-rw-r--r--model/riscv_insts_vext_vset.sail178
-rw-r--r--model/riscv_insts_zbb.sail24
-rw-r--r--model/riscv_insts_zbc.sail6
-rw-r--r--model/riscv_insts_zbkb.sail6
-rw-r--r--model/riscv_insts_zbkx.sail4
-rw-r--r--model/riscv_insts_zicsr.sail2
-rw-r--r--model/riscv_pmp_control.sail43
-rwxr-xr-xmodel/riscv_vreg_type.sail1
10 files changed, 157 insertions, 163 deletions
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 28ed111..efe9bae 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -28,7 +28,7 @@ function ext_rvfi_init () = {
THIS(csrno, priv, isWrite) allows an extension to block access to csrno,
at Privilege level priv. It should return true if the access is allowed.
*/
-val ext_check_CSR : (bits(12), Privilege, bool) -> bool
+val ext_check_CSR : (csreg, Privilege, bool) -> bool
function ext_check_CSR (csrno, p, isWrite) = true
/*!
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index 6bf94ee..d7f9dc7 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -20,11 +20,10 @@ mapping encdec_mul_op : mul_op <-> bits(3) = {
struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> 0b011
}
-mapping clause encdec = MUL(rs2, rs1, rd, mul_op)
- <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011
+mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if haveMulDiv() | haveZmmul()
+ <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if haveMulDiv() | haveZmmul()
function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
- if haveMulDiv() | haveZmmul() then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val);
@@ -35,10 +34,6 @@ function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
else result_wide[(sizeof(xlen) - 1) .. 0];
X(rd) = result;
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping mul_mnemonic : mul_op <-> string = {
@@ -54,11 +49,10 @@ mapping clause assembly = MUL(rs2, rs1, rd, mul_op)
/* ****************************************************************** */
union clause ast = DIV : (regidx, regidx, regidx, bool)
-mapping clause encdec = DIV(rs2, rs1, rd, s)
- <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011
+mapping clause encdec = DIV(rs2, rs1, rd, s) if haveMulDiv()
+ <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
function clause execute (DIV(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -68,10 +62,6 @@ function clause execute (DIV(rs2, rs1, rd, s)) = {
let q': int = if s & q > xlen_max_signed then xlen_min_signed else q;
X(rd) = to_bits(sizeof(xlen), q');
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping maybe_not_u : bool <-> string = {
@@ -85,11 +75,10 @@ mapping clause assembly = DIV(rs2, rs1, rd, s)
/* ****************************************************************** */
union clause ast = REM : (regidx, regidx, regidx, bool)
-mapping clause encdec = REM(rs2, rs1, rd, s)
- <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011
+mapping clause encdec = REM(rs2, rs1, rd, s) if haveMulDiv()
+ <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
function clause execute (REM(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -98,10 +87,6 @@ function clause execute (REM(rs2, rs1, rd, s)) = {
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = to_bits(sizeof(xlen), r);
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = REM(rs2, rs1, rd, s)
@@ -111,12 +96,11 @@ mapping clause assembly = REM(rs2, rs1, rd, s)
union clause ast = MULW : (regidx, regidx, regidx)
mapping clause encdec = MULW(rs2, rs1, rd)
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
<-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
function clause execute (MULW(rs2, rs1, rd)) = {
- if haveMulDiv() | haveZmmul() then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = signed(rs1_val);
@@ -126,10 +110,6 @@ function clause execute (MULW(rs2, rs1, rd)) = {
let result : xlenbits = sign_extend(result32);
X(rd) = result;
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = MULW(rs2, rs1, rd)
@@ -141,12 +121,11 @@ mapping clause assembly = MULW(rs2, rs1, rd)
union clause ast = DIVW : (regidx, regidx, regidx, bool)
mapping clause encdec = DIVW(rs2, rs1, rd, s)
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
function clause execute (DIVW(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -156,10 +135,6 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = {
let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q;
X(rd) = sign_extend(to_bits(32, q'));
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = DIVW(rs2, rs1, rd, s)
@@ -171,12 +146,11 @@ mapping clause assembly = DIVW(rs2, rs1, rd, s)
union clause ast = REMW : (regidx, regidx, regidx, bool)
mapping clause encdec = REMW(rs2, rs1, rd, s)
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
function clause execute (REMW(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -185,10 +159,6 @@ function clause execute (REMW(rs2, rs1, rd, s)) = {
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = sign_extend(to_bits(32, r));
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = REMW(rs2, rs1, rd, s)
diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
index abd5587..40a7ea9 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
+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)
diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail
index c7671a6..d39afc0 100644
--- a/model/riscv_insts_zbb.sail
+++ b/model/riscv_insts_zbb.sail
@@ -184,7 +184,7 @@ mapping clause assembly = RISCV_REV8(rs1, rd)
function clause execute (RISCV_REV8(rs1, rd)) = {
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8)
result[(i + 7) .. i] = rs1_val[(sizeof(xlen) - i - 1) .. (sizeof(xlen) - i - 8)];
X(rd) = result;
@@ -202,7 +202,7 @@ mapping clause assembly = RISCV_ORCB(rs1, rd)
function clause execute (RISCV_ORCB(rs1, rd)) = {
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8)
result[(i + 7) .. i] = if rs1_val[(i + 7) .. i] == zeros()
then 0x00
@@ -222,7 +222,7 @@ mapping clause assembly = RISCV_CPOP(rs1, rd)
function clause execute (RISCV_CPOP(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
+ var result : nat = 0;
foreach (i from 0 to (xlen_val - 1))
if rs1_val[i] == bitone then result = result + 1;
X(rd) = to_bits(sizeof(xlen), result);
@@ -240,7 +240,7 @@ mapping clause assembly = RISCV_CPOPW(rs1, rd)
function clause execute (RISCV_CPOPW(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
+ var result : nat = 0;
foreach (i from 0 to 31)
if rs1_val[i] == bitone then result = result + 1;
X(rd) = to_bits(sizeof(xlen), result);
@@ -258,8 +258,8 @@ mapping clause assembly = RISCV_CLZ(rs1, rd)
function clause execute (RISCV_CLZ(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from (sizeof(xlen) - 1) downto 0)
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
@@ -279,8 +279,8 @@ mapping clause assembly = RISCV_CLZW(rs1, rd)
function clause execute (RISCV_CLZW(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from 31 downto 0)
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
@@ -300,8 +300,8 @@ mapping clause assembly = RISCV_CTZ(rs1, rd)
function clause execute (RISCV_CTZ(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from 0 to (sizeof(xlen) - 1))
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
@@ -321,8 +321,8 @@ mapping clause assembly = RISCV_CTZW(rs1, rd)
function clause execute (RISCV_CTZW(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from 0 to 31)
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
diff --git a/model/riscv_insts_zbc.sail b/model/riscv_insts_zbc.sail
index 910db1b..458b9fa 100644
--- a/model/riscv_insts_zbc.sail
+++ b/model/riscv_insts_zbc.sail
@@ -18,7 +18,7 @@ mapping clause assembly = RISCV_CLMUL(rs2, rs1, rd)
function clause execute (RISCV_CLMUL(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (xlen_val - 1))
if rs2_val[i] == bitone then result = result ^ (rs1_val << i);
X(rd) = result;
@@ -37,7 +37,7 @@ mapping clause assembly = RISCV_CLMULH(rs2, rs1, rd)
function clause execute (RISCV_CLMULH(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (xlen_val - 1))
if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i));
X(rd) = result;
@@ -56,7 +56,7 @@ mapping clause assembly = RISCV_CLMULR(rs2, rs1, rd)
function clause execute (RISCV_CLMULR(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (xlen_val - 1))
if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i - 1));
X(rd) = result;
diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail
index 76190f0..f6246d1 100644
--- a/model/riscv_insts_zbkb.sail
+++ b/model/riscv_insts_zbkb.sail
@@ -64,7 +64,7 @@ mapping clause assembly = RISCV_ZIP(rs1, rd)
function clause execute (RISCV_ZIP(rs1, rd)) = {
assert(sizeof(xlen) == 32);
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
result[i*2] = rs1_val[i];
result[i*2 + 1] = rs1_val[i + sizeof(xlen_bytes)*4];
@@ -85,7 +85,7 @@ mapping clause assembly = RISCV_UNZIP(rs1, rd)
function clause execute (RISCV_UNZIP(rs1, rd)) = {
assert(sizeof(xlen) == 32);
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
result[i] = rs1_val[i*2];
result[i + sizeof(xlen_bytes)*4] = rs1_val[i*2 + 1];
@@ -105,7 +105,7 @@ mapping clause assembly = RISCV_BREV8(rs1, rd)
function clause execute (RISCV_BREV8(rs1, rd)) = {
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8)
result[i+7..i] = reverse(rs1_val[i+7..i]);
X(rd) = result;
diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail
index 59a90c6..d19a2b1 100644
--- a/model/riscv_insts_zbkx.sail
+++ b/model/riscv_insts_zbkx.sail
@@ -18,7 +18,7 @@ mapping clause assembly = RISCV_XPERM8(rs2, rs1, rd)
function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8) {
let index = unsigned(rs2_val[i+7..i]);
result[i+7..i] = if 8*index < sizeof(xlen)
@@ -41,7 +41,7 @@ mapping clause assembly = RISCV_XPERM4(rs2, rs1, rd)
function clause execute (RISCV_XPERM4(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 4) by 4) {
let index = unsigned(rs2_val[i+3..i]);
result[i+3..i] = if 4*index < sizeof(xlen)
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 7c52abd..f2980fb 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -10,7 +10,7 @@
/* This file specifies the instructions in the 'Zicsr' extension. */
/* ****************************************************************** */
-union clause ast = CSR : (bits(12), regidx, regidx, bool, csrop)
+union clause ast = CSR : (csreg, regidx, regidx, bool, csrop)
mapping encdec_csrop : csrop <-> bits(2) = {
CSRRW <-> 0b01,
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 1e4cb77..ce53caf 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -8,19 +8,17 @@
/* address ranges */
-// TODO: handle the 34-bit paddr32 on RV32
+// [min, max) of the matching range, in units of 4 bytes.
+type pmp_addr_range_in_words = option((xlenbits, xlenbits))
-/* [min, max) of the matching range. */
-type pmp_addr_range = option((xlenbits, xlenbits))
-
-function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range = {
+function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range_in_words = {
match pmpAddrMatchType_of_bits(cfg[A]) {
OFF => None(),
- TOR => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) },
+ TOR => { Some ((prev_pmpaddr, pmpaddr)) },
NA4 => {
// NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg().
assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1.");
- let lo = pmpaddr << 2;
+ let lo = pmpaddr;
Some((lo, lo + 4))
},
NAPOT => {
@@ -33,7 +31,7 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
let lo = pmpaddr & (~ (mask));
// mask + 1: 0b00000100000
let len = mask + 1;
- Some((lo << 2, (lo + len) << 2))
+ Some((lo, (lo + len)))
}
}
}
@@ -65,18 +63,27 @@ function pmpCheckPerms(ent, acc, priv) = {
enum pmpAddrMatch = {PMP_NoMatch, PMP_PartialMatch, PMP_Match}
-function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range) -> pmpAddrMatch = {
+function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range_in_words) -> pmpAddrMatch = {
match rng {
None() => PMP_NoMatch,
- Some((lo, hi)) => if hi <=_u lo /* to handle mis-configuration */
- then PMP_NoMatch
- else {
- if (addr + width <=_u lo) | (hi <=_u addr)
- then PMP_NoMatch
- else if (lo <=_u addr) & (addr + width <=_u hi)
- then PMP_Match
- else PMP_PartialMatch
- }
+ Some((lo, hi)) => {
+ // Convert to integers.
+ let addr = unsigned(addr);
+ let width = unsigned(width);
+ // These are in units of 4 bytes.
+ let lo = unsigned(lo) * 4;
+ let hi = unsigned(hi) * 4;
+
+ if hi <= lo /* to handle mis-configuration */
+ then PMP_NoMatch
+ else {
+ if (addr + width <= lo) | (hi <= addr)
+ then PMP_NoMatch
+ else if (lo <= addr) & (addr + width <= hi)
+ then PMP_Match
+ else PMP_PartialMatch
+ }
+ },
}
}
diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail
index a1f292a..2ab211b 100755
--- a/model/riscv_vreg_type.sail
+++ b/model/riscv_vreg_type.sail
@@ -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,
generated by cgit v1.1 at 2024-06-29 03:37:30 +0000