From: Jacob Lifshay <programmerjake@gmail.com>
Date: Thu, 24 Feb 2022 03:12:49 +0000 (-0800)
Subject: add formal proof for OP_RLCR
X-Git-Url: https://git.libre-soc.org/?p=soc.git;a=commitdiff_plain;h=de7c129d52e01a3b21b7cf02fcf69c9e5bee241a

add formal proof for OP_RLCR
---

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 ebfab28c..8c755e6a 100644
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -481,7 +481,25 @@ class Driver(Elaboratable):
         m.d.comb += Assert(dut.o.xer_ca.data == 0)
 
     def _check_rlcr(self, m, dut):
-        raise NotImplementedError
+        m.d.comb += Assume(~dut.i.ctx.op.is_32bit)
+        # rldicr and rldcr
+
+        m.d.comb += Assume(~dut.i.ctx.op.is_signed)
+        m.d.comb += Assume(dut.i.ra == 0)
+
+        m.submodules.mask = mask = Mask()
+        m.d.comb += mask.start.eq(0)
+        me = dut.fields.FormMD.me[:]
+        m.d.comb += mask.end.eq(Cat(me[1:6], me[0]))
+
+        rot = Signal(64)
+        m.d.comb += rot.eq(rotl64(dut.i.rs, dut.i.rb[:6]))
+
+        expected = Signal(64)
+        m.d.comb += expected.eq(rot & mask.out)
+
+        m.d.comb += Assert(dut.o.o.data == expected)
+        m.d.comb += Assert(dut.o.xer_ca.data == 0)
 
     def _check_extswsli(self, m, dut):
         m.d.comb += Assume(dut.i.ra == 0)