From 0c721b4a8af4d144e6ddcaae833c194540c30950 Mon Sep 17 00:00:00 2001
From: "Samuel A. Falvo II" <kc5tja@arrl.net>
Date: Thu, 30 Jul 2020 16:18:49 -0700
Subject: [PATCH] WIP: rlwinm/rlwnm/rlwimi-type proofs

Been trying to wittle away at this for several days now, without luck.
What am I missing?!
---
 .../fu/shift_rot/formal/proof_main_stage.py   | 44 ++++++++++++++++++-
 1 file changed, 42 insertions(+), 2 deletions(-)

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 c45c875d..168bf2c2 100644
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -16,6 +16,8 @@ from soc.fu.shift_rot.rotator import right_mask, left_mask
 from soc.fu.shift_rot.pipe_data import ShiftRotPipeSpec
 from soc.fu.shift_rot.sr_input_record import CompSROpSubset
 from soc.decoder.power_enums import MicrOp
+from soc.consts import field
+
 import unittest
 from nmutil.extend import exts
 
@@ -151,9 +153,47 @@ class Driver(Elaboratable):
                     comb += a_s.eq(exts(a, 32, 64))
                     comb += Assert(o == ((a_s << b[0:7]) & ((1 << 64)-1)))
 
-            #TODO
+            # rlwinm, rlwnm, rlwimi
+            # *CAN* these even be 64-bit capable?  I don't think they are.
             with m.Case(MicrOp.OP_RLC):
-                pass
+                comb += Assume(ra == 0)
+                
+                # Duplicate some signals so that they're much easier to find in gtkwave.
+                # Pro-tip: when debugging, factor out expressions into explicitly named
+                # signals, and search using a unique grep-tag (RLC in my case).  After
+                # debugging, resubstitute values to taste.
+
+                mrl = Signal(32, reset_less=True, name='MASK_FOR_RLC')
+                comb += mrl.eq(ml & mr)
+
+                ainp = Signal(32, reset_less=True, name='A_INP_FOR_RLC')
+                comb += ainp.eq(field(a, 32, 63))
+
+                sh = Signal(6, reset_less=True, name='SH_FOR_RLC')
+                comb += sh.eq(b[0:6])
+
+                exp_shl = Signal(32, reset_less=True, name='A_SHIFTED_LEFT_BY_SH_FOR_RLC')
+                comb += exp_shl.eq((ainp << sh) & 0xFFFFFFFF)
+
+                exp_shr = Signal(32, reset_less=True, name='A_SHIFTED_RIGHT_FOR_RLC')
+                comb += exp_shr.eq((ainp >> (32 - sh)) & 0xFFFFFFFF)
+
+                exp_ol = Signal(32, reset_less=True, name='EXPECTED_OL_FOR_RLC')
+                comb += exp_ol.eq(((exp_shl | exp_shr) & mrl) | (ainp & ~mrl))
+
+                # If I uncomment the following lines, I can confirm that all
+                # 32-bit rotations work.  If I uncomment only one of the
+                # following lines, I can confirm that all 32-bit rotations
+                # work.  When I remove/recomment BOTH lines, however, the
+                # assertion fails.  Why??
+
+#               comb += Assume(mr == 0xFFFFFFFF)
+#               comb += Assume(ml == 0xFFFFFFFF)
+                with m.If(rec.is_32bit):
+                    comb += Assert(field(o, 32, 63) == exp_ol)
+                    comb += Assert(field(o, 0, 31) == 0)
+
+            #TODO
             with m.Case(MicrOp.OP_RLCR):
                 pass
             with m.Case(MicrOp.OP_RLCL):
-- 
2.30.2