attempting 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 6346950da5599f0ecd8d6a36d993f52896c864cb..e6e8b7c7ca0d1952a83025abd3495ab26e3fae5a 100644 (file)
--- 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,7 @@ from soc.fu.alu.pipe_data import ALUPipeSpec
 from soc.fu.alu.alu_input_record import CompALUOpSubset
 from soc.decoder.power_enums import MicrOp
 import unittest
+from nmutil.extend import exts
 
 
 # This defines a module to drive the device under test and assert
@@ -47,11 +48,10 @@ class Driver(Elaboratable):
         o = dut.o.o.data
 
         # setup random inputs
-        comb += [a.eq(AnyConst(64)),
-                 b.eq(AnyConst(64)),
-                 carry_in.eq(AnyConst(1)),
-                 carry_in32.eq(AnyConst(1)),
-                 ]
+        comb += a.eq(AnyConst(64))
+        comb += b.eq(AnyConst(64))
+        comb += carry_in.eq(AnyConst(1))
+        comb += carry_in32.eq(AnyConst(1))
 
         comb += dut.i.ctx.op.eq(rec)
 
@@ -104,7 +104,18 @@ class Driver(Elaboratable):
             with m.Case(MicrOp.OP_RLCL):
                 pass
             with m.Case(MicrOp.OP_EXTSWSLI):
-                pass
+                # 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 ec35aaae02ad5cea03d46bd271f3edfa75e176f0..ee11bad252aec7366629712ddde1f96e4f6301e4 100644 (file)
--- a/src/soc/fu/shift_rot/test/test_pipe_caller.py
+++ b/src/soc/fu/shift_rot/test/test_pipe_caller.py
@@ -142,12 +142,24 @@ class ShiftRotTestCase(FHDLTestCase):
         self.run_tst_program(Program(lst, bigendian), initial_regs)
 
     def test_regression_extswsli(self):
-        sh = random.randint(0, 63)
         lst = [f"extswsli 3, 1, 34"]
         initial_regs = [0] * 32
         initial_regs[1] = 0x5678
         self.run_tst_program(Program(lst, bigendian), initial_regs)
 
+    def test_regression_extswsli_2(self):
+        lst = [f"extswsli 3, 1, 7"]
+        initial_regs = [0] * 32
+        initial_regs[1] = 0x3ffffd7377f19fdd
+        self.run_tst_program(Program(lst, bigendian), initial_regs)
+
+    def test_regression_extswsli_3(self):
+        lst = [f"extswsli 3, 1, 0"]
+        initial_regs = [0] * 32
+        initial_regs[1] = 0x80000000fb4013e2
+        #initial_regs[1] = 0x3ffffd73f7f19fdd
+        self.run_tst_program(Program(lst, bigendian), initial_regs)
+
     def test_extswsli(self):
         for i in range(40):
             sh = random.randint(0, 63)