Fix bug introduced in rebase
authorMichael Nolan <mtnolan2640@gmail.com>
Wed, 20 May 2020 17:11:18 +0000 (13:11 -0400)
committerMichael Nolan <mtnolan2640@gmail.com>
Wed, 20 May 2020 17:11:39 +0000 (13:11 -0400)
src/soc/fu/alu/formal/proof_main_stage.py

index 91aaac5bfb21cb7d93022164b615936f81a7fa1f..960342ce4d5ec100c004c658a1d33b995e54c4f0 100644 (file)
@@ -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]: