From e2c9cea3781da372bed293b67264cd62bb0c5439 Mon Sep 17 00:00:00 2001
From: Michael Nolan <mtnolan2640@gmail.com>
Date: Mon, 3 Feb 2020 15:00:53 -0500
Subject: [PATCH] Add tree-based greater than experiment

---
 .../part_cmp/experiments/formal/proof_gt.py   | 75 +++++++++++++++++++
 .../part_cmp/experiments/gt_combiner.py       | 41 ++++++++++
 2 files changed, 116 insertions(+)
 create mode 100644 src/ieee754/part_cmp/experiments/formal/proof_gt.py
 create mode 100644 src/ieee754/part_cmp/experiments/gt_combiner.py

diff --git a/src/ieee754/part_cmp/experiments/formal/proof_gt.py b/src/ieee754/part_cmp/experiments/formal/proof_gt.py
new file mode 100644
index 00000000..379e89b8
--- /dev/null
+++ b/src/ieee754/part_cmp/experiments/formal/proof_gt.py
@@ -0,0 +1,75 @@
+# Proof of correctness for partitioned equal signal combiner
+# Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
+
+from nmigen import Module, Signal, Elaboratable, Mux
+from nmigen.asserts import Assert, AnyConst
+from nmigen.test.utils import FHDLTestCase
+from nmigen.cli import rtlil
+
+from ieee754.part_cmp.experiments.gt_combiner import GTCombiner
+import unittest
+
+
+# This defines a module to drive the device under test and assert
+# properties about its outputs
+class CombinerDriver(Elaboratable):
+    def __init__(self):
+        # inputs and outputs
+        pass
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+        width = 3
+
+        # setup the inputs and outputs of the DUT as anyconst
+        eqs = Signal(width)
+        gts = Signal(width)
+        gates = Signal(width-1)
+        out = Signal(width)
+        comb += [eqs.eq(AnyConst(width)),
+                     gates.eq(AnyConst(width)),
+                     gts.eq(AnyConst(width))]
+
+        m.submodules.dut = dut = GTCombiner(width)
+
+        with m.Switch(gates):
+            with m.Case(0b11):
+                for i in range(out.width):
+                    comb += Assert(out[i] == gts[i])
+            with m.Case(0b10):
+                comb += Assert(out[2] == gts[2])
+                comb += Assert(out[1] == 0)
+                comb += Assert(out[0] == (gts[0] | (eqs[0] & gts[1])))
+            with m.Case(0b01):
+                comb += Assert(out[2] == 0)
+                comb += Assert(out[1] == (gts[1] | (eqs[1] & gts[2])))
+                comb += Assert(out[0] == gts[0])
+            with m.Case(0b00):
+                comb += Assert(out[2] == 0)
+                comb += Assert(out[1] == 0)
+                comb += Assert(out[0] == (gts[0] | (eqs[0] & (gts[1] | (eqs[1] & gts[2])))))
+
+
+
+        # connect up the inputs and outputs.
+        comb += dut.eqs.eq(eqs)
+        comb += dut.gts.eq(gts)
+        comb += dut.gates.eq(gates)
+        comb += out.eq(dut.outputs)
+
+        return m
+
+class GTCombinerTestCase(FHDLTestCase):
+    def test_gt_combiner(self):
+        module = CombinerDriver()
+        self.assertFormal(module, mode="bmc", depth=4)
+    def test_ilang(self):
+        dut = GTCombiner(3)
+        vl = rtlil.convert(dut, ports=dut.ports())
+        with open("partition_combiner.il", "w") as f:
+            f.write(vl)
+
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/src/ieee754/part_cmp/experiments/gt_combiner.py b/src/ieee754/part_cmp/experiments/gt_combiner.py
new file mode 100644
index 00000000..5cd2d8c2
--- /dev/null
+++ b/src/ieee754/part_cmp/experiments/gt_combiner.py
@@ -0,0 +1,41 @@
+from nmigen import Signal, Module, Elaboratable, Mux
+from ieee754.part_mul_add.partpoints import PartitionPoints
+from ieee754.part_cmp.experiments.eq_combiner import Twomux
+
+
+# This is similar to EQCombiner, except that for a greater than
+# comparison, it needs to deal with both the greater than and equals
+# signals from each partition. The signals are combined using a
+# cascaded AND/OR to give the following effect:
+# When a partition is open, the output is set if either the current
+# partition's greater than flag is set, or the current partition's
+# equal flag is set AND the previous partition's greater than output
+# is true
+class GTCombiner(Elaboratable):
+    def __init__(self, width):
+        self.width = width
+        self.eqs = Signal(width, reset_less=True) # the flags for EQ
+        self.gts = Signal(width, reset_less=True) # the flags for GT
+        self.gates = Signal(width-1, reset_less=True)
+        self.outputs = Signal(width, reset_less=True)
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+
+        previnput = self.gts[-1]
+        for i in range(self.width-1, 0, -1): # counts down from width-1 to 1
+            m.submodules["mux{}".format(i)] = mux = Twomux()
+
+            comb += mux.ina.eq(previnput)
+            comb += mux.inb.eq(0)
+            comb += mux.sel.eq(self.gates[i-1])
+            comb += self.outputs[i].eq(mux.outb)
+            previnput =  self.gts[i-1] | (self.eqs[i-1] & mux.outa)
+        
+        comb += self.outputs[0].eq(previnput)
+
+        return m
+
+    def ports(self):
+        return [self.eqs, self.gts, self.gates, self.outputs]
-- 
2.30.2