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 (file)
index 0000000..e69de29

diff --git a/src/nmutil/formal/test_picker.py b/src/nmutil/formal/test_picker.py
new file mode 100644 (file)
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 8df01e783445f53e623e61eac7e1ef3698ed660b..f2cf0502f625c61b368d7d16a47594781ce37d56 100644 (file)
--- 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)