Have input_stage set the b operand to imm_data if it is valid
authorMichael Nolan <mtnolan2640@gmail.com>
Fri, 8 May 2020 17:49:27 +0000 (13:49 -0400)
committerMichael Nolan <mtnolan2640@gmail.com>
Fri, 8 May 2020 17:49:27 +0000 (13:49 -0400)
src/soc/alu/formal/proof_input_stage.py
src/soc/alu/input_stage.py

index ab679e01e25352a872398103cbe2639448a25dad..b3fc7f281c4375a5637e855c28428278ea520fcc 100644 (file)
@@ -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)
 
 
 
index f7c38673baf01b44e4469c664ad22fcc38e6a066..6d5e1e46c3ec47a40762331f3bff3b6b9236efc3 100644 (file)
@@ -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)