From 2ad42f91f4f13d6e57f76b17dc93785381d32066 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 2 Feb 2018 16:59:22 +0000
Subject: Add M extension to RISCV. Slightly inelegant implementation for now
 but passing tests.

---
 src/gen_lib/sail_values.lem | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'src/gen_lib')

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
-- 
cgit v1.2.3