[otbn] Relax assertion for blanking of Adder Y
For `BN.SUBM` with `a >= b` (thus the result of Adder X has the carry
bit set), the result of Adder Y is not used, but it cannot be blanked
solely based on the carry bit (see issue #14603).
This commit relaxes the assertion that checks the blanking of Adder Y to
allow this case, and thereby fixes #14603.
Signed-off-by: Andreas Kurth <adk@lowrisc.org>
diff --git a/hw/ip/otbn/rtl/otbn_alu_bignum.sv b/hw/ip/otbn/rtl/otbn_alu_bignum.sv
index 3298975..d679494 100644
--- a/hw/ip/otbn/rtl/otbn_alu_bignum.sv
+++ b/hw/ip/otbn/rtl/otbn_alu_bignum.sv
@@ -858,8 +858,12 @@
!expected_adder_y_op_shifter_en |-> adder_y_op_shifter_res_blanked == '0,
clk_i, !rst_ni)
+ // Adder Y must be blanked when its result is not used, with one exception: For `BN.SUBM` with
+ // `a >= b` (thus the result of Adder X has the carry bit set), the result of Adder Y is not used
+ // but it cannot be blanked solely based on the carry bit.
`ASSERT(BlankingBignumAluYResUsed_A,
- !adder_y_res_used |-> {x_res_operand_a_mux_out, adder_y_op_b} == '0,
+ !adder_y_res_used && !(operation_i.op == AluOpBignumSubm && adder_x_res[WLEN+1])
+ |-> {x_res_operand_a_mux_out, adder_y_op_b} == '0,
clk_i, !rst_ni)
// shifter_res related blanking
