From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 11 May 2020 14:33:08 +0000 (-0400)
Subject: Fix proof_input_stage.py
X-Git-Tag: div_pipeline~1282
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0afd17e56d5dec3b5f1ab1b6d47ab7847efbc055;p=soc.git

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 b3fc7f28..bb62fb67 100644
--- 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)