From 849a8a6d21b23faec1e6a19e0a1f7333ad57d80e Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 5 Feb 2020 09:40:56 -0500 Subject: [PATCH] Add a signal to disable the gt inputs to gt_combiner --- .../part_cmp/experiments/formal/proof_gt.py | 20 +++++++++---------- .../part_cmp/experiments/gt_combiner.py | 9 +++++---- 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/ieee754/part_cmp/experiments/formal/proof_gt.py b/src/ieee754/part_cmp/experiments/formal/proof_gt.py index c0fb998e..923fcf90 100644 --- 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 8be22dec..0ca8e84f 100644 --- 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) -- 2.30.2