Remove unneeded and gate in gt_combiner

The and gate that forces the lanes that are not the MSB in a partiton
to 0 is no longer needed because reorder_bits ignores those bits.

diff --git a/src/ieee754/part_cmp/formal/proof_gt.py b/src/ieee754/part_cmp/formal/proof_gt.py
index cdf1bb0474e0f42335282607a2f4a2659939dfb1..a64eca0faedce56950115961656ac9b2ceab19f2 100644 (file)
--- a/src/ieee754/part_cmp/formal/proof_gt.py
+++ b/src/ieee754/part_cmp/formal/proof_gt.py
@@ -51,15 +51,11 @@ class CombinerDriver(Elaboratable):
                 with m.Case(0b10):
                     comb += Assert(out[2] == gts[2])
                     comb += Assert(out[1] == (gts[1] | (eqs[1] & gts[0])))
-                    comb += Assert(out[0] == 0)
                 with m.Case(0b01):
                     comb += Assert(out[2] == (gts[2] | (eqs[2] & gts[1])))
-                    comb += Assert(out[1] == 0)
                     comb += Assert(out[0] == gts[0])
                 with m.Case(0b00):
                     comb += Assert(out[2] == (gts[2] | (eqs[2] & (gts[1] | (eqs[1] & gts[0])))))
-                    comb += Assert(out[1] == 0)
-                    comb += Assert(out[0] == 0)
         # With the aux_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
@@ -70,15 +66,11 @@ class CombinerDriver(Elaboratable):
                         comb += Assert(out[i] == eqs[i])
                 with m.Case(0b00):
                     comb += Assert(out[2] == (eqs[0] & eqs[1] & eqs[2]))
-                    comb += Assert(out[1] == 0)
-                    comb += Assert(out[0] == 0)
                 with m.Case(0b10):
-                    comb += Assert(out[0] == 0)
                     comb += Assert(out[1] == (eqs[0] & eqs[1]))
                     comb += Assert(out[2] == eqs[2])
                 with m.Case(0b01):
                     comb += Assert(out[0] == eqs[0])
-                    comb += Assert(out[1] == 0)
                     comb += Assert(out[2] == (eqs[1] & eqs[2]))
 
 

diff --git a/src/ieee754/part_cmp/gt_combiner.py b/src/ieee754/part_cmp/gt_combiner.py
index 419a48598e1f1b5351691a0820e361f89302a01d..2828cd16d1311f63ac0b8cf7e9e72b7345efb65d 100644 (file)
--- a/src/ieee754/part_cmp/gt_combiner.py
+++ b/src/ieee754/part_cmp/gt_combiner.py
@@ -15,7 +15,7 @@ class Combiner(Elaboratable):
         comb = m.d.comb
 
         comb += self.outa.eq(Mux(self.sel, self.inb, self.ina))
-        comb += self.outb.eq(self.sel & self.ina)
+        comb += self.outb.eq(self.ina)
 
         return m