add formal proof for OP_RLCL

[soc.git] / src / soc / fu / shift_rot / formal / proof_main_stage.py

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 576a1658021d2d5fdbd578263d85ff62cf0a3dc5..ebfab28c824afca05310ca7e793207b5eb90b647 100644 (file)
--- 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