From 4b596f43d794f128d23a687d65d4b05aedf2711b Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Fri, 8 May 2020 13:52:30 -0400 Subject: [PATCH] Add carry in and out --- src/soc/alu/formal/proof_main_stage.py | 13 ++++++++++--- src/soc/alu/main_stage.py | 4 +++- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/soc/alu/formal/proof_main_stage.py b/src/soc/alu/formal/proof_main_stage.py index 4b7da69b..372cf993 100644 --- 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 -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 ee823451..d443e977 100644 --- 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) -- 2.30.2