Add a signal to disable the gt inputs to gt_combiner

diff --git a/src/ieee754/part_cmp/experiments/formal/proof_gt.py b/src/ieee754/part_cmp/experiments/formal/proof_gt.py
index c0fb998e21a19f6b2bed8bed54629a213ed10f58..923fcf901abf215d46ee70315cd6d440dab59a4f 100644 (file)
--- a/src/ieee754/part_cmp/experiments/formal/proof_gt.py
+++ b/src/ieee754/part_cmp/experiments/formal/proof_gt.py
@@ -27,21 +27,23 @@ class CombinerDriver(Elaboratable):
         gts = Signal(width)
         gates = Signal(width-1)
         out = Signal(width)
-        mux_input = Signal()
+        aux_input = Signal()
+        gt_en = Signal()
         comb += [eqs.eq(AnyConst(width)),
                  gates.eq(AnyConst(width)),
                  gts.eq(AnyConst(width)),
-                 mux_input.eq(AnyConst(1))]
+                 aux_input.eq(AnyConst(1)),
+                 gt_en.eq(AnyConst(1))]
 
 
         m.submodules.dut = dut = GTCombiner(width)
 
 
-        # If the mux_input is 0, then this should work exactly as
+        # If the aux_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.If((aux_input == 0) & (gt_en == 1)):
             with m.Switch(gates):
                 with m.Case(0b11):
                     for i in range(out.width):
@@ -58,13 +60,10 @@ class CombinerDriver(Elaboratable):
                     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
+        # 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
-        with m.Else():
-            for i in range(gts.width):
-                comb += Assume(gts[i] == 0)
-
+        with m.Elif((aux_input == 1) & (gt_en == 0)):
             with m.Switch(gates):
                 with m.Case(0b11):
                     for i in range(out.width):
@@ -88,7 +87,8 @@ 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 += dut.aux_input.eq(aux_input)
+        comb += dut.gt_en.eq(gt_en)
         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 8be22dec3963d4eeb72d04c005149f6bee49e9b2..0ca8e84f1addaff2aa37a238d63f1dbf29583ac0 100644 (file)
--- a/src/ieee754/part_cmp/experiments/gt_combiner.py
+++ b/src/ieee754/part_cmp/experiments/gt_combiner.py
@@ -32,7 +32,8 @@ class GTCombiner(Elaboratable):
 
     def __init__(self, width):
         self.width = width
-        self.mux_input = Signal(reset_less=True)  # right hand side mux input
+        self.aux_input = Signal(reset_less=True)  # right hand side mux input
+        self.gt_en = Signal(reset_less=True)      # enable or disable the gt signal
         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)
@@ -42,16 +43,16 @@ class GTCombiner(Elaboratable):
         m = Module()
         comb = m.d.comb
 
-        previnput = self.gts[-1] | (self.eqs[-1] & self.mux_input)
+        previnput = (self.gts[-1] & self.gt_en) | (self.eqs[-1] & self.aux_input)
 
         for i in range(self.width-1, 0, -1): # counts down from width-1 to 1
             m.submodules["mux%d" % i] = mux = Combiner()
 
             comb += mux.ina.eq(previnput)
-            comb += mux.inb.eq(self.mux_input)
+            comb += mux.inb.eq(self.aux_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)
+            previnput = (self.gts[i-1] & self.gt_en) | (self.eqs[i-1] & mux.outa)
 
         comb += self.outputs[0].eq(previnput)