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

add formal proof for OP_RLCL
---

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 576a1658..ebfab28c 100644
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -460,7 +460,25 @@ class Driver(Elaboratable):
         m.d.comb += Assert(dut.o.xer_ca.data == 0)
 
     def _check_rlcl(self, m, dut):
-        raise NotImplementedError
+        m.d.comb += Assume(~dut.i.ctx.op.is_32bit)
+        # rldicl and rldcl
+
+        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.end.eq(63)
+        mb = dut.fields.FormMD.mb[:]
+        m.d.comb += mask.start.eq(Cat(mb[1:6], mb[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_rlcr(self, m, dut):
         raise NotImplementedError