Fix bug introduced in rebase

[soc.git] / src / soc / fu / alu / formal / proof_main_stage.py

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 91aaac5bfb21cb7d93022164b615936f81a7fa1f..960342ce4d5ec100c004c658a1d33b995e54c4f0 100644 (file)
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -75,7 +75,7 @@ class Driver(Elaboratable):
                 comb += Assert(Cat(o, carry_out) == (a + b + carry_in))
 
                 # CA32 - XXX note this fails! replace with carry_in and it works
-                comb += Assert((a[0:32] + b[0:32] + carry_in32)[32]
+                comb += Assert((a[0:32] + b[0:32] + carry_in)[32]
                                == carry_out32)
             with m.Case(InternalOp.OP_EXTS):
                 for i in [1, 2, 4]: