From 0afd17e56d5dec3b5f1ab1b6d47ab7847efbc055 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 11 May 2020 10:33:08 -0400 Subject: [PATCH] Fix proof_input_stage.py --- src/soc/alu/formal/proof_input_stage.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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) -- 2.30.2