From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 20 May 2020 13:52:05 +0000 (-0400)
Subject: Add 32 bit carry handling to alu
X-Git-Tag: div_pipeline~1041
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=48306a1eb31536b154342b34b8db2b82f229a0d9;p=soc.git

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 601a4875..33c97809 100644
--- 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 fb0ed939..b2b2612a 100644
--- 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 935e272f..4f682f67 100644
--- 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)