Fix bug in shift_rot, update proof to handle new interface

diff --git a/src/soc/shift_rot/formal/proof_main_stage.py b/src/soc/shift_rot/formal/proof_main_stage.py
index 2cb2b0d161a2ae6b31573fbd89eef1c3370f3d4b..50264d5c33d2f73078f13e45cd46e6381a62fe79 100644 (file)
--- a/src/soc/shift_rot/formal/proof_main_stage.py
+++ b/src/soc/shift_rot/formal/proof_main_stage.py
@@ -37,8 +37,9 @@ class Driver(Elaboratable):
         m.submodules.dut = dut = ShiftRotMainStage(pspec)
 
         # convenience variables
-        a = dut.i.a
-        b = dut.i.b
+        a = dut.i.rs
+        b = dut.i.rb
+        ra = dut.i.ra
         carry_in = dut.i.carry_in
         so_in = dut.i.so
         carry_out = dut.o.carry_out
@@ -67,12 +68,14 @@ class Driver(Elaboratable):
         # main assertion of arithmetic operations
         with m.Switch(rec.insn_type):
             with m.Case(InternalOp.OP_SHL):
+                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():
                     comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1)))
             with m.Case(InternalOp.OP_SHR):
+                comb += Assume(ra == 0)
                 with m.If(~rec.is_signed):
                     with m.If(rec.is_32bit):
                         comb += Assert(o[0:32] == (a[0:32] >> b[0:6]))

diff --git a/src/soc/shift_rot/rotator.py b/src/soc/shift_rot/rotator.py
index b695a4e12146dcc96f7fc8a441c441569bb17fb5..60694729a184ca187573acec783551fb9ccacb02 100644 (file)
--- a/src/soc/shift_rot/rotator.py
+++ b/src/soc/shift_rot/rotator.py
@@ -122,7 +122,7 @@ class Rotator(Elaboratable):
             comb += me.eq(Cat(self.mb, self.mb_extra, Const(0b0, 1)))
         with m.Else():
             # effectively, 63 - sh
-            comb += me.eq(Cat(~self.shift[0:6], self.shift[6]))
+            comb += me.eq(Cat(~sh[0:6], sh[6]))
 
         # Calculate left and right masks
         comb += mr.eq(right_mask(m, mb))

diff --git a/src/soc/shift_rot/test/test_pipe_caller.py b/src/soc/shift_rot/test/test_pipe_caller.py
index e1ca7fc5e122585a87dc806a0d2b85ca821abb50..97df2f20d59343b191119c185199451430dfd3eb 100644 (file)
--- a/src/soc/shift_rot/test/test_pipe_caller.py
+++ b/src/soc/shift_rot/test/test_pipe_caller.py
@@ -123,11 +123,12 @@ class ALUTestCase(FHDLTestCase):
         self.run_tst_program(Program(lst), initial_regs)
 
     def test_shift_once(self):
-        lst = ["sraw 3, 1, 2"]
+        lst = ["slw 3, 1, 4",
+               "slw 3, 1, 2"]
         initial_regs = [0] * 32
-        initial_regs[1] = 0xdeadbeefcafec0de
-        initial_regs[2] = 53
-        print(initial_regs[1], initial_regs[2])
+        initial_regs[1] = 0x80000000
+        initial_regs[2] = 0x40
+        initial_regs[4] = 0x00
         self.run_tst_program(Program(lst), initial_regs)
 
     def test_rlwinm(self):