Skip to content

Commit

Permalink
Refactor MUL instruction
Browse files Browse the repository at this point in the history
This instruction had a bit of a case of 'boolean blindness' code smell,
where the mul operation was represented as a triple of booleans. This
commit refactors the implemention to use a struct with named fields for
high, signed_rs1, and signed_rs2.

The C_MUL instruction in Zcb also needs to be changed appropriately

The mul_op struct was added in riscv_types

While there do some housekeeping w.r.t the comment about a workaround for
Sail < 0.15.1, as this is no longer needed.
  • Loading branch information
Alasdair committed May 12, 2024
1 parent 82acf05 commit f852d65
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 34 deletions.
39 changes: 19 additions & 20 deletions model/riscv_insts_mext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -11,27 +11,26 @@

/* ****************************************************************** */

union clause ast = MUL : (regidx, regidx, regidx, bool, bool, bool)
union clause ast = MUL : (regidx, regidx, regidx, mul_op)

mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = {
(false, true, true) <-> 0b000,
(true, true, true) <-> 0b001,
(true, true, false) <-> 0b010,
(true, false, false) <-> 0b011
mapping encdec_mul_op : mul_op <-> bits(3) = {
struct { high = false, signed_rs1 = true, signed_rs2 = true } <-> 0b000,
struct { high = true, signed_rs1 = true, signed_rs2 = true } <-> 0b001,
struct { high = true, signed_rs1 = true, signed_rs2 = false } <-> 0b010,
struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> 0b011
}

/* for some reason the : bits(3) here is still necessary - BUG */
mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2)
<-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011
mapping clause encdec = MUL(rs2, rs1, rd, mul_op)
<-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011

function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = {
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 signed1 then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val);
let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if mul_op.signed_rs2 then signed(rs2_val) else unsigned(rs2_val);
let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int);
let result = if high
let result = if mul_op.high
then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)]
else result_wide[(sizeof(xlen) - 1) .. 0];
X(rd) = result;
Expand All @@ -42,15 +41,15 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = {
}
}

mapping mul_mnemonic : (bool, bool, bool) <-> string = {
(false, true, true) <-> "mul",
(true, true, true) <-> "mulh",
(true, true, false) <-> "mulhsu",
(true, false, false) <-> "mulhu"
mapping mul_mnemonic : mul_op <-> string = {
struct { high = false, signed_rs1 = true, signed_rs2 = true } <-> "mul",
struct { high = true, signed_rs1 = true, signed_rs2 = true } <-> "mulh",
struct { high = true, signed_rs1 = true, signed_rs2 = false } <-> "mulhsu",
struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> "mulhu"
}

mapping clause assembly = MUL(rs2, rs1, rd, high, signed1, signed2)
<-> mul_mnemonic(high, signed1, signed2) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
mapping clause assembly = MUL(rs2, rs1, rd, mul_op)
<-> mul_mnemonic(mul_op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)

/* ****************************************************************** */
union clause ast = DIV : (regidx, regidx, regidx, bool)
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_insts_zcb.sail
Original file line number Diff line number Diff line change
Expand Up @@ -206,5 +206,5 @@ mapping clause assembly = C_MUL(rsdc, rs2c) <->
function clause execute C_MUL(rsdc, rs2c) = {
let rd = creg2reg_idx(rsdc);
let rs = creg2reg_idx(rs2c);
execute(MUL(rs, rd, rd, false, true, true))
execute(MUL(rs, rd, rd, struct { high = false, signed_rs1 = true, signed_rs2 = true }))
}
21 changes: 8 additions & 13 deletions model/riscv_types.sail
Original file line number Diff line number Diff line change
Expand Up @@ -389,6 +389,12 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8} = {
DOUBLE <-> 8,
}

struct mul_op = {
high : bool,
signed_rs1 : bool,
signed_rs2 : bool
}

/*!
* Raise an internal error reporting that width w is invalid for access kind, k,
* and current xlen. The file name and line number should be passed in as the
Expand All @@ -399,17 +405,6 @@ mapping size_bytes : word_width <-> {1, 2, 4, 8} = {
*/
val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a
function report_invalid_width(f , l, w, k) -> 'a = {
/*
* Ideally we would call internal_error here but this triggers a Sail bug,
* https://github.com/rems-project/sail/issues/203 in versions < 0.15.1, so
* we work around this by manually inlining.
* TODO when we are happy to require Sail >= 0.15.1 uncomment the following
* and remove the rest of the function.
*/
// internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
// " with xlen=" ^ dec_str(sizeof(xlen)));
assert (false, f ^ ":" ^ dec_str(l) ^ ": " ^ "Invalid width, "
^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen="
^ dec_str(sizeof(xlen)));
throw Error_internal_error()
internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
" with xlen=" ^ dec_str(sizeof(xlen)))
}

0 comments on commit f852d65

Please sign in to comment.