diff options
Diffstat (limited to 'src/gen_lib/sail_values.lem')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 4fded5a1..38f7d512 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -257,12 +257,16 @@ let hardware_mod (a: integer) (b:integer) : integer = then (a mod b) - b else a mod b +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) let hardware_quot (a:integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) / (abs b) - else if (a < 0 && b > 0) - then (a/b) + 1 - else a/b + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) let quot_signed = hardware_quot |