[otbn] Fix possible overflow in BN.SUBM
This was triggered by comments on commit 840e329 (a similar fix for
BN.ADDM). As specced before, you'd get an overflow if wrs1 = 0 and
wrs2 > 2**255 because the result would have a zero top bit when
truncated to 256 bits.
Since we're not using the borrow at all here, I've changed the
spec (and ISS code) to be more explicit, showing the subtraction and
testing whether the result is less than zero.
Note that the detailed behaviour depends on the fact that our negative
numbers are 2's-complement (in the case that the intermediate result
is less than -MOD), so I've made sure to say so explicitly in the
spec change.
Signed-off-by: Rupert Swarbrick <rswarbrick@lowrisc.org>
diff --git a/hw/ip/otbn/data/bignum-insns.yml b/hw/ip/otbn/data/bignum-insns.yml
index c2af187..551241b 100644
--- a/hw/ip/otbn/data/bignum-insns.yml
+++ b/hw/ip/otbn/data/bignum-insns.yml
@@ -453,21 +453,27 @@
synopsis: Pseudo-modulo subtraction
operands: [wrd, wrs1, wrs2]
doc: |
- Subtracts the second WDR value from the first WDR value, performs a modulo operation with the MOD WSR, and writes the result to the destination WDR.
- This operation is equivalent to a modulo subtraction as long as `wrs1 - wrs2 >= -MOD` holds.
- This constraint is not checked in hardware.
+ Subtract `<wrs2>` from `<wrs1>`, modulo the `MOD` WSR.
+
+ The intermediate result is treated as a signed number (of width `WLEN + 1`).
+ If it is negative, `MOD` is added to it.
+ The 2's-complement result is then truncated to 256 bits and stored in `<wrd>`.
+
+ This operation correctly implements subtraction modulo `MOD`, providing that the intermediate result at least `-MOD` and at most `MOD - 1`.
+ This is guaranteed if both inputs are less than `MOD`.
+
Flags are not used or saved.
decode: |
d = UInt(wrd)
a = UInt(wrs1)
b = UInt(wrs2)
operation: |
- (result, ) = SubtractWithBorrow(a, b, 0)
+ result = a - b
if result < 0:
result = MOD + result
- WDR[d] = result
+ WDR[d] = result & ((1 << 256) - 1)
encoding:
scheme: bnam
mapping:
diff --git a/hw/ip/otbn/dv/otbnsim/sim/insn.py b/hw/ip/otbn/dv/otbnsim/sim/insn.py
index d290b63..d25bcd4 100644
--- a/hw/ip/otbn/dv/otbnsim/sim/insn.py
+++ b/hw/ip/otbn/dv/otbnsim/sim/insn.py
@@ -599,18 +599,13 @@
a = state.wdrs.get_reg(self.wrs1).read_unsigned()
b = state.wdrs.get_reg(self.wrs2).read_unsigned()
- (ures, _) = state.sub_with_borrow(a, b, 0)
-
mod_val = state.wsrs.MOD.read_unsigned()
- # sub_with_borrow returns an unsigned result (in 2's complement), so
- # the result is negative if the top bit is set.
- is_negative = bool(ures >> 255)
- if is_negative:
- result = (ures + mod_val) & ((1 << 256) - 1)
- else:
- result = ures
+ diff = a - b
+ if diff < 0:
+ diff += mod_val
+ result = diff & ((1 << 256) - 1)
state.wdrs.get_reg(self.wrd).write_unsigned(result)
