Add proof for using the greater than combiner to do equals as well

It works for the active outputs, however some of the active outputs
get set to 1 instead of 0

diff --git a/src/ieee754/part_cmp/experiments/formal/proof_gt.py b/src/ieee754/part_cmp/experiments/formal/proof_gt.py
index 379e89b8c915bfdb49384dced4052f2727cf4e91..691d831707bf54d45451f76b34b0010547093ff7 100644 (file)
--- a/src/ieee754/part_cmp/experiments/formal/proof_gt.py
+++ b/src/ieee754/part_cmp/experiments/formal/proof_gt.py
@@ -2,7 +2,7 @@
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 
 from nmigen import Module, Signal, Elaboratable, Mux
-from nmigen.asserts import Assert, AnyConst
+from nmigen.asserts import Assert, AnyConst, Assume
 from nmigen.test.utils import FHDLTestCase
 from nmigen.cli import rtlil
 
@@ -27,28 +27,56 @@ class CombinerDriver(Elaboratable):
         gts = Signal(width)
         gates = Signal(width-1)
         out = Signal(width)
+        mux_input = Signal()
         comb += [eqs.eq(AnyConst(width)),
-                     gates.eq(AnyConst(width)),
-                     gts.eq(AnyConst(width))]
+                 gates.eq(AnyConst(width)),
+                 gts.eq(AnyConst(width)),
+                 mux_input.eq(AnyConst(1))]
+
 
         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])))))
+
+        # If the mux_input is 0, then this should work exactly as
+        # described in
+        # https://libre-riscv.org/3d_gpu/architecture/dynamic_simd/gt/
+        # except for 2 gate bits, not 3
+        with m.If(mux_input == 0):
+            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])))))
+        # With the mux_input set to 1, this should work similarly to
+        # eq_combiner. It appears this is the case, however the
+        # ungated inputs are not set to 0 like they are in eq
+        with m.Else():
+            for i in range(gts.width):
+                comb += Assume(gts[i] == 0)
+
+            with m.Switch(gates):
+                with m.Case(0b11):
+                    for i in range(out.width):
+                        comb += Assert(out[i] == eqs[i])
+                with m.Case(0b00):
+                    comb += Assert(out[0] == (eqs[0] & eqs[1] & eqs[2]))
+                with m.Case(0b10):
+                    comb += Assert(out[0] == (eqs[0] & eqs[1]))
+                    comb += Assert(out[2] == eqs[2])
+                with m.Case(0b01):
+                    comb += Assert(out[0] == eqs[0])
+                    comb += Assert(out[1] == (eqs[1] & eqs[2]))
 
 
 
@@ -56,6 +84,7 @@ class CombinerDriver(Elaboratable):
         comb += dut.eqs.eq(eqs)
         comb += dut.gts.eq(gts)
         comb += dut.gates.eq(gates)
+        comb += dut.mux_input.eq(mux_input)
         comb += out.eq(dut.outputs)
 
         return m

diff --git a/src/ieee754/part_cmp/experiments/gt_combiner.py b/src/ieee754/part_cmp/experiments/gt_combiner.py
index 5cd2d8c2cdaad4e3134cdefb4732ca8d22762f04..7fd4da2a089b07a01c80b4a46a281eabeb016bc6 100644 (file)
--- a/src/ieee754/part_cmp/experiments/gt_combiner.py
+++ b/src/ieee754/part_cmp/experiments/gt_combiner.py
@@ -14,6 +14,7 @@ from ieee754.part_cmp.experiments.eq_combiner import Twomux
 class GTCombiner(Elaboratable):
     def __init__(self, width):
         self.width = width
+        self.mux_input = Signal(reset_less=True)  # right hand side mux input
         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)
@@ -23,16 +24,16 @@ class GTCombiner(Elaboratable):
         m = Module()
         comb = m.d.comb
 
-        previnput = self.gts[-1]
+        previnput = self.gts[-1] | (self.eqs[-1] & self.mux_input)
         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.inb.eq(self.mux_input)
             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