Fix proof_input_stage.py

diff --git a/src/soc/alu/formal/proof_input_stage.py b/src/soc/alu/formal/proof_input_stage.py
index b3fc7f281c4375a5637e855c28428278ea520fcc..bb62fb67c5a392c824e8afaf8b97e90723d88377 100644 (file)
--- a/src/soc/alu/formal/proof_input_stage.py
+++ b/src/soc/alu/formal/proof_input_stage.py
@@ -9,6 +9,7 @@ from nmigen.cli import rtlil
 from soc.alu.input_stage import ALUInputStage
 from soc.alu.pipe_data import ALUPipeSpec
 from soc.alu.alu_input_record import CompALUOpSubset
+from soc.decoder.power_enums import InternalOp
 import unittest
 
 
@@ -57,7 +58,8 @@ class Driver(Elaboratable):
         with m.Else():
             comb += Assert(dut.o.a == a)
 
-        with m.If(rec.imm_data.imm_ok):
+        with m.If(rec.imm_data.imm_ok &
+                  ~(rec.insn_type == InternalOp.OP_RLC)):
             comb += Assert(dut.o.b == rec.imm_data.imm)
         with m.Else():
             comb += Assert(dut.o.b == b)