From 419a7fce211635a7c21c58ab857a39f98a238572 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 3 Feb 2020 22:28:50 -0500 Subject: [PATCH] Modify gt experiment to handle eq as well --- .../part_cmp/experiments/formal/proof_gt.py | 4 ++++ .../part_cmp/experiments/gt_combiner.py | 20 ++++++++++++++++--- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/src/ieee754/part_cmp/experiments/formal/proof_gt.py b/src/ieee754/part_cmp/experiments/formal/proof_gt.py index 691d8317..c0fb998e 100644 --- a/src/ieee754/part_cmp/experiments/formal/proof_gt.py +++ b/src/ieee754/part_cmp/experiments/formal/proof_gt.py @@ -71,12 +71,16 @@ class CombinerDriver(Elaboratable): comb += Assert(out[i] == eqs[i]) with m.Case(0b00): comb += Assert(out[0] == (eqs[0] & eqs[1] & eqs[2])) + comb += Assert(out[1] == 0) + comb += Assert(out[2] == 0) with m.Case(0b10): comb += Assert(out[0] == (eqs[0] & eqs[1])) + comb += Assert(out[1] == 0) comb += Assert(out[2] == eqs[2]) with m.Case(0b01): comb += Assert(out[0] == eqs[0]) comb += Assert(out[1] == (eqs[1] & eqs[2])) + comb += Assert(out[2] == 0) diff --git a/src/ieee754/part_cmp/experiments/gt_combiner.py b/src/ieee754/part_cmp/experiments/gt_combiner.py index 7fd4da2a..445d3994 100644 --- a/src/ieee754/part_cmp/experiments/gt_combiner.py +++ b/src/ieee754/part_cmp/experiments/gt_combiner.py @@ -1,7 +1,21 @@ from nmigen import Signal, Module, Elaboratable, Mux from ieee754.part_mul_add.partpoints import PartitionPoints -from ieee754.part_cmp.experiments.eq_combiner import Twomux +class Combiner(Elaboratable): + def __init__(self): + self.ina = Signal() + self.inb = Signal() + self.sel = Signal() + self.outa = Signal() + self.outb = Signal() + def elaborate(self, platform): + m = Module() + comb = m.d.comb + + comb += self.outa.eq(Mux(self.sel, self.inb, self.ina)) + comb += self.outb.eq(self.sel & self.ina) + + return m # This is similar to EQCombiner, except that for a greater than # comparison, it needs to deal with both the greater than and equals @@ -26,13 +40,13 @@ class GTCombiner(Elaboratable): 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() + m.submodules["mux{}".format(i)] = mux = Combiner() comb += mux.ina.eq(previnput) 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) + previnput = self.gts[i-1] | (self.eqs[i-1] & mux.outa) comb += self.outputs[0].eq(previnput) -- 2.30.2