From be18a2965b96e3a42b6f70071eb20ea899a0bb79 Mon Sep 17 00:00:00 2001 From: Anton Blanchard Date: Wed, 21 Sep 2022 14:41:19 +1000 Subject: [PATCH 1/2] adder: Add carry_in/carry_out Signed-off-by: Anton Blanchard --- README.md | 2 -- ci/formal.sh | 8 ++++++++ formal/carry_adder.tcl | 25 +++++++++++++++++++++++++ gold/carry_adder.v | 16 ++++++++++++++++ vlsiffra/adder.py | 31 +++++++++++++++++++++++++++++-- vlsiffra/vlsi-adder | 13 +++++++++++++ 6 files changed, 91 insertions(+), 4 deletions(-) create mode 100644 formal/carry_adder.tcl create mode 100644 gold/carry_adder.v diff --git a/README.md b/README.md index 0eb1ee1..7a440d4 100644 --- a/README.md +++ b/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 diff --git a/ci/formal.sh b/ci/formal.sh index 8eca6ce..0b4d62c 100755 --- a/ci/formal.sh +++ b/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 diff --git a/formal/carry_adder.tcl b/formal/carry_adder.tcl new file mode 100644 index 0000000..26a4956 --- /dev/null +++ b/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 diff --git a/gold/carry_adder.v b/gold/carry_adder.v new file mode 100644 index 0000000..b4ff318 --- /dev/null +++ b/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 diff --git a/vlsiffra/adder.py b/vlsiffra/adder.py index 1906ac6..8cb2d88 100644 --- a/vlsiffra/adder.py +++ b/vlsiffra/adder.py @@ -4,11 +4,24 @@ 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 @@ -62,6 +80,15 @@ def elaborate(self, platform): # This also flattens the list of bits when writing to o self._generate_xor(p_tmp[i], self._g[i], o[i]) + if self._carry_out: + carry_out = Signal() + m.d.comb += carry_out.eq(self._g[self._bits]) + + 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) if self._register_output: m.d.sync += o2.eq(o) diff --git a/vlsiffra/vlsi-adder b/vlsiffra/vlsi-adder index 6bc088b..668c922 100644 --- a/vlsiffra/vlsi-adder +++ b/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)) From 3508dbca4c147f53b30c4d15e737638ff7f6563f Mon Sep 17 00:00:00 2001 From: Anton Blanchard Date: Wed, 21 Sep 2022 15:11:51 +1000 Subject: [PATCH 2/2] adder: Remove unnecessary xor of lowest bit Mikey noticed the lowest bit of the adder has an xor with 0. To fix this, we have to move the flattening of the array of signals later. Signed-off-by: Anton Blanchard --- vlsiffra/adder.py | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/vlsiffra/adder.py b/vlsiffra/adder.py index 8cb2d88..dd972dc 100644 --- a/vlsiffra/adder.py +++ b/vlsiffra/adder.py @@ -1,6 +1,6 @@ import math -from amaranth import Elaboratable, Module, Signal, Const +from amaranth import Elaboratable, Module, Signal, Cat class AdderFramework(Elaboratable): @@ -68,21 +68,18 @@ 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]) + m.d.comb += carry_out.eq(self._g[self._bits - 1]) if self._register_output: m.d.sync += self.carry_out.eq(carry_out) @@ -90,10 +87,11 @@ def elaborate(self, platform): 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