part_shift_scalar now has maked shift amounts working

diff --git a/src/ieee754/part_shift/formal/proof_shift_scalar.py b/src/ieee754/part_shift/formal/proof_shift_scalar.py
index 8e7b0b682b8e39d2bb0356af9b9b8300dfde46f0..b150e25b716c04859a07fa09c0c16aa9477c651d 100644 (file)
--- a/src/ieee754/part_shift/formal/proof_shift_scalar.py
+++ b/src/ieee754/part_shift/formal/proof_shift_scalar.py
@@ -62,19 +62,19 @@ class ShifterDriver(Elaboratable):
         expected = Signal(width)
 
         with m.Switch(points.as_sig()):
-            # with m.Case(0b00):
-            #     comb += Assert(
-            #         out[0:24] == (data[0:24] << (shifter & 0x1f)) & 0xffffff)
+            with m.Case(0b00):
+                comb += Assert(
+                    out[0:24] == (data[0:24] << (shifter & 0x1f)) & 0xffffff)
 
             with m.Case(0b01):
                 comb += Assert(out[0:8] ==
                                (data[0:8] << (shifter & 0x7)) & 0xFF)
-                # comb += Assert(out[8:16] ==
-                #                (data[8:16] << (shifter)) & 0xffff)
+                comb += Assert(out[8:24] ==
+                               (data[8:24] << (shifter & 0xf)) & 0xffff)
 
-            # with m.Case(0b10):
-                # comb += Assert(out[16:24] ==
-                #                (data[16:24] << (shifter & 0x7)) & 0xff)
+            with m.Case(0b10):
+                comb += Assert(out[16:24] ==
+                               (data[16:24] << (shifter & 0x7)) & 0xff)
                 comb += Assert(out[0:16] ==
                                (data[0:16] << (shifter & 0xf)) & 0xffff)
 
@@ -92,8 +92,8 @@ class PartitionedScalarShiftTestCase(FHDLTestCase):
         module = ShifterDriver()
         self.assertFormal(module, mode="bmc", depth=4)
     def test_ilang(self):
-        width = 32
-        mwidth = 4
+        width = 24
+        mwidth = 3
         gates = Signal(mwidth-1)
         points = PartitionPoints()
         step = int(width/mwidth)

diff --git a/src/ieee754/part_shift/part_shift_scalar.py b/src/ieee754/part_shift/part_shift_scalar.py
index 43d16bdb5fb21c352c86a6e3a8970a1c9d1a8e49..eb155df746300cfe63a956f27dc4c4448656dcd0 100644 (file)
--- a/src/ieee754/part_shift/part_shift_scalar.py
+++ b/src/ieee754/part_shift/part_shift_scalar.py
@@ -55,17 +55,24 @@ class PartitionedScalarShift(Elaboratable):
         shifter_masks = []
         for i in range(len(intervals)):
             max_bits = math.ceil(math.log2(width-intervals[i][0]))
+            sm_mask = Signal(shiftbits, name="sm_mask%d" % i)
             if pwid-i != 0:
                 sm = ShifterMask(pwid-i, shiftbits,
                                  max_bits, min_bits)
-                setattr(m.submodules, "sm%d" % i, sm)
                 comb += sm.gates.eq(gates[i:pwid])
-                mask = Signal(shiftbits, name="sm_mask%d" % i)
-                comb += mask.eq(sm.mask)
-                shifter_masks.append(mask)
+                comb += sm_mask.eq(sm.mask)
+                setattr(m.submodules, "sm%d" % i, sm)
             else: # having a 0 width signal seems to give the proof issues
-                shifter_masks.append((1<<min_bits)-1)
-        print(m.submodules)
+                # this seems to fix it
+                comb += sm_mask.eq((1<<min_bits)-1)
+            if i != 0:
+                shifter_mask = Signal(shiftbits, name="shifter_mask%d" % i)
+                comb += shifter_mask.eq(Mux(gates[i-1],
+                                         sm_mask,
+                                         shifter_masks[i-1]))
+                shifter_masks.append(shifter_mask)
+            else:
+                shifter_masks.append(sm_mask)
 
         for i, interval in enumerate(intervals):
             s,e = interval