From bac3a07250026743e1521154d9dc82ddacbcb825 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Fri, 8 May 2020 11:09:40 -0400 Subject: [PATCH] Add handling of A inversion and B input --- src/soc/alu/formal/proof_input_stage.py | 19 ++++++++++++++++++- src/soc/alu/input_stage.py | 11 +++++++++++ 2 files changed, 29 insertions(+), 1 deletion(-) diff --git a/src/soc/alu/formal/proof_input_stage.py b/src/soc/alu/formal/proof_input_stage.py index faf68e07..22cd52bf 100644 --- a/src/soc/alu/formal/proof_input_stage.py +++ b/src/soc/alu/formal/proof_input_stage.py @@ -26,20 +26,37 @@ class Driver(Elaboratable): pspec = ALUPipeSpec() m.submodules.dut = dut = ALUInputStage(pspec) + a = Signal(64) + b = Signal(64) + comb += [dut.i.a.eq(a), + dut.i.b.eq(b), + a.eq(AnyConst(64)), + b.eq(AnyConst(64))] + + # Setup random inputs for dut.op rec = CompALUOpSubset() - for p in rec.ports(): width = p.width comb += p.eq(AnyConst(width)) comb += dut.i.op.eq(rec) + + # Assert that op gets copied from the input to output for p in rec.ports(): name = p.name rec_sig = p dut_sig = getattr(dut.o.op, name) comb += Assert(dut_sig == rec_sig) + with m.If(rec.invert_a): + comb += Assert(dut.o.a == ~a) + with m.Else(): + comb += Assert(dut.o.a == a) + comb += Assert(dut.o.b == b) + + + return m diff --git a/src/soc/alu/input_stage.py b/src/soc/alu/input_stage.py index 5bcff4f2..ccf00301 100644 --- a/src/soc/alu/input_stage.py +++ b/src/soc/alu/input_stage.py @@ -20,4 +20,15 @@ class ALUInputStage(PipeModBase): comb += self.o.op.eq(self.i.op) + a = Signal.like(self.i.a) + + with m.If(self.i.op.invert_a): + comb += a.eq(~self.i.a) + with m.Else(): + comb += a.eq(self.i.a) + + comb += self.o.a.eq(a) + + comb += self.o.b.eq(self.i.b) + return m -- 2.30.2