From 939c409c32e7a522edeb4879d14c30a4efb6b2f8 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Fri, 8 May 2020 13:49:27 -0400 Subject: [PATCH] Have input_stage set the b operand to imm_data if it is valid --- src/soc/alu/formal/proof_input_stage.py | 6 +++++- src/soc/alu/input_stage.py | 6 +++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/soc/alu/formal/proof_input_stage.py b/src/soc/alu/formal/proof_input_stage.py index ab679e01..b3fc7f28 100644 --- a/src/soc/alu/formal/proof_input_stage.py +++ b/src/soc/alu/formal/proof_input_stage.py @@ -56,7 +56,11 @@ class Driver(Elaboratable): comb += Assert(dut.o.a == ~a) with m.Else(): comb += Assert(dut.o.a == a) - comb += Assert(dut.o.b == b) + + with m.If(rec.imm_data.imm_ok): + comb += Assert(dut.o.b == rec.imm_data.imm) + with m.Else(): + comb += Assert(dut.o.b == b) diff --git a/src/soc/alu/input_stage.py b/src/soc/alu/input_stage.py index f7c38673..6d5e1e46 100644 --- a/src/soc/alu/input_stage.py +++ b/src/soc/alu/input_stage.py @@ -28,7 +28,11 @@ class ALUInputStage(PipeModBase): comb += self.o.a.eq(a) - comb += self.o.b.eq(self.i.b) + # If there's an immediate, set the B operand to that + with m.If(self.i.ctx.op.imm_data.imm_ok): + comb += self.o.b.eq(self.i.ctx.op.imm_data.imm) + with m.Else(): + comb += self.o.b.eq(self.i.b) comb += self.o.ctx.eq(self.i.ctx) -- 2.30.2