summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--riscv/prelude.sail5
-rw-r--r--riscv/riscv.sail87
-rw-r--r--src/gen_lib/sail_values.lem9
-rw-r--r--src/sail_lib.ml26
4 files changed, 121 insertions, 6 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 754a5cec..ad74434c 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -159,7 +159,7 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
-val int_power = {lem: "pow"} : (int, int) -> int
+val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int
val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real
@@ -252,6 +252,9 @@ val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
overload operator / = {quotient_nat, quotient, quotient_real}
+val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int
+val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int
+
val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int
overload operator % = {modulus}
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))
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 92ef7037..50dacf5e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -69,12 +69,11 @@ let rec replace bs (n : integer) b' = match bs with
let upper n = n
+(* Modulus operation corresponding to quot below -- result
+ has sign of dividend. *)
let hardware_mod (a: integer) (b:integer) : integer =
- if a < 0 && b < 0
- then (abs a) mod (abs b)
- else if (a < 0 && b >= 0)
- then (a mod b) - b
- else a mod b
+ let m = (abs a) mod (abs b) in
+ if a < 0 then ~m else m
(* There are different possible answers for integer divide regarding
rounding behaviour on negative operands. Positive operands always
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 7a8dc88c..4d6e32bc 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -176,6 +176,31 @@ let add_int (x, y) = Big_int.add x y
let sub_int (x, y) = Big_int.sub x y
let mult (x, y) = Big_int.mul x y
let quotient (x, y) = Big_int.div x y
+
+(* Big_int does not provide divide with rounding towards zero so roll
+ our own, assuming that division of positive integers rounds down *)
+let quot_round_zero (x, y) =
+ let posX = Big_int.greater_equal x Big_int.zero in
+ let posY = Big_int.greater_equal y Big_int.zero in
+ let absX = Big_int.abs x in
+ let absY = Big_int.abs y in
+ let q = Big_int.div absX absY in
+ if posX != posY then
+ Big_int.negate q
+ else
+ q
+
+(* The corresponding remainder function for above just respects the sign of x *)
+let rem_round_zero (x, y) =
+ let posX = Big_int.greater_equal x Big_int.zero in
+ let absX = Big_int.abs x in
+ let absY = Big_int.abs y in
+ let r = Big_int.modulus absX absY in
+ if posX then
+ r
+ else
+ Big_int.negate r
+
let modulus (x, y) = Big_int.modulus x y
let negate x = Big_int.negate x
@@ -425,6 +450,7 @@ let round_up x = failwith "round_up" (* Num.big_int_of_num (Num.ceiling_num x) *
let quotient_real (x, y) = Rational.div x y
let mult_real (x, y) = Rational.mul x y (* Num.mult_num x y *)
let real_power (x, y) = failwith "real_power" (* Num.power_num x (Num.num_of_big_int y) *)
+let int_power (x, y) = Big_int.pow_int x (Big_int.to_int y)
let add_real (x, y) = Rational.add x y
let sub_real (x, y) = Rational.sub x y
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 15:38:24 +0000