From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 17 Feb 2020 16:07:47 +0000 (-0500)
Subject: Fix proof crashing instead of giving a vcd
X-Git-Tag: ls180-24jan2020~144
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eaa16ff671a2a4ea884adab62ae1cce86a232872;p=ieee754fpu.git

Fix proof crashing instead of giving a vcd
---

diff --git a/src/ieee754/part_shift/formal/proof_shift_scalar.py b/src/ieee754/part_shift/formal/proof_shift_scalar.py
index 59e66358..8e7b0b68 100644
--- a/src/ieee754/part_shift/formal/proof_shift_scalar.py
+++ b/src/ieee754/part_shift/formal/proof_shift_scalar.py
@@ -69,28 +69,43 @@ class ShifterDriver(Elaboratable):
             with m.Case(0b01):
                 comb += Assert(out[0:8] ==
                                (data[0:8] << (shifter & 0x7)) & 0xFF)
-                comb += Assert(out[8:24] ==
-                               (data[8:24] << (shifter & 0xF)) & 0xffff)
+                # comb += Assert(out[8:16] ==
+                #                (data[8:16] << (shifter)) & 0xffff)
 
             # 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)
-
-            # with m.Case(0b11):
-            #     comb += Assert(out[0:8] ==
-            #                    (data[0:8] << (shifter & 0x7)) & 0xFF)
-            #     comb += Assert(out[8:16] ==
-            #                    (data[8:16] << (shifter & 0x7)) & 0xff)
-            #     comb += Assert(out[16:24] ==
-            #                    (data[16:24] << (shifter & 0x7)) & 0xff)
+                # comb += Assert(out[16:24] ==
+                #                (data[16:24] << (shifter & 0x7)) & 0xff)
+                comb += Assert(out[0:16] ==
+                               (data[0:16] << (shifter & 0xf)) & 0xffff)
+
+            with m.Case(0b11):
+                comb += Assert(out[0:8] ==
+                               (data[0:8] << (shifter & 0x7)) & 0xFF)
+                comb += Assert(out[8:16] ==
+                               (data[8:16] << (shifter & 0x7)) & 0xff)
+                comb += Assert(out[16:24] ==
+                               (data[16:24] << (shifter & 0x7)) & 0xff)
         return m
 
 class PartitionedScalarShiftTestCase(FHDLTestCase):
     def test_shift(self):
         module = ShifterDriver()
         self.assertFormal(module, mode="bmc", depth=4)
+    def test_ilang(self):
+        width = 32
+        mwidth = 4
+        gates = Signal(mwidth-1)
+        points = PartitionPoints()
+        step = int(width/mwidth)
+        for i in range(mwidth-1):
+            points[(i+1)*step] = gates[i]
+        print(points)
+        dut = PartitionedScalarShift(width, points)
+        vl = rtlil.convert(dut, ports=[gates, dut.data,
+                                       dut.shifter,
+                                       dut.output])
+        with open("scalar_shift.il", "w") as f:
+            f.write(vl)
 
 if __name__ == "__main__":
     unittest.main()
diff --git a/src/ieee754/part_shift/part_shift_scalar.py b/src/ieee754/part_shift/part_shift_scalar.py
index 2fe37f81..43d16bdb 100644
--- a/src/ieee754/part_shift/part_shift_scalar.py
+++ b/src/ieee754/part_shift/part_shift_scalar.py
@@ -32,9 +32,9 @@ class PartitionedScalarShift(Elaboratable):
         m = Module()
         comb = m.d.comb
         width = self.width
+        pwid = self.partition_points.get_max_partition_count(width)-1
         shiftbits = self.shiftbits
         shifted = Signal(self.data.width)
-        pwid = self.partition_points.get_max_partition_count(width)-1
         gates = self.partition_points.as_sig()
         comb += shifted.eq(self.data << self.shifter)
 
@@ -44,33 +44,37 @@ class PartitionedScalarShift(Elaboratable):
         intervals = []
         keys = list(self.partition_points.keys()) + [self.width]
         start = 0
-
-        shifter_masks = []
         for i in range(len(keys)):
             end = keys[i]
             parts.append(self.data[start:end])
             outputs.append(self.output[start:end])
             intervals.append((start,end))
-            start = end
+            start = end  # for next time round loop
 
         min_bits = math.ceil(math.log2(intervals[0][1] - intervals[0][0]))
-        for i in range(len(keys)):
+        shifter_masks = []
+        for i in range(len(intervals)):
             max_bits = math.ceil(math.log2(width-intervals[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])
-            shifter_masks.append(sm.mask)
+            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)
+            else: # having a 0 width signal seems to give the proof issues
+                shifter_masks.append((1<<min_bits)-1)
+        print(m.submodules)
 
-        start = 0
-        for i in range(len(keys)):
-            end = keys[i]
-            sp = Signal(width)
-            _shifter = Signal(shiftbits, name="shifter%d" % i)
+        for i, interval in enumerate(intervals):
+            s,e = interval
+            sp = Signal(width, name="sp%d" % i)
+            _shifter = Signal(self.shifter.width, name="shifter%d" % i)
             comb += _shifter.eq(self.shifter & shifter_masks[i])
-            comb += sp[start:].eq(self.data[start:end] << _shifter)
+            comb += sp[s:].eq(self.data[s:e] << _shifter)
             shiftparts.append(sp)
 
-            start = end  # for next time round loop
 
         for i, interval in enumerate(intervals):
             start, end = interval