Add M extension to RISCV. Slightly inelegant implementation for now but passing tests.

1 files changed, 4 insertions, 5 deletions

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