WIP: check MB > ME and select mask appropriately

diff --git a/src/soc/fu/shift_rot/formal/proof_main_stage.py b/src/soc/fu/shift_rot/formal/proof_main_stage.py
index fa1674f3826d62d7fed1029034eed31f255aeeb1..2f0455f48bc1ba048eef3ee444a1804e6fb9a9ee 100644 (file)
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -185,7 +185,10 @@ class Driver(Elaboratable):
                 # code norms.
 
                 mrl = Signal(64, reset_less=True, name='MASK_FOR_RLC')
-                comb += mrl.eq(ml | mr)
+                with m.If(mb > me):
+                    comb += mrl.eq(ml | mr)
+                with m.Else():
+                    comb += mrl.eq(ml & mr)
 
                 ainp = Signal(64, reset_less=True, name='A_INP_FOR_RLC')
                 comb += ainp.eq(field(a, 32, 63))