From: Michael Nolan Date: Mon, 3 Feb 2020 19:41:36 +0000 (-0500) Subject: Move experiments with partition methods to a separate folder X-Git-Tag: ls180-24jan2020~287 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b7dcaba26f793e49acf82fa8408568b810369eb;p=ieee754fpu.git Move experiments with partition methods to a separate folder --- diff --git a/src/ieee754/part_cmp/eq_combiner.py b/src/ieee754/part_cmp/eq_combiner.py deleted file mode 100644 index 07b73429..00000000 --- a/src/ieee754/part_cmp/eq_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 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/experiments/eq_combiner.py b/src/ieee754/part_cmp/experiments/eq_combiner.py new file mode 100644 index 00000000..07b73429 --- /dev/null +++ b/src/ieee754/part_cmp/experiments/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/experiments/formal/.gitignore b/src/ieee754/part_cmp/experiments/formal/.gitignore new file mode 100644 index 00000000..37ad79e3 --- /dev/null +++ b/src/ieee754/part_cmp/experiments/formal/.gitignore @@ -0,0 +1 @@ +proof_*/** diff --git a/src/ieee754/part_cmp/experiments/formal/proof_eq.py b/src/ieee754/part_cmp/experiments/formal/proof_eq.py new file mode 100644 index 00000000..80fd7f1d --- /dev/null +++ b/src/ieee754/part_cmp/experiments/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.experiments.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/experiments/test.py b/src/ieee754/part_cmp/experiments/test.py new file mode 100644 index 00000000..18a24566 --- /dev/null +++ b/src/ieee754/part_cmp/experiments/test.py @@ -0,0 +1,86 @@ +from ieee754.part_mul_add.partpoints import PartitionPoints +import ieee754.part_cmp.equal_ortree as ortree +import ieee754.part_cmp.equal as equal +from nmigen.cli import rtlil +from nmigen import Signal, Module + +def create_ilang(mod, name, ports): + vl = rtlil.convert(mod, ports=ports) + with open(name, "w") as f: + f.write(vl) + +def create_ortree(width, points): + sig = Signal(len(points.values())) + for i, key in enumerate(points): + points[key] = sig[i] + eq = ortree.PartitionedEq(width, points) + + create_ilang(eq, "ortree.il", [eq.a, eq.b, eq.output, sig]) + +def create_equal(width, points): + sig = Signal(len(points.values())) + for i, key in enumerate(points): + points[key] = sig[i] + + eq = equal.PartitionedEq(width, points) + + create_ilang(eq, "equal.il", [eq.a, eq.b, eq.output, sig]) + + +if __name__ == "__main__": + points = PartitionPoints() + sig = Signal(7) + for i in range(sig.width): + points[i*8+8] = True + + # create_equal(32, points) + create_ortree(64, points) + + + + + +# ortree: +# === design hierarchy === + + # top 1 + # mux1 1 + # mux2 1 + # mux3 1 + + # Number of wires: 49 + # Number of wire bits: 89 + # Number of public wires: 36 + # Number of public wire bits: 76 + # Number of memories: 0 + # Number of memory bits: 0 + # Number of processes: 0 + # Number of cells: 29 + # $_MUX_ 6 + # $_NOR_ 1 + # $_NOT_ 3 + # $_OR_ 8 + # $_XOR_ 11 + + +# equals: +# === top === + +# Number of wires: 121 +# Number of wire bits: 161 +# Number of public wires: 12 +# Number of public wire bits: 52 +# Number of memories: 0 +# Number of memory bits: 0 +# Number of processes: 0 +# Number of cells: 113 +# $_ANDNOT_ 32 +# $_AND_ 7 +# $_MUX_ 4 +# $_NAND_ 1 +# $_NOR_ 2 +# $_NOT_ 1 +# $_ORNOT_ 6 +# $_OR_ 44 +# $_XNOR_ 1 +# $_XOR_ 15 diff --git a/src/ieee754/part_cmp/formal/proof_eq.py b/src/ieee754/part_cmp/formal/proof_eq.py deleted file mode 100644 index b72bad6d..00000000 --- a/src/ieee754/part_cmp/formal/proof_eq.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.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()