1 files changed, 87 insertions, 0 deletions
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index a29f68f3..fc9c4d77 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -252,6 +252,93 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) =
   wGPR(rd, EXTS(result))
 
 /* ****************************************************************** */
+
+union clause ast = MUL : (regbits, regbits, regbits, bool, bool, bool)
+
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd, false,  true, true))  /* MUL */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b001 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true,  true, true))  /* MULH */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true,  true, false)) /* MULHSU */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0110011 = Some(MUL(rs2, rs1, rd,  true, false, false)) /* MULHU */
+function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val) in
+  let result128 = to_bits(128, rs1_int * rs2_int) in
+  let result = if high then result128[127..64] else result128[63..0] in
+  wGPR(rd, result)
+
+/* ****************************************************************** */
+
+union clause ast = DIV : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd,  true))  /* DIV */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0110011 = Some(DIV(rs2, rs1, rd, false))  /* DIVU */
+function clause execute (DIV(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in
+  let q': int = if s & q > (2 ^ 63 - 1) then  (0 - 2^63) else q in /* check for signed overflow */
+  wGPR(rd, to_bits(64, q'))
+
+/* ****************************************************************** */
+
+union clause ast = REM : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd,  true))  /* REM */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0110011 = Some(REM(rs2, rs1, rd, false))  /* REMU */
+function clause execute (REM(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1) in
+  let rs2_val = rGPR(rs2) in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in
+  /* signed overflow case returns zero naturally as required due to -1 divisor */
+  wGPR(rd, to_bits(64, r))
+
+/* ****************************************************************** */
+
+union clause ast = MULW : (regbits, regbits, regbits)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b000 @ rd : regbits @ 0b0111011 = Some(MULW(rs2, rs1, rd)) /* MULW */
+function clause execute (MULW(rs2, rs1, rd)) =
+  let rs1_val = rGPR(rs1)[31..0] in
+  let rs2_val = rGPR(rs2)[31..0] in
+  let rs1_int : int = signed(rs1_val) in
+  let rs2_int : int = signed(rs2_val) in
+  let result32 = to_bits(64, rs1_int * rs2_int)[31..0] in /* XXX surprising behaviour of to_bits requires exapnsion to 64 bits followed by truncation... */
+  let result64 : regval = EXTS(result32) in
+  wGPR(rd, result64)
+
+/* ****************************************************************** */
+
+union clause ast = DIVW : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b100 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd,  true))  /* DIVW */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0111011 = Some(DIVW(rs2, rs1, rd, false))  /* DIVUW */
+function clause execute (DIVW(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1)[31..0] in
+  let rs2_val = rGPR(rs2)[31..0] in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in
+  let q': int = if s & q > (2 ^ 31 - 1) then  (0 - 2^31) else q in /* check for signed overflow */
+  wGPR(rd, EXTS(to_bits(32, q')))
+
+/* ****************************************************************** */
+
+union clause ast = REMW : (regbits, regbits, regbits, bool)
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd,  true))  /* REMW */
+function clause decode 0b0000001 @ rs2 : regbits @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b0111011 = Some(REMW(rs2, rs1, rd, false))  /* REMUW */
+function clause execute (REMW(rs2, rs1, rd, s)) =
+  let rs1_val = rGPR(rs1)[31..0] in
+  let rs2_val = rGPR(rs2)[31..0] in
+  let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in
+  let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in
+  let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in
+  /* signed overflow case returns zero naturally as required due to -1 divisor */
+  wGPR(rd, EXTS(to_bits(32, r)))
+
+/* ****************************************************************** */
+
 union clause ast = FENCE : (bits(4), bits(4))
 
 function clause decode 0b0000 @ pred : bits(4) @ succ : bits(4) @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111 = Some(FENCE(pred, succ))