From: Michael Nolan Date: Wed, 5 Feb 2020 15:52:47 +0000 (-0500) Subject: move gt_combiner out of experiments/ X-Git-Tag: ls180-24jan2020~263 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6dd865ff437d6339e08a3061ce20f111a30c1034;p=ieee754fpu.git move gt_combiner out of experiments/ --- diff --git a/src/ieee754/part_cmp/eq_gt_ge.py b/src/ieee754/part_cmp/eq_gt_ge.py index 7120ca1f..cb6d117d 100644 --- a/src/ieee754/part_cmp/eq_gt_ge.py +++ b/src/ieee754/part_cmp/eq_gt_ge.py @@ -18,7 +18,7 @@ from nmigen.back.pysim import Simulator, Delay, Settle from nmigen.cli import main from ieee754.part_mul_add.partpoints import PartitionPoints -from ieee754.part_cmp.experiments.gt_combiner import GTCombiner +from ieee754.part_cmp.gt_combiner import GTCombiner class PartitionedEqGtGe(Elaboratable): diff --git a/src/ieee754/part_cmp/experiments/formal/proof_gt.py b/src/ieee754/part_cmp/experiments/formal/proof_gt.py deleted file mode 100644 index a1033132..00000000 --- a/src/ieee754/part_cmp/experiments/formal/proof_gt.py +++ /dev/null @@ -1,108 +0,0 @@ -# Proof of correctness for partitioned equal signal combiner -# Copyright (C) 2020 Michael Nolan - -from nmigen import Module, Signal, Elaboratable, Mux -from nmigen.asserts import Assert, AnyConst, Assume -from nmigen.test.utils import FHDLTestCase -from nmigen.cli import rtlil - -from ieee754.part_cmp.experiments.gt_combiner import GTCombiner -import unittest - - -# This defines a module to drive the device under test and assert -# properties about its outputs -class CombinerDriver(Elaboratable): - def __init__(self): - # inputs and outputs - pass - - def elaborate(self, platform): - m = Module() - comb = m.d.comb - width = 3 - - # setup the inputs and outputs of the DUT as anyconst - eqs = Signal(width) - gts = Signal(width) - gates = Signal(width-1) - out = Signal(width) - aux_input = Signal() - gt_en = Signal() - comb += [eqs.eq(AnyConst(width)), - gates.eq(AnyConst(width)), - gts.eq(AnyConst(width)), - aux_input.eq(AnyConst(1)), - gt_en.eq(AnyConst(1))] - - - m.submodules.dut = dut = GTCombiner(width) - - - # 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((aux_input == 0) & (gt_en == 1)): - 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] == (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 - with m.Elif((aux_input == 1) & (gt_en == 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[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])) - - - - # connect up the inputs and outputs. - comb += dut.eqs.eq(eqs) - comb += dut.gts.eq(gts) - comb += dut.gates.eq(gates) - comb += dut.aux_input.eq(aux_input) - comb += dut.gt_en.eq(gt_en) - comb += out.eq(dut.outputs) - - return m - -class GTCombinerTestCase(FHDLTestCase): - def test_gt_combiner(self): - module = CombinerDriver() - self.assertFormal(module, mode="bmc", depth=4) - def test_ilang(self): - dut = GTCombiner(3) - vl = rtlil.convert(dut, ports=dut.ports()) - with open("gt_combiner.il", "w") as f: - f.write(vl) - - -if __name__ == '__main__': - unittest.main() diff --git a/src/ieee754/part_cmp/experiments/gt_combiner.py b/src/ieee754/part_cmp/experiments/gt_combiner.py deleted file mode 100644 index 419a4859..00000000 --- a/src/ieee754/part_cmp/experiments/gt_combiner.py +++ /dev/null @@ -1,76 +0,0 @@ -from nmigen import Signal, Module, Elaboratable, Mux -from ieee754.part_mul_add.partpoints import PartitionPoints - -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 -# signals from each partition. The signals are combined using a -# cascaded AND/OR to give the following effect: -# When a partition is open, the output is set if either the current -# partition's greater than flag is set, or the current partition's -# equal flag is set AND the previous partition's greater than output -# is true - -class GTCombiner(Elaboratable): - - def __init__(self, width): - self.width = width - - # These two signals allow this module to do more than just a - # partitioned greater than comparison. - # - If aux_input is set to 0 and gt_en is set to 1, then this - # module performs a partitioned greater than comparision - # - If aux_input is set to 1 and gt_en is set to 0, then this - # module is functionally equivalent to the eq_combiner - # module. - # - If aux_input is set to 1 and gt_en is set to 1, then this - # module performs a partitioned greater than or equals - # comparison - self.aux_input = Signal(reset_less=True) # right hand side mux input - self.gt_en = Signal(reset_less=True) # enable or disable 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) - self.outputs = Signal(width, reset_less=True) - - def elaborate(self, platform): - m = Module() - comb = m.d.comb - - previnput = (self.gts[0] & self.gt_en) | (self.eqs[0] & self.aux_input) - - for i in range(self.width-1): - m.submodules["mux%d" % i] = mux = Combiner() - - comb += mux.ina.eq(previnput) - comb += mux.inb.eq(self.aux_input) - comb += mux.sel.eq(self.gates[i]) - comb += self.outputs[i].eq(mux.outb) - previnput = (self.gts[i+1] & self.gt_en) | \ - (self.eqs[i+1] & mux.outa) - - comb += self.outputs[-1].eq(previnput) - - return m - - def ports(self): - return [self.eqs, self.gts, self.gates, self.outputs, - self.gt_en, self.aux_input] diff --git a/src/ieee754/part_cmp/formal/proof_gt.py b/src/ieee754/part_cmp/formal/proof_gt.py new file mode 100644 index 00000000..cdf1bb04 --- /dev/null +++ b/src/ieee754/part_cmp/formal/proof_gt.py @@ -0,0 +1,108 @@ +# Proof of correctness for partitioned equal signal combiner +# Copyright (C) 2020 Michael Nolan + +from nmigen import Module, Signal, Elaboratable, Mux +from nmigen.asserts import Assert, AnyConst, Assume +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil + +from ieee754.part_cmp.gt_combiner import GTCombiner +import unittest + + +# This defines a module to drive the device under test and assert +# properties about its outputs +class CombinerDriver(Elaboratable): + def __init__(self): + # inputs and outputs + pass + + def elaborate(self, platform): + m = Module() + comb = m.d.comb + width = 3 + + # setup the inputs and outputs of the DUT as anyconst + eqs = Signal(width) + gts = Signal(width) + gates = Signal(width-1) + out = Signal(width) + aux_input = Signal() + gt_en = Signal() + comb += [eqs.eq(AnyConst(width)), + gates.eq(AnyConst(width)), + gts.eq(AnyConst(width)), + aux_input.eq(AnyConst(1)), + gt_en.eq(AnyConst(1))] + + + m.submodules.dut = dut = GTCombiner(width) + + + # 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((aux_input == 0) & (gt_en == 1)): + 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] == (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 + with m.Elif((aux_input == 1) & (gt_en == 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[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])) + + + + # connect up the inputs and outputs. + comb += dut.eqs.eq(eqs) + comb += dut.gts.eq(gts) + comb += dut.gates.eq(gates) + comb += dut.aux_input.eq(aux_input) + comb += dut.gt_en.eq(gt_en) + comb += out.eq(dut.outputs) + + return m + +class GTCombinerTestCase(FHDLTestCase): + def test_gt_combiner(self): + module = CombinerDriver() + self.assertFormal(module, mode="bmc", depth=4) + def test_ilang(self): + dut = GTCombiner(3) + vl = rtlil.convert(dut, ports=dut.ports()) + with open("gt_combiner.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main() diff --git a/src/ieee754/part_cmp/gt_combiner.py b/src/ieee754/part_cmp/gt_combiner.py new file mode 100644 index 00000000..419a4859 --- /dev/null +++ b/src/ieee754/part_cmp/gt_combiner.py @@ -0,0 +1,76 @@ +from nmigen import Signal, Module, Elaboratable, Mux +from ieee754.part_mul_add.partpoints import PartitionPoints + +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 +# signals from each partition. The signals are combined using a +# cascaded AND/OR to give the following effect: +# When a partition is open, the output is set if either the current +# partition's greater than flag is set, or the current partition's +# equal flag is set AND the previous partition's greater than output +# is true + +class GTCombiner(Elaboratable): + + def __init__(self, width): + self.width = width + + # These two signals allow this module to do more than just a + # partitioned greater than comparison. + # - If aux_input is set to 0 and gt_en is set to 1, then this + # module performs a partitioned greater than comparision + # - If aux_input is set to 1 and gt_en is set to 0, then this + # module is functionally equivalent to the eq_combiner + # module. + # - If aux_input is set to 1 and gt_en is set to 1, then this + # module performs a partitioned greater than or equals + # comparison + self.aux_input = Signal(reset_less=True) # right hand side mux input + self.gt_en = Signal(reset_less=True) # enable or disable 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) + self.outputs = Signal(width, reset_less=True) + + def elaborate(self, platform): + m = Module() + comb = m.d.comb + + previnput = (self.gts[0] & self.gt_en) | (self.eqs[0] & self.aux_input) + + for i in range(self.width-1): + m.submodules["mux%d" % i] = mux = Combiner() + + comb += mux.ina.eq(previnput) + comb += mux.inb.eq(self.aux_input) + comb += mux.sel.eq(self.gates[i]) + comb += self.outputs[i].eq(mux.outb) + previnput = (self.gts[i+1] & self.gt_en) | \ + (self.eqs[i+1] & mux.outa) + + comb += self.outputs[-1].eq(previnput) + + return m + + def ports(self): + return [self.eqs, self.gts, self.gates, self.outputs, + self.gt_en, self.aux_input]