Add 32 bit carry handling to alu

diff --git a/src/soc/fu/alu/formal/proof_main_stage.py b/src/soc/fu/alu/formal/proof_main_stage.py
index 601a487576e39d9da2682095818b6773ef544b42..33c97809ff074c9bd674043da05807b97137b302 100644 (file)
--- a/src/soc/fu/alu/formal/proof_main_stage.py
+++ b/src/soc/fu/alu/formal/proof_main_stage.py
@@ -41,7 +41,8 @@ class Driver(Elaboratable):
         b = dut.i.b
         carry_in = dut.i.carry_in
         so_in = dut.i.so
-        carry_out = dut.o.carry_out
+        carry_out = dut.o.xer_co.data[0]
+        carry_out32 = dut.o.xer_co.data[1]
         o = dut.o.o
 
         # setup random inputs
@@ -64,11 +65,18 @@ class Driver(Elaboratable):
         comb += a_signed.eq(a)
         comb += a_signed_32.eq(a[0:32])
 
+        comb += Assume(a[32:64] == 0)
+        comb += Assume(b[32:64] == 0)
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):
             with m.Case(InternalOp.OP_ADD):
+                
                 comb += Assert(Cat(o, carry_out) == (a + b + carry_in))
 
+                # CA32
+                comb += Assert((a[0:32] + b[0:32] + carry_in)[32]
+                               == carry_out32)
+
         return m
 
 

diff --git a/src/soc/fu/alu/main_stage.py b/src/soc/fu/alu/main_stage.py
index fb0ed9396fa19f7e5f9b44457999b034fc9809bb..b2b2612a18443506390bb71b25268759157fe1b1 100644 (file)
--- a/src/soc/fu/alu/main_stage.py
+++ b/src/soc/fu/alu/main_stage.py
@@ -62,9 +62,10 @@ class ALUMainStage(PipeModBase):
                 comb += o.eq(add_output[1:-1])
                 comb += carry_out.data[0].eq(add_output[-1]) # XER.CO
 
-                # XXX no!  wrongggg, see microwatt OP_ADD code
+                # see microwatt OP_ADD code
                 # https://bugs.libre-soc.org/show_bug.cgi?id=319#c5
-                comb += carry_out.data[1].eq(add_output[-1]) # XER.CO32
+                comb += carry_out.data[1].eq(add_output[33] ^
+                                             (a[32] ^ b[32])) # XER.CO32
 
             #### exts (sign-extend) ####
             with m.Case(InternalOp.OP_EXTS):

diff --git a/src/soc/fu/alu/test/test_pipe_caller.py b/src/soc/fu/alu/test/test_pipe_caller.py
index 935e272fc6534de7b077dec969463e000f91ca6b..4f682f6751373ebd1d3dfef00cd4f8ae04a1baa5 100644 (file)
--- a/src/soc/fu/alu/test/test_pipe_caller.py
+++ b/src/soc/fu/alu/test/test_pipe_caller.py
@@ -267,7 +267,7 @@ class TestRunner(FHDLTestCase):
             self.assertEqual(expected_carry, real_carry, code)
             expected_carry32 = 1 if sim.spr['XER'][XER_bits['CA32']] else 0
             real_carry32 = yield alu.n.data_o.xer_co.data[1] # XXX CO32
-            self.assertEqual(expected_carry, real_carry, code)
+            self.assertEqual(expected_carry32, real_carry32, code)