Begin adding partitioned scalar shifter

diff --git a/src/ieee754/part_shift_scalar/formal/.gitignore b/src/ieee754/part_shift_scalar/formal/.gitignore
new file mode 100644 (file)
index 0000000..37ad79e
--- /dev/null
+++ b/src/ieee754/part_shift_scalar/formal/.gitignore
@@ -0,0 +1 @@
+proof_*/**

diff --git a/src/ieee754/part_shift_scalar/formal/proof_shift_scalar.py b/src/ieee754/part_shift_scalar/formal/proof_shift_scalar.py
new file mode 100644 (file)
index 0000000..780c48b
--- /dev/null
+++ b/src/ieee754/part_shift_scalar/formal/proof_shift_scalar.py
@@ -0,0 +1,80 @@
+# Proof of correctness for partitioned scalar shifter
+# Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+
+from nmigen import Module, Signal, Elaboratable, Mux, Cat
+from nmigen.asserts import Assert, AnyConst, Assume
+from nmigen.test.utils import FHDLTestCase
+from nmigen.cli import rtlil
+
+from ieee754.part_mul_add.partpoints import PartitionPoints
+from ieee754.part_shift_scalar.part_shift_scalar import PartitionedScalarShift
+import unittest
+
+
+# This defines a module to drive the device under test and assert
+# properties about its outputs
+class ShifterDriver(Elaboratable):
+    def __init__(self):
+        # inputs and outputs
+        pass
+
+    def get_intervals(self, signal, points):
+        start = 0
+        interval = []
+        keys = list(points.keys()) + [signal.width]
+        for key in keys:
+            end = key
+            interval.append(signal[start:end])
+            start = end
+        return interval
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+        width = 24
+        shifterwidth = 5
+        mwidth = 3
+
+        # setup the inputs and outputs of the DUT as anyconst
+        data = Signal(width)
+        out = Signal(width)
+        shifter = Signal(shifterwidth)
+        points = PartitionPoints()
+        gates = Signal(mwidth-1)
+        step = int(width/mwidth)
+        for i in range(mwidth-1):
+            points[(i+1)*step] = gates[i]
+        print(points)
+
+        comb += [data.eq(AnyConst(width)),
+                 shifter.eq(AnyConst(shifterwidth)),
+                 gates.eq(AnyConst(mwidth-1))]
+
+        m.submodules.dut = dut = PartitionedScalarShift(width, points)
+
+        data_intervals = self.get_intervals(data, points)
+        out_intervals = self.get_intervals(out, points)
+
+        comb += [dut.data.eq(data),
+                 dut.shifter.eq(shifter),
+                 out.eq(dut.output)]
+
+        expected = Signal(width)
+        comb += expected.eq(data << shifter)
+
+        with m.Switch(points.as_sig()):
+            with m.Case(0b00):
+                comb += Assert(out[0:8] == expected[0:8])
+                comb += Assert(out[8:16] == expected[8:16])
+
+        
+        return m
+
+class PartitionedScalarShiftTestCase(FHDLTestCase):
+    def test_shift(self):
+        module = ShifterDriver()
+        self.assertFormal(module, mode="bmc", depth=4)
+
+if __name__ == "__main__":
+    unittest.main()
+

diff --git a/src/ieee754/part_shift_scalar/part_shift_scalar.py b/src/ieee754/part_shift_scalar/part_shift_scalar.py
new file mode 100644 (file)
index 0000000..13ae564
--- /dev/null
+++ b/src/ieee754/part_shift_scalar/part_shift_scalar.py
@@ -0,0 +1,45 @@
+# SPDX-License-Identifier: LGPL-2.1-or-later
+# See Notices.txt for copyright information
+
+"""
+Copyright (C) 2020 Luke Kenneth Casson Leighton <lkcl@lkcl.net>
+Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+
+dynamically-partitionable "comparison" class, directly equivalent
+to Signal.__eq__, __gt__ and __ge__, except SIMD-partitionable
+
+See:
+
+* http://libre-riscv.org/3d_gpu/architecture/dynamic_simd/shift/
+* http://bugs.libre-riscv.org/show_bug.cgi?id=173
+"""
+from nmigen import Signal, Module, Elaboratable, Cat, C
+from ieee754.part_mul_add.partpoints import PartitionPoints
+import math
+
+
+class PartitionedScalarShift(Elaboratable):
+    def __init__(self, width, partition_points):
+        self.width = width
+        self.partition_points = PartitionPoints(partition_points)
+
+        self.data = Signal(width)
+        self.shiftbits = math.ceil(math.log2(width))
+        self.shifter = Signal(self.shiftbits)
+        self.output = Signal(width)
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+        width = self.width
+        shiftbits = self.shiftbits
+
+        shifted = Signal(self.data.width)
+        comb += shifted.eq(self.data << self.shifter)
+
+        comb += self.output[0:8].eq(shifted[0:8])
+        comb += self.output[8:16].eq(shifted[8:16])
+
+        return m
+        
+