From: Jacob Lifshay Date: Wed, 3 Aug 2022 05:25:17 +0000 (-0700) Subject: formal test for PriorityPicker passes X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9773d1d531a27ad483ae6dd4309b37aca3ada2e3;p=nmutil.git formal test for PriorityPicker passes I had to rename PriorityPicker's lsb_mode=False argument to msb_mode, since it was actually doing lsb-priority mode by default. Nothing came up when searching for uses of the lsb_mode parameter. --- diff --git a/src/nmutil/formal/__init__.py b/src/nmutil/formal/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/src/nmutil/formal/test_picker.py b/src/nmutil/formal/test_picker.py new file mode 100644 index 0000000..573129c --- /dev/null +++ b/src/nmutil/formal/test_picker.py @@ -0,0 +1,228 @@ +# SPDX-License-Identifier: LGPL-3-or-later +# Copyright 2022 Jacob Lifshay + +import unittest +from nmigen.hdl.ast import AnyConst, Assert, Signal, Const +from nmigen.hdl.dsl import Module +from nmutil.formaltest import FHDLTestCase +from nmutil.picker import PriorityPicker, MultiPriorityPicker + + +class TestPriorityPicker(FHDLTestCase): + def tst(self, wid, msb_mode, reverse_i, reverse_o): + assert isinstance(wid, int) + assert isinstance(msb_mode, bool) + assert isinstance(reverse_i, bool) + assert isinstance(reverse_o, bool) + dut = PriorityPicker(wid=wid, msb_mode=msb_mode, reverse_i=reverse_i, + reverse_o=reverse_o) + self.assertEqual(wid, dut.wid) + self.assertEqual(msb_mode, dut.msb_mode) + self.assertEqual(reverse_i, dut.reverse_i) + self.assertEqual(reverse_o, dut.reverse_o) + self.assertEqual(len(dut.i), wid) + self.assertEqual(len(dut.o), wid) + self.assertEqual(len(dut.en_o), 1) + m = Module() + m.submodules.dut = dut + m.d.comb += dut.i.eq(AnyConst(wid)) + + # assert dut.o only has zero or one bit set + m.d.comb += Assert((dut.o & (dut.o - 1)) == 0) + + m.d.comb += Assert((dut.o != 0) == dut.en_o) + + unreversed_i = Signal(wid) + if reverse_i: + m.d.comb += unreversed_i.eq(dut.i[::-1]) + else: + m.d.comb += unreversed_i.eq(dut.i) + + unreversed_o = Signal(wid) + if reverse_o: + m.d.comb += unreversed_o.eq(dut.o[::-1]) + else: + m.d.comb += unreversed_o.eq(dut.o) + + expected_unreversed_o = Signal(wid) + + found = Const(False, 1) + for i in reversed(range(wid)) if msb_mode else range(wid): + m.d.comb += expected_unreversed_o[i].eq(unreversed_i[i] & ~found) + found |= unreversed_i[i] + + m.d.comb += Assert(expected_unreversed_o == unreversed_o) + + self.assertFormal(m) + + def test_1_msbm_f_revi_f_revo_f(self): + self.tst(wid=1, msb_mode=False, reverse_i=False, reverse_o=False) + + def test_1_msbm_f_revi_f_revo_t(self): + self.tst(wid=1, msb_mode=False, reverse_i=False, reverse_o=True) + + def test_1_msbm_f_revi_t_revo_f(self): + self.tst(wid=1, msb_mode=False, reverse_i=True, reverse_o=False) + + def test_1_msbm_f_revi_t_revo_t(self): + self.tst(wid=1, msb_mode=False, reverse_i=True, reverse_o=True) + + def test_1_msbm_t_revi_f_revo_f(self): + self.tst(wid=1, msb_mode=True, reverse_i=False, reverse_o=False) + + def test_1_msbm_t_revi_f_revo_t(self): + self.tst(wid=1, msb_mode=True, reverse_i=False, reverse_o=True) + + def test_1_msbm_t_revi_t_revo_f(self): + self.tst(wid=1, msb_mode=True, reverse_i=True, reverse_o=False) + + def test_1_msbm_t_revi_t_revo_t(self): + self.tst(wid=1, msb_mode=True, reverse_i=True, reverse_o=True) + + def test_2_msbm_f_revi_f_revo_f(self): + self.tst(wid=2, msb_mode=False, reverse_i=False, reverse_o=False) + + def test_2_msbm_f_revi_f_revo_t(self): + self.tst(wid=2, msb_mode=False, reverse_i=False, reverse_o=True) + + def test_2_msbm_f_revi_t_revo_f(self): + self.tst(wid=2, msb_mode=False, reverse_i=True, reverse_o=False) + + def test_2_msbm_f_revi_t_revo_t(self): + self.tst(wid=2, msb_mode=False, reverse_i=True, reverse_o=True) + + def test_2_msbm_t_revi_f_revo_f(self): + self.tst(wid=2, msb_mode=True, reverse_i=False, reverse_o=False) + + def test_2_msbm_t_revi_f_revo_t(self): + self.tst(wid=2, msb_mode=True, reverse_i=False, reverse_o=True) + + def test_2_msbm_t_revi_t_revo_f(self): + self.tst(wid=2, msb_mode=True, reverse_i=True, reverse_o=False) + + def test_2_msbm_t_revi_t_revo_t(self): + self.tst(wid=2, msb_mode=True, reverse_i=True, reverse_o=True) + + def test_3_msbm_f_revi_f_revo_f(self): + self.tst(wid=3, msb_mode=False, reverse_i=False, reverse_o=False) + + def test_3_msbm_f_revi_f_revo_t(self): + self.tst(wid=3, msb_mode=False, reverse_i=False, reverse_o=True) + + def test_3_msbm_f_revi_t_revo_f(self): + self.tst(wid=3, msb_mode=False, reverse_i=True, reverse_o=False) + + def test_3_msbm_f_revi_t_revo_t(self): + self.tst(wid=3, msb_mode=False, reverse_i=True, reverse_o=True) + + def test_3_msbm_t_revi_f_revo_f(self): + self.tst(wid=3, msb_mode=True, reverse_i=False, reverse_o=False) + + def test_3_msbm_t_revi_f_revo_t(self): + self.tst(wid=3, msb_mode=True, reverse_i=False, reverse_o=True) + + def test_3_msbm_t_revi_t_revo_f(self): + self.tst(wid=3, msb_mode=True, reverse_i=True, reverse_o=False) + + def test_3_msbm_t_revi_t_revo_t(self): + self.tst(wid=3, msb_mode=True, reverse_i=True, reverse_o=True) + + def test_4_msbm_f_revi_f_revo_f(self): + self.tst(wid=4, msb_mode=False, reverse_i=False, reverse_o=False) + + def test_4_msbm_f_revi_f_revo_t(self): + self.tst(wid=4, msb_mode=False, reverse_i=False, reverse_o=True) + + def test_4_msbm_f_revi_t_revo_f(self): + self.tst(wid=4, msb_mode=False, reverse_i=True, reverse_o=False) + + def test_4_msbm_f_revi_t_revo_t(self): + self.tst(wid=4, msb_mode=False, reverse_i=True, reverse_o=True) + + def test_4_msbm_t_revi_f_revo_f(self): + self.tst(wid=4, msb_mode=True, reverse_i=False, reverse_o=False) + + def test_4_msbm_t_revi_f_revo_t(self): + self.tst(wid=4, msb_mode=True, reverse_i=False, reverse_o=True) + + def test_4_msbm_t_revi_t_revo_f(self): + self.tst(wid=4, msb_mode=True, reverse_i=True, reverse_o=False) + + def test_4_msbm_t_revi_t_revo_t(self): + self.tst(wid=4, msb_mode=True, reverse_i=True, reverse_o=True) + + def test_8_msbm_f_revi_f_revo_f(self): + self.tst(wid=8, msb_mode=False, reverse_i=False, reverse_o=False) + + def test_8_msbm_f_revi_f_revo_t(self): + self.tst(wid=8, msb_mode=False, reverse_i=False, reverse_o=True) + + def test_8_msbm_f_revi_t_revo_f(self): + self.tst(wid=8, msb_mode=False, reverse_i=True, reverse_o=False) + + def test_8_msbm_f_revi_t_revo_t(self): + self.tst(wid=8, msb_mode=False, reverse_i=True, reverse_o=True) + + def test_8_msbm_t_revi_f_revo_f(self): + self.tst(wid=8, msb_mode=True, reverse_i=False, reverse_o=False) + + def test_8_msbm_t_revi_f_revo_t(self): + self.tst(wid=8, msb_mode=True, reverse_i=False, reverse_o=True) + + def test_8_msbm_t_revi_t_revo_f(self): + self.tst(wid=8, msb_mode=True, reverse_i=True, reverse_o=False) + + def test_8_msbm_t_revi_t_revo_t(self): + self.tst(wid=8, msb_mode=True, reverse_i=True, reverse_o=True) + + def test_32_msbm_f_revi_f_revo_f(self): + self.tst(wid=32, msb_mode=False, reverse_i=False, reverse_o=False) + + def test_32_msbm_f_revi_f_revo_t(self): + self.tst(wid=32, msb_mode=False, reverse_i=False, reverse_o=True) + + def test_32_msbm_f_revi_t_revo_f(self): + self.tst(wid=32, msb_mode=False, reverse_i=True, reverse_o=False) + + def test_32_msbm_f_revi_t_revo_t(self): + self.tst(wid=32, msb_mode=False, reverse_i=True, reverse_o=True) + + def test_32_msbm_t_revi_f_revo_f(self): + self.tst(wid=32, msb_mode=True, reverse_i=False, reverse_o=False) + + def test_32_msbm_t_revi_f_revo_t(self): + self.tst(wid=32, msb_mode=True, reverse_i=False, reverse_o=True) + + def test_32_msbm_t_revi_t_revo_f(self): + self.tst(wid=32, msb_mode=True, reverse_i=True, reverse_o=False) + + def test_32_msbm_t_revi_t_revo_t(self): + self.tst(wid=32, msb_mode=True, reverse_i=True, reverse_o=True) + + def test_64_msbm_f_revi_f_revo_f(self): + self.tst(wid=64, msb_mode=False, reverse_i=False, reverse_o=False) + + def test_64_msbm_f_revi_f_revo_t(self): + self.tst(wid=64, msb_mode=False, reverse_i=False, reverse_o=True) + + def test_64_msbm_f_revi_t_revo_f(self): + self.tst(wid=64, msb_mode=False, reverse_i=True, reverse_o=False) + + def test_64_msbm_f_revi_t_revo_t(self): + self.tst(wid=64, msb_mode=False, reverse_i=True, reverse_o=True) + + def test_64_msbm_t_revi_f_revo_f(self): + self.tst(wid=64, msb_mode=True, reverse_i=False, reverse_o=False) + + def test_64_msbm_t_revi_f_revo_t(self): + self.tst(wid=64, msb_mode=True, reverse_i=False, reverse_o=True) + + def test_64_msbm_t_revi_t_revo_f(self): + self.tst(wid=64, msb_mode=True, reverse_i=True, reverse_o=False) + + def test_64_msbm_t_revi_t_revo_t(self): + self.tst(wid=64, msb_mode=True, reverse_i=True, reverse_o=True) + + +if __name__ == "__main__": + unittest.main() diff --git a/src/nmutil/picker.py b/src/nmutil/picker.py index 8df01e7..f2cf050 100644 --- a/src/nmutil/picker.py +++ b/src/nmutil/picker.py @@ -1,5 +1,5 @@ # SPDX-License-Identifier: LGPL-3-or-later -""" Priority Picker: optimised back-to-back PriorityEncoder and Decoder +""" Priority Picker: optimized back-to-back PriorityEncoder and Decoder and MultiPriorityPicker: cascading mutually-exclusive pickers This work is funded through NLnet under Grant 2019-02-012 @@ -26,27 +26,29 @@ """ from nmigen import Module, Signal, Cat, Elaboratable, Array, Const, Mux -from nmigen.cli import verilog, rtlil +from nmigen.cli import rtlil import math class PriorityPicker(Elaboratable): """ implements a priority-picker. input: N bits, output: N bits - * lsb_mode is for a LSB-priority picker - * reverse_i=True is for convenient reverseal of the input bits + * msb_mode is for a MSB-priority picker + * reverse_i=True is for convenient reversal of the input bits * reverse_o=True is for convenient reversal of the output bits """ - def __init__(self, wid, lsb_mode=False, reverse_i=False, reverse_o=False): + def __init__(self, wid, msb_mode=False, reverse_i=False, reverse_o=False): self.wid = wid # inputs - self.lsb_mode = lsb_mode + self.msb_mode = msb_mode self.reverse_i = reverse_i self.reverse_o = reverse_o self.i = Signal(wid, reset_less=True) self.o = Signal(wid, reset_less=True) - self.en_o = Signal(reset_less=True) # true if any output is true + + self.en_o = Signal(reset_less=True) + "true if any output is true" def elaborate(self, platform): m = Module() @@ -57,9 +59,11 @@ class PriorityPicker(Elaboratable): i = list(self.i) if self.reverse_i: i.reverse() + if self.msb_mode: + i.reverse() m.d.comb += ni.eq(~Cat(*i)) prange = list(range(0, self.wid)) - if self.lsb_mode: + if self.msb_mode: prange.reverse() for n in prange: t = Signal(name="t%d" % n, reset_less=True)