Refactor MUL instruction

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.

3 files changed, 28 insertions, 34 deletions

diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index c1da229..6bf94ee 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -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;
@@ -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)
diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail
index 1320736..86253bf 100644
--- a/model/riscv_insts_zcb.sail
+++ b/model/riscv_insts_zcb.sail
@@ -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 }))
 }
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index e9a5a19..2b1c132 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -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
@@ -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)))
 }