From: Michael Nolan Date: Mon, 3 Feb 2020 17:13:20 +0000 (-0500) Subject: Rename partition_combiner to eq_combiner X-Git-Tag: ls180-24jan2020~289 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39a32f562d9a735e7fd4db30bd95a342e4d8b377;p=ieee754fpu.git Rename partition_combiner to eq_combiner --- diff --git a/src/ieee754/part_cmp/eq_combiner.py b/src/ieee754/part_cmp/eq_combiner.py new file mode 100644 index 00000000..07b73429 --- /dev/null +++ b/src/ieee754/part_cmp/eq_combiner.py @@ -0,0 +1,53 @@ +from nmigen import Signal, Module, Elaboratable, Mux +from ieee754.part_mul_add.partpoints import PartitionPoints + + + +class Twomux(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(Mux(self.sel, self.ina, self.inb)) + + return m + +#This module is a test of a better way to implement combining the +#signals for equals for the partitioned equality module than +#equals.py's giant switch statement. The idea is to use a tree of two +#input/two output multiplexors and or gates to select whether each +#signal is or isn't combined with its neighbors. +class EQCombiner(Elaboratable): + def __init__(self, width): + self.width = width + self.neqs = Signal(width, reset_less=True) + 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.neqs[-1] + for i in range(self.width-1, 0, -1): # counts down from width-1 to 1 + m.submodules["mux{}".format(i)] = mux = Twomux() + + comb += mux.ina.eq(previnput) + comb += mux.inb.eq(0) + comb += mux.sel.eq(~self.gates[i-1]) + comb += self.outputs[i].eq(mux.outa ^ self.gates[i-1]) + previnput = mux.outb | self.neqs[i-1] + + comb += self.outputs[0].eq(~previnput) + + return m + + def ports(self): + return [self.neqs, self.gates, self.outputs] diff --git a/src/ieee754/part_cmp/formal/proof_combiner.py b/src/ieee754/part_cmp/formal/proof_combiner.py deleted file mode 100644 index 37022ef4..00000000 --- a/src/ieee754/part_cmp/formal/proof_combiner.py +++ /dev/null @@ -1,76 +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 -from nmigen.test.utils import FHDLTestCase -from nmigen.cli import rtlil - -from ieee754.part_cmp.partition_combiner import Combiner -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) - neqs = Signal(width) - gates = Signal(width-1) - out = Signal(width) - comb += [eqs.eq(AnyConst(width)), - gates.eq(AnyConst(width)), - neqs.eq(~eqs)] - - m.submodules.dut = dut = Combiner(width) - - with m.Switch(gates): - with m.Case(0b11): - for i in range(width): - 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) - - - - - - # connect up the inputs and outputs. - comb += dut.neqs.eq(neqs) - comb += dut.gates.eq(gates) - comb += out.eq(dut.outputs) - - return m - -class CombinerTestCase(FHDLTestCase): - def test_combiner(self): - module = CombinerDriver() - self.assertFormal(module, mode="bmc", depth=4) - def test_ilang(self): - dut = Combiner(3) - vl = rtlil.convert(dut, ports=dut.ports()) - with open("partition_combiner.il", "w") as f: - f.write(vl) - - -if __name__ == '__main__': - unittest.main() diff --git a/src/ieee754/part_cmp/formal/proof_eq.py b/src/ieee754/part_cmp/formal/proof_eq.py new file mode 100644 index 00000000..b72bad6d --- /dev/null +++ b/src/ieee754/part_cmp/formal/proof_eq.py @@ -0,0 +1,76 @@ +# 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 +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil + +from ieee754.part_cmp.eq_combiner import EQCombiner +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) + neqs = Signal(width) + gates = Signal(width-1) + out = Signal(width) + comb += [eqs.eq(AnyConst(width)), + gates.eq(AnyConst(width)), + neqs.eq(~eqs)] + + m.submodules.dut = dut = EQCombiner(width) + + with m.Switch(gates): + with m.Case(0b11): + for i in range(width): + 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) + + + + + + # connect up the inputs and outputs. + comb += dut.neqs.eq(neqs) + comb += dut.gates.eq(gates) + comb += out.eq(dut.outputs) + + return m + +class EQCombinerTestCase(FHDLTestCase): + def test_combiner(self): + module = CombinerDriver() + self.assertFormal(module, mode="bmc", depth=4) + def test_ilang(self): + dut = EQCombiner(3) + vl = rtlil.convert(dut, ports=dut.ports()) + with open("partition_combiner.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main() diff --git a/src/ieee754/part_cmp/partition_combiner.py b/src/ieee754/part_cmp/partition_combiner.py deleted file mode 100644 index 2608097b..00000000 --- a/src/ieee754/part_cmp/partition_combiner.py +++ /dev/null @@ -1,53 +0,0 @@ -from nmigen import Signal, Module, Elaboratable, Mux -from ieee754.part_mul_add.partpoints import PartitionPoints - - - -class Twomux(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(Mux(self.sel, self.ina, self.inb)) - - return m - -#This module is a test of a better way to implement combining the -#signals for equals for the partitioned equality module than -#equals.py's giant switch statement. The idea is to use a tree of two -#input/two output multiplexors and or gates to select whether each -#signal is or isn't combined with its neighbors. -class Combiner(Elaboratable): - def __init__(self, width): - self.width = width - self.neqs = Signal(width, reset_less=True) - 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.neqs[-1] - for i in range(self.width-1, 0, -1): # counts down from width-1 to 1 - m.submodules["mux{}".format(i)] = mux = Twomux() - - comb += mux.ina.eq(previnput) - comb += mux.inb.eq(0) - comb += mux.sel.eq(~self.gates[i-1]) - comb += self.outputs[i].eq(mux.outa ^ self.gates[i-1]) - previnput = mux.outb | self.neqs[i-1] - - comb += self.outputs[0].eq(~previnput) - - return m - - def ports(self): - return [self.neqs, self.gates, self.outputs]