Add carry_in/carry_out

README.md

@@ -180,8 +180,6 @@ Using ASAP7 as an example:
 
 - No support for signed multipliers. Planning to add this.
 
-- No support for carry in or carry out of adders. Planning to add this.
-
 - No support for clock gating yet.
 
 - Formal verification of multipliers is slow, and gets unbearably slow as

ci/formal.sh

@@ -16,6 +16,14 @@ for PROCESS in ${PROCESSES}; do
 	done
 done
 
+for PROCESS in ${PROCESSES}; do
+	for ADDER in ${ADDERS}; do
+		VERILOG=generated/carry_adder_${PROCESS}_${ADDER}.v
+		vlsi-adder --bits=64 --carry-in --carry-out --algorithm=${ADDER} --tech=${PROCESS} --output=${VERILOG}
+		BITS=64 VERILOG=${VERILOG} PROCESS_VERILOG=verilog/${PROCESS}.v yosys -c formal/carry_adder.tcl
+	done
+done
+
 # Test multipliers
 for PROCESS in ${PROCESSES}; do
 	for ADDER in ${ADDERS}; do

formal/carry_adder.tcl

@@ -0,0 +1,25 @@
+yosys -import
+
+read_verilog -defer gold/carry_adder.v
+chparam -set BITS $::env(BITS) gold_carry_adder
+prep -flatten -top gold_carry_adder
+splitnets -ports
+design -stash gold
+
+read_verilog $::env(VERILOG) $::env(PROCESS_VERILOG)
+prep -flatten -top adder
+splitnets -ports
+design -stash gate
+
+design -copy-from gold -as gold gold_carry_adder
+design -copy-from gate -as gate adder
+equiv_make gold gate equiv
+prep -flatten -top equiv
+
+opt_clean -purge
+#show -prefix equiv-prep -colors 1 -stretch
+
+opt -full
+equiv_simple
+equiv_induct
+equiv_status -assert

gold/carry_adder.v

@@ -0,0 +1,16 @@
+module gold_carry_adder
+#(
+    parameter BITS=64
+) (
+`ifdef USE_POWER_PINS
+    input VPWR,
+    input VGND,
+`endif
+    input [BITS-1:0] a,
+    input [BITS-1:0] b,
+    input carry_in,
+    output [BITS-1:0] o,
+    output carry_out
+);
+    assign {carry_out, o} = a + b + carry_in;
+endmodule

vlsiffra/adder.py

@@ -1,14 +1,27 @@
 import math
 
-from amaranth import Elaboratable, Module, Signal, Const
+from amaranth import Elaboratable, Module, Signal, Cat
 
 
 class AdderFramework(Elaboratable):
-    def __init__(self, bits=64, register_input=False, register_output=False, powered=False):
+    def __init__(self, bits=64, register_input=False, register_output=False,
+                 carry_in=False, carry_out=False, powered=False):
         self.a = Signal(bits)
         self.b = Signal(bits)
         self.o = Signal(bits)
 
+        if carry_in:
+            self._carry_in = True
+            self.carry_in = Signal()
+        else:
+            self._carry_in = False
+
+        if carry_out:
+            self._carry_out = True
+            self.carry_out = Signal()
+        else:
+            self._carry_out = False
+
         if powered:
             self._powered = True
             self.VPWR = Signal()
@@ -41,7 +54,12 @@ def elaborate(self, platform):
         self._p = [Signal() for i in range(self._bits)]
         self._g = [Signal() for i in range(self._bits)]
 
-        for i in range(self._bits):
+        if self._carry_in:
+            self._generate_full_adder(a[0], b[0], self.carry_in, self._p[0], self._g[0])
+        else:
+            self._generate_half_adder(a[0], b[0], self._p[0], self._g[0])
+
+        for i in range(1, self._bits):
             self._generate_half_adder(a[i], b[i], self._p[i], self._g[i])
 
         # We need a copy of p
@@ -50,23 +68,30 @@ def elaborate(self, platform):
             m.d.comb += p_tmp[i].eq(self._p[i])
 
         self._calculate_pg()
+        o = [Signal() for i in range(self._bits)]
 
         # g is the carry out signal. We need to shift it left one bit then
-        # xor it with the sum (ie p_tmp). Since we have a list of 1 bit
-        # signals, just insert a constant zero signal at the head of of the
-        # list to shift g.
-        self._g.insert(0, Const(0))
+        # xor it with the sum (ie p_tmp). This means bit 0 is just p.
+        m.d.comb += o[0].eq(p_tmp[0])
 
-        o = Signal(self._bits)
-        for i in range(self._bits):
-            # This also flattens the list of bits when writing to o
-            self._generate_xor(p_tmp[i], self._g[i], o[i])
+        for i in range(1, self._bits):
+            self._generate_xor(p_tmp[i], self._g[i - 1], o[i])
+
+        if self._carry_out:
+            carry_out = Signal()
+            m.d.comb += carry_out.eq(self._g[self._bits - 1])
+
+            if self._register_output:
+                m.d.sync += self.carry_out.eq(carry_out)
+            else:
+                m.d.comb += self.carry_out.eq(carry_out)
 
         o2 = Signal(self._bits, reset_less=True)
+        # This also flattens the list of bits when writing to o2
         if self._register_output:
-            m.d.sync += o2.eq(o)
+            m.d.sync += o2.eq(Cat(o[n] for n in range(len(o))))
         else:
-            m.d.comb += o2.eq(o)
+            m.d.comb += o2.eq(Cat(o[n] for n in range(len(o))))
 
         m.d.comb += self.o.eq(o2)
         return m

vlsiffra/vlsi-adder

@@ -27,6 +27,12 @@ if __name__ == "__main__":
     parser.add_argument('--algorithm',
                         help='Adder algorithm (brentkung (default), koggestone, hancarlson, inferred)')
 
+    parser.add_argument('--carry-in', action='store_true',
+                        help='Carry in signal')
+
+    parser.add_argument('--carry-out', action='store_true',
+                        help='Carry out signal')
+
     parser.add_argument('--powered', action='store_true',
                         help='Add power pins (eg VPWR/VGND)')
 
@@ -60,10 +66,17 @@ if __name__ == "__main__":
         pass
 
     adder = myadder(bits=args.bits, register_input=args.register_input,
+                    carry_in=args.carry_in, carry_out=args.carry_out,
                     register_output=args.register_output, powered=args.powered)
 
     ports = [adder.a, adder.b, adder.o]
     if args.powered:
         ports.extend([adder.VPWR, adder.VGND])
 
+    if args.carry_in:
+        ports.append(adder.carry_in)
+
+    if args.carry_out:
+        ports.append(adder.carry_out)
+
     args.output.write(verilog.convert(adder, ports=ports, name='adder', strip_internal_attrs=True))