formal proof of OP_EXTSWSLI

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 21ce002fa415a02a9024ecd5ffe9ba3bdd73f3f2..582c674504a244bad68efcbf1a7005d42aa6f7cf 100644 (file)
--- a/src/soc/fu/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py
@@ -75,6 +75,7 @@ class Driver(Elaboratable):
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):
 
+            # left-shift: 64/32-bit
             with m.Case(MicrOp.OP_SHL):
                 comb += Assume(ra == 0)
                 with m.If(rec.is_32bit):
@@ -83,6 +84,7 @@ class Driver(Elaboratable):
                 with m.Else():
                     comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1)))
 
+            # right-shift: 64/32-bit / signed
             with m.Case(MicrOp.OP_SHR):
                 comb += Assume(ra == 0)
                 with m.If(~rec.is_signed):
@@ -97,6 +99,19 @@ class Driver(Elaboratable):
                         comb += Assert(o[32:64] == Repl(a[31], 32))
                     with m.Else():
                         comb += Assert(o == (a_signed >> b[0:7]))
+
+            # extswsli: 32/64-bit moded
+            with m.Case(MicrOp.OP_EXTSWSLI):
+                comb += Assume(ra == 0)
+                with m.If(rec.is_32bit):
+                    comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
+                    comb += Assert(o[32:64] == 0)
+                with m.Else():
+                    # sign-extend to 64 bit
+                    a_s = Signal(64, reset_less=True)
+                    comb += a_s.eq(exts(a, 32, 64))
+                    comb += Assert(o == ((a_s << b[0:7]) & ((1 << 64)-1)))
+
             #TODO
             with m.Case(MicrOp.OP_RLC):
                 pass
@@ -104,19 +119,6 @@ class Driver(Elaboratable):
                 pass
             with m.Case(MicrOp.OP_RLCL):
                 pass
-            with m.Case(MicrOp.OP_EXTSWSLI):
-                # sign-extend
-                a_s = Signal(64, reset_less=True)
-                comb += a_s.eq(exts(a, 32, 64))
-                # assume b[0:6] is sh
-                comb += Assume(b[7:] == 0)
-                with m.If(b[0:7] == 0):
-                    comb += Assert(o[0:32] == a_s[0:32])
-                with m.Else():
-                    #b_s = 64-b[0:6]
-                    #comb += Assert(o == ((a_s << b_s) & ((1 << 64)-1)))
-                    pass
-
             with m.Default():
                 comb += o_ok.eq(0)
 

diff --git a/src/soc/fu/shift_rot/test/test_pipe_caller.py b/src/soc/fu/shift_rot/test/test_pipe_caller.py
index ee11bad252aec7366629712ddde1f96e4f6301e4..6e48cb2c22312691a0e11f7b26ef75e858e6cea0 100644 (file)
--- a/src/soc/fu/shift_rot/test/test_pipe_caller.py
+++ b/src/soc/fu/shift_rot/test/test_pipe_caller.py
@@ -156,7 +156,10 @@ class ShiftRotTestCase(FHDLTestCase):
     def test_regression_extswsli_3(self):
         lst = [f"extswsli 3, 1, 0"]
         initial_regs = [0] * 32
-        initial_regs[1] = 0x80000000fb4013e2
+        #initial_regs[1] = 0x80000000fb4013e2
+        #initial_regs[1] = 0xffffffffffffffff
+        #initial_regs[1] = 0x00000000ffffffff
+        initial_regs[1] = 0x0000010180122900
         #initial_regs[1] = 0x3ffffd73f7f19fdd
         self.run_tst_program(Program(lst, bigendian), initial_regs)