From: Michael Nolan <mtnolan2640@gmail.com>
Date: Thu, 14 May 2020 14:35:44 +0000 (-0400)
Subject: Fix bug in shift_rot, update proof to handle new interface
X-Git-Tag: div_pipeline~1236
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a1f49befd9b61093c4b8017fe7ba1242022b4c90;p=soc.git

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 2cb2b0d1..50264d5c 100644
--- 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 b695a4e1..60694729 100644
--- 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 e1ca7fc5..97df2f20 100644
--- 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):