Add carry in and out

diff --git a/src/soc/alu/formal/proof_main_stage.py b/src/soc/alu/formal/proof_main_stage.py
index 4b7da69b0b47c15a51719b6479455b199a8d584a..372cf99338102a926cf86191a77dd935dcb19890 100644 (file)
--- a/src/soc/alu/formal/proof_main_stage.py
+++ b/src/soc/alu/formal/proof_main_stage.py
@@ -1,7 +1,7 @@
 # Proof of correctness for partitioned equal signal combiner
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 
-from nmigen import Module, Signal, Elaboratable, Mux
+from nmigen import Module, Signal, Elaboratable, Mux, Cat
 from nmigen.asserts import Assert, AnyConst, Assume, Cover
 from nmigen.test.utils import FHDLTestCase
 from nmigen.cli import rtlil
@@ -37,10 +37,16 @@ class Driver(Elaboratable):
 
         a = Signal(64)
         b = Signal(64)
+        carry_in = Signal(64)
+        so_in = Signal(64)
         comb += [dut.i.a.eq(a),
                  dut.i.b.eq(b),
+                 dut.i.carry_in.eq(carry_in),
+                 dut.i.so.eq(so_in),
                  a.eq(AnyConst(64)),
-                 b.eq(AnyConst(64))]
+                 b.eq(AnyConst(64)),
+                 carry_in.eq(AnyConst(1)),
+                 so_in.eq(AnyConst(1))]
                       
 
         comb += dut.i.ctx.op.eq(rec)
@@ -54,7 +60,8 @@ class Driver(Elaboratable):
             comb += Assert(dut_sig == rec_sig)
 
         with m.If(rec.insn_type == InternalOp.OP_ADD):
-            comb += Assert(dut.o.o == (a + b) & ((1<<64)-1))
+            comb += Assert(Cat(dut.o.o, dut.o.carry_out) ==
+                           (a + b + carry_in))
 
 
         return m

diff --git a/src/soc/alu/main_stage.py b/src/soc/alu/main_stage.py
index ee8234515a5ace12cbba79328c39781264ead618..d443e9777476a8b608cae760289fe0c4255fa777 100644 (file)
--- a/src/soc/alu/main_stage.py
+++ b/src/soc/alu/main_stage.py
@@ -20,12 +20,14 @@ class ALUMainStage(PipeModBase):
         comb = m.d.comb
 
         add_output = Signal(self.i.a.width + 1, reset_less=True)
-        comb += add_output.eq(self.i.a + self.i.b)
+        comb += add_output.eq(self.i.a + self.i.b + self.i.carry_in)
 
 
         with m.Switch(self.i.ctx.op.insn_type):
             with m.Case(InternalOp.OP_ADD):
                 comb += self.o.o.eq(add_output[0:64])
+                comb += self.o.carry_out.eq(add_output[64])
+
 
         comb += self.o.ctx.eq(self.i.ctx)