src/nmutil/formal/test_picker.py

   1 # SPDX-License-Identifier: LGPL-3-or-later
   2 # Copyright 2022 Jacob Lifshay
   3
   4 from functools import reduce
   5 import operator
   6 import unittest
   7 from nmigen.hdl.ast import AnyConst, Assert, Signal, Const, Array, Shape, Mux
   8 from nmigen.hdl.dsl import Module
   9 from nmutil.formaltest import FHDLTestCase
  10 from nmutil.picker import (BetterMultiPriorityPicker, PriorityPicker,
  11                            MultiPriorityPicker)
  12 from nmutil.sim_util import write_il
  13
  14
  15 class TestPriorityPicker(FHDLTestCase):
  16     def tst(self, wid, msb_mode, reverse_i, reverse_o):
  17         assert isinstance(wid, int)
  18         assert isinstance(msb_mode, bool)
  19         assert isinstance(reverse_i, bool)
  20         assert isinstance(reverse_o, bool)
  21         dut = PriorityPicker(wid=wid, msb_mode=msb_mode, reverse_i=reverse_i,
  22                              reverse_o=reverse_o)
  23         self.assertEqual(wid, dut.wid)
  24         self.assertEqual(msb_mode, dut.msb_mode)
  25         self.assertEqual(reverse_i, dut.reverse_i)
  26         self.assertEqual(reverse_o, dut.reverse_o)
  27         self.assertEqual(len(dut.i), wid)
  28         self.assertEqual(len(dut.o), wid)
  29         self.assertEqual(len(dut.en_o), 1)
  30         m = Module()
  31         m.submodules.dut = dut
  32         m.d.comb += dut.i.eq(AnyConst(wid))
  33
  34         # assert dut.o only has zero or one bit set
  35         m.d.comb += Assert((dut.o & (dut.o - 1)) == 0)
  36
  37         m.d.comb += Assert((dut.o != 0) == dut.en_o)
  38
  39         unreversed_i = Signal(wid)
  40         if reverse_i:
  41             m.d.comb += unreversed_i.eq(dut.i[::-1])
  42         else:
  43             m.d.comb += unreversed_i.eq(dut.i)
  44
  45         unreversed_o = Signal(wid)
  46         if reverse_o:
  47             m.d.comb += unreversed_o.eq(dut.o[::-1])
  48         else:
  49             m.d.comb += unreversed_o.eq(dut.o)
  50
  51         expected_unreversed_o = Signal(wid)
  52
  53         found = Const(False, 1)
  54         for i in reversed(range(wid)) if msb_mode else range(wid):
  55             m.d.comb += expected_unreversed_o[i].eq(unreversed_i[i] & ~found)
  56             found |= unreversed_i[i]
  57
  58         m.d.comb += Assert(expected_unreversed_o == unreversed_o)
  59
  60         self.assertFormal(m)
  61
  62     def test_1_msbm_f_revi_f_revo_f(self):
  63         self.tst(wid=1, msb_mode=False, reverse_i=False, reverse_o=False)
  64
  65     def test_1_msbm_f_revi_f_revo_t(self):
  66         self.tst(wid=1, msb_mode=False, reverse_i=False, reverse_o=True)
  67
  68     def test_1_msbm_f_revi_t_revo_f(self):
  69         self.tst(wid=1, msb_mode=False, reverse_i=True, reverse_o=False)
  70
  71     def test_1_msbm_f_revi_t_revo_t(self):
  72         self.tst(wid=1, msb_mode=False, reverse_i=True, reverse_o=True)
  73
  74     def test_1_msbm_t_revi_f_revo_f(self):
  75         self.tst(wid=1, msb_mode=True, reverse_i=False, reverse_o=False)
  76
  77     def test_1_msbm_t_revi_f_revo_t(self):
  78         self.tst(wid=1, msb_mode=True, reverse_i=False, reverse_o=True)
  79
  80     def test_1_msbm_t_revi_t_revo_f(self):
  81         self.tst(wid=1, msb_mode=True, reverse_i=True, reverse_o=False)
  82
  83     def test_1_msbm_t_revi_t_revo_t(self):
  84         self.tst(wid=1, msb_mode=True, reverse_i=True, reverse_o=True)
  85
  86     def test_2_msbm_f_revi_f_revo_f(self):
  87         self.tst(wid=2, msb_mode=False, reverse_i=False, reverse_o=False)
  88
  89     def test_2_msbm_f_revi_f_revo_t(self):
  90         self.tst(wid=2, msb_mode=False, reverse_i=False, reverse_o=True)
  91
  92     def test_2_msbm_f_revi_t_revo_f(self):
  93         self.tst(wid=2, msb_mode=False, reverse_i=True, reverse_o=False)
  94
  95     def test_2_msbm_f_revi_t_revo_t(self):
  96         self.tst(wid=2, msb_mode=False, reverse_i=True, reverse_o=True)
  97
  98     def test_2_msbm_t_revi_f_revo_f(self):
  99         self.tst(wid=2, msb_mode=True, reverse_i=False, reverse_o=False)
 100
 101     def test_2_msbm_t_revi_f_revo_t(self):
 102         self.tst(wid=2, msb_mode=True, reverse_i=False, reverse_o=True)
 103
 104     def test_2_msbm_t_revi_t_revo_f(self):
 105         self.tst(wid=2, msb_mode=True, reverse_i=True, reverse_o=False)
 106
 107     def test_2_msbm_t_revi_t_revo_t(self):
 108         self.tst(wid=2, msb_mode=True, reverse_i=True, reverse_o=True)
 109
 110     def test_3_msbm_f_revi_f_revo_f(self):
 111         self.tst(wid=3, msb_mode=False, reverse_i=False, reverse_o=False)
 112
 113     def test_3_msbm_f_revi_f_revo_t(self):
 114         self.tst(wid=3, msb_mode=False, reverse_i=False, reverse_o=True)
 115
 116     def test_3_msbm_f_revi_t_revo_f(self):
 117         self.tst(wid=3, msb_mode=False, reverse_i=True, reverse_o=False)
 118
 119     def test_3_msbm_f_revi_t_revo_t(self):
 120         self.tst(wid=3, msb_mode=False, reverse_i=True, reverse_o=True)
 121
 122     def test_3_msbm_t_revi_f_revo_f(self):
 123         self.tst(wid=3, msb_mode=True, reverse_i=False, reverse_o=False)
 124
 125     def test_3_msbm_t_revi_f_revo_t(self):
 126         self.tst(wid=3, msb_mode=True, reverse_i=False, reverse_o=True)
 127
 128     def test_3_msbm_t_revi_t_revo_f(self):
 129         self.tst(wid=3, msb_mode=True, reverse_i=True, reverse_o=False)
 130
 131     def test_3_msbm_t_revi_t_revo_t(self):
 132         self.tst(wid=3, msb_mode=True, reverse_i=True, reverse_o=True)
 133
 134     def test_4_msbm_f_revi_f_revo_f(self):
 135         self.tst(wid=4, msb_mode=False, reverse_i=False, reverse_o=False)
 136
 137     def test_4_msbm_f_revi_f_revo_t(self):
 138         self.tst(wid=4, msb_mode=False, reverse_i=False, reverse_o=True)
 139
 140     def test_4_msbm_f_revi_t_revo_f(self):
 141         self.tst(wid=4, msb_mode=False, reverse_i=True, reverse_o=False)
 142
 143     def test_4_msbm_f_revi_t_revo_t(self):
 144         self.tst(wid=4, msb_mode=False, reverse_i=True, reverse_o=True)
 145
 146     def test_4_msbm_t_revi_f_revo_f(self):
 147         self.tst(wid=4, msb_mode=True, reverse_i=False, reverse_o=False)
 148
 149     def test_4_msbm_t_revi_f_revo_t(self):
 150         self.tst(wid=4, msb_mode=True, reverse_i=False, reverse_o=True)
 151
 152     def test_4_msbm_t_revi_t_revo_f(self):
 153         self.tst(wid=4, msb_mode=True, reverse_i=True, reverse_o=False)
 154
 155     def test_4_msbm_t_revi_t_revo_t(self):
 156         self.tst(wid=4, msb_mode=True, reverse_i=True, reverse_o=True)
 157
 158     def test_8_msbm_f_revi_f_revo_f(self):
 159         self.tst(wid=8, msb_mode=False, reverse_i=False, reverse_o=False)
 160
 161     def test_8_msbm_f_revi_f_revo_t(self):
 162         self.tst(wid=8, msb_mode=False, reverse_i=False, reverse_o=True)
 163
 164     def test_8_msbm_f_revi_t_revo_f(self):
 165         self.tst(wid=8, msb_mode=False, reverse_i=True, reverse_o=False)
 166
 167     def test_8_msbm_f_revi_t_revo_t(self):
 168         self.tst(wid=8, msb_mode=False, reverse_i=True, reverse_o=True)
 169
 170     def test_8_msbm_t_revi_f_revo_f(self):
 171         self.tst(wid=8, msb_mode=True, reverse_i=False, reverse_o=False)
 172
 173     def test_8_msbm_t_revi_f_revo_t(self):
 174         self.tst(wid=8, msb_mode=True, reverse_i=False, reverse_o=True)
 175
 176     def test_8_msbm_t_revi_t_revo_f(self):
 177         self.tst(wid=8, msb_mode=True, reverse_i=True, reverse_o=False)
 178
 179     def test_8_msbm_t_revi_t_revo_t(self):
 180         self.tst(wid=8, msb_mode=True, reverse_i=True, reverse_o=True)
 181
 182     def test_32_msbm_f_revi_f_revo_f(self):
 183         self.tst(wid=32, msb_mode=False, reverse_i=False, reverse_o=False)
 184
 185     def test_32_msbm_f_revi_f_revo_t(self):
 186         self.tst(wid=32, msb_mode=False, reverse_i=False, reverse_o=True)
 187
 188     def test_32_msbm_f_revi_t_revo_f(self):
 189         self.tst(wid=32, msb_mode=False, reverse_i=True, reverse_o=False)
 190
 191     def test_32_msbm_f_revi_t_revo_t(self):
 192         self.tst(wid=32, msb_mode=False, reverse_i=True, reverse_o=True)
 193
 194     def test_32_msbm_t_revi_f_revo_f(self):
 195         self.tst(wid=32, msb_mode=True, reverse_i=False, reverse_o=False)
 196
 197     def test_32_msbm_t_revi_f_revo_t(self):
 198         self.tst(wid=32, msb_mode=True, reverse_i=False, reverse_o=True)
 199
 200     def test_32_msbm_t_revi_t_revo_f(self):
 201         self.tst(wid=32, msb_mode=True, reverse_i=True, reverse_o=False)
 202
 203     def test_32_msbm_t_revi_t_revo_t(self):
 204         self.tst(wid=32, msb_mode=True, reverse_i=True, reverse_o=True)
 205
 206     def test_64_msbm_f_revi_f_revo_f(self):
 207         self.tst(wid=64, msb_mode=False, reverse_i=False, reverse_o=False)
 208
 209     def test_64_msbm_f_revi_f_revo_t(self):
 210         self.tst(wid=64, msb_mode=False, reverse_i=False, reverse_o=True)
 211
 212     def test_64_msbm_f_revi_t_revo_f(self):
 213         self.tst(wid=64, msb_mode=False, reverse_i=True, reverse_o=False)
 214
 215     def test_64_msbm_f_revi_t_revo_t(self):
 216         self.tst(wid=64, msb_mode=False, reverse_i=True, reverse_o=True)
 217
 218     def test_64_msbm_t_revi_f_revo_f(self):
 219         self.tst(wid=64, msb_mode=True, reverse_i=False, reverse_o=False)
 220
 221     def test_64_msbm_t_revi_f_revo_t(self):
 222         self.tst(wid=64, msb_mode=True, reverse_i=False, reverse_o=True)
 223
 224     def test_64_msbm_t_revi_t_revo_f(self):
 225         self.tst(wid=64, msb_mode=True, reverse_i=True, reverse_o=False)
 226
 227     def test_64_msbm_t_revi_t_revo_t(self):
 228         self.tst(wid=64, msb_mode=True, reverse_i=True, reverse_o=True)
 229
 230
 231 class TestMultiPriorityPicker(FHDLTestCase):
 232     def make_dut(self, width, levels, indices, multi_in):
 233         dut = MultiPriorityPicker(wid=width, levels=levels, indices=indices,
 234                                   multi_in=multi_in)
 235         self.assertEqual(width, dut.wid)
 236         self.assertEqual(levels, dut.levels)
 237         self.assertEqual(indices, dut.indices)
 238         self.assertEqual(multi_in, dut.multi_in)
 239         return dut
 240
 241     def tst(self, *, width, levels, indices, multi_in):
 242         assert isinstance(width, int) and width >= 1
 243         assert isinstance(levels, int) and 1 <= levels <= width
 244         assert isinstance(indices, bool)
 245         assert isinstance(multi_in, bool)
 246         dut = self.make_dut(width=width, levels=levels, indices=indices,
 247                             multi_in=multi_in)
 248         expected_ports = []
 249         if multi_in:
 250             self.assertIsInstance(dut.i, (Array, list))
 251             self.assertEqual(len(dut.i), levels)
 252             for i in dut.i:
 253                 self.assertIsInstance(i, Signal)
 254                 self.assertEqual(len(i), width)
 255                 expected_ports.append(i)
 256         else:
 257             self.assertIsInstance(dut.i, Signal)
 258             self.assertEqual(len(dut.i), width)
 259             expected_ports.append(dut.i)
 260
 261         self.assertIsInstance(dut.o, (Array, list))
 262         self.assertEqual(len(dut.o), levels)
 263         for o in dut.o:
 264             self.assertIsInstance(o, Signal)
 265             self.assertEqual(len(o), width)
 266             expected_ports.append(o)
 267
 268         self.assertEqual(len(dut.en_o), levels)
 269         expected_ports.append(dut.en_o)
 270
 271         if indices:
 272             self.assertIsInstance(dut.idx_o, (Array, list))
 273             self.assertEqual(len(dut.idx_o), levels)
 274             for idx_o in dut.idx_o:
 275                 self.assertIsInstance(idx_o, Signal)
 276                 expected_ports.append(idx_o)
 277         else:
 278             self.assertFalse(hasattr(dut, "idx_o"))
 279
 280         self.assertListEqual(expected_ports, dut.ports())
 281
 282         write_il(self, dut, ports=dut.ports())
 283
 284         m = Module()
 285         m.submodules.dut = dut
 286         if multi_in:
 287             for i in dut.i:
 288                 m.d.comb += i.eq(AnyConst(width))
 289         else:
 290             m.d.comb += dut.i.eq(AnyConst(width))
 291
 292         prev_set = 0
 293         for o, en_o in zip(dut.o, dut.en_o):
 294             # assert o only has zero or one bit set
 295             m.d.comb += Assert((o & (o - 1)) == 0)
 296             # assert o doesn't overlap any previous outputs
 297             m.d.comb += Assert((o & prev_set) == 0)
 298             prev_set |= o
 299
 300             m.d.comb += Assert((o != 0) == en_o)
 301
 302         prev_set = Const(0, width)
 303         priority_pickers = [PriorityPicker(width) for _ in range(levels)]
 304         for level in range(levels):
 305             pp = priority_pickers[level]
 306             setattr(m.submodules, f"pp_{level}", pp)
 307             inp = dut.i[level] if multi_in else dut.i
 308             m.d.comb += pp.i.eq(inp & ~prev_set)
 309             cur_set = Signal(width, name=f"cur_set_{level}")
 310             m.d.comb += cur_set.eq(prev_set | pp.o)
 311             prev_set = cur_set
 312             m.d.comb += Assert(pp.o == dut.o[level])
 313             expected_idx = Signal(32, name=f"expected_idx_{level}")
 314             number_of_prev_en_o_set = reduce(
 315                 operator.add, (i.en_o for i in priority_pickers[:level]), 0)
 316             m.d.comb += expected_idx.eq(number_of_prev_en_o_set)
 317             if indices:
 318                 m.d.comb += Assert(expected_idx == dut.idx_o[level])
 319
 320         self.assertFormal(m)
 321
 322     def test_4_levels_1_idxs_f_mi_f(self):
 323         self.tst(width=4, levels=1, indices=False, multi_in=False)
 324
 325     def test_4_levels_1_idxs_f_mi_t(self):
 326         self.tst(width=4, levels=1, indices=False, multi_in=True)
 327
 328     def test_4_levels_1_idxs_t_mi_f(self):
 329         self.tst(width=4, levels=1, indices=True, multi_in=False)
 330
 331     def test_4_levels_1_idxs_t_mi_t(self):
 332         self.tst(width=4, levels=1, indices=True, multi_in=True)
 333
 334     def test_4_levels_2_idxs_f_mi_f(self):
 335         self.tst(width=4, levels=2, indices=False, multi_in=False)
 336
 337     def test_4_levels_2_idxs_f_mi_t(self):
 338         self.tst(width=4, levels=2, indices=False, multi_in=True)
 339
 340     def test_4_levels_2_idxs_t_mi_f(self):
 341         self.tst(width=4, levels=2, indices=True, multi_in=False)
 342
 343     def test_4_levels_2_idxs_t_mi_t(self):
 344         self.tst(width=4, levels=2, indices=True, multi_in=True)
 345
 346     def test_4_levels_3_idxs_f_mi_f(self):
 347         self.tst(width=4, levels=3, indices=False, multi_in=False)
 348
 349     def test_4_levels_3_idxs_f_mi_t(self):
 350         self.tst(width=4, levels=3, indices=False, multi_in=True)
 351
 352     def test_4_levels_3_idxs_t_mi_f(self):
 353         self.tst(width=4, levels=3, indices=True, multi_in=False)
 354
 355     def test_4_levels_3_idxs_t_mi_t(self):
 356         self.tst(width=4, levels=3, indices=True, multi_in=True)
 357
 358     def test_4_levels_4_idxs_f_mi_f(self):
 359         self.tst(width=4, levels=4, indices=False, multi_in=False)
 360
 361     def test_4_levels_4_idxs_f_mi_t(self):
 362         self.tst(width=4, levels=4, indices=False, multi_in=True)
 363
 364     def test_4_levels_4_idxs_t_mi_f(self):
 365         self.tst(width=4, levels=4, indices=True, multi_in=False)
 366
 367     def test_4_levels_4_idxs_t_mi_t(self):
 368         self.tst(width=4, levels=4, indices=True, multi_in=True)
 369
 370     def test_8_levels_1_idxs_f_mi_f(self):
 371         self.tst(width=8, levels=1, indices=False, multi_in=False)
 372
 373     def test_8_levels_1_idxs_f_mi_t(self):
 374         self.tst(width=8, levels=1, indices=False, multi_in=True)
 375
 376     def test_8_levels_1_idxs_t_mi_f(self):
 377         self.tst(width=8, levels=1, indices=True, multi_in=False)
 378
 379     def test_8_levels_1_idxs_t_mi_t(self):
 380         self.tst(width=8, levels=1, indices=True, multi_in=True)
 381
 382     def test_8_levels_2_idxs_f_mi_f(self):
 383         self.tst(width=8, levels=2, indices=False, multi_in=False)
 384
 385     def test_8_levels_2_idxs_f_mi_t(self):
 386         self.tst(width=8, levels=2, indices=False, multi_in=True)
 387
 388     def test_8_levels_2_idxs_t_mi_f(self):
 389         self.tst(width=8, levels=2, indices=True, multi_in=False)
 390
 391     def test_8_levels_2_idxs_t_mi_t(self):
 392         self.tst(width=8, levels=2, indices=True, multi_in=True)
 393
 394     def test_8_levels_3_idxs_f_mi_f(self):
 395         self.tst(width=8, levels=3, indices=False, multi_in=False)
 396
 397     def test_8_levels_3_idxs_f_mi_t(self):
 398         self.tst(width=8, levels=3, indices=False, multi_in=True)
 399
 400     def test_8_levels_3_idxs_t_mi_f(self):
 401         self.tst(width=8, levels=3, indices=True, multi_in=False)
 402
 403     def test_8_levels_3_idxs_t_mi_t(self):
 404         self.tst(width=8, levels=3, indices=True, multi_in=True)
 405
 406     def test_8_levels_4_idxs_f_mi_f(self):
 407         self.tst(width=8, levels=4, indices=False, multi_in=False)
 408
 409     def test_8_levels_4_idxs_f_mi_t(self):
 410         self.tst(width=8, levels=4, indices=False, multi_in=True)
 411
 412     def test_8_levels_4_idxs_t_mi_f(self):
 413         self.tst(width=8, levels=4, indices=True, multi_in=False)
 414
 415     def test_8_levels_4_idxs_t_mi_t(self):
 416         self.tst(width=8, levels=4, indices=True, multi_in=True)
 417
 418     def test_8_levels_5_idxs_f_mi_f(self):
 419         self.tst(width=8, levels=5, indices=False, multi_in=False)
 420
 421     def test_8_levels_5_idxs_f_mi_t(self):
 422         self.tst(width=8, levels=5, indices=False, multi_in=True)
 423
 424     def test_8_levels_5_idxs_t_mi_f(self):
 425         self.tst(width=8, levels=5, indices=True, multi_in=False)
 426
 427     def test_8_levels_5_idxs_t_mi_t(self):
 428         self.tst(width=8, levels=5, indices=True, multi_in=True)
 429
 430     def test_8_levels_6_idxs_f_mi_f(self):
 431         self.tst(width=8, levels=6, indices=False, multi_in=False)
 432
 433     def test_8_levels_6_idxs_f_mi_t(self):
 434         self.tst(width=8, levels=6, indices=False, multi_in=True)
 435
 436     def test_8_levels_6_idxs_t_mi_f(self):
 437         self.tst(width=8, levels=6, indices=True, multi_in=False)
 438
 439     def test_8_levels_6_idxs_t_mi_t(self):
 440         self.tst(width=8, levels=6, indices=True, multi_in=True)
 441
 442     def test_8_levels_7_idxs_f_mi_f(self):
 443         self.tst(width=8, levels=7, indices=False, multi_in=False)
 444
 445     def test_8_levels_7_idxs_f_mi_t(self):
 446         self.tst(width=8, levels=7, indices=False, multi_in=True)
 447
 448     def test_8_levels_7_idxs_t_mi_f(self):
 449         self.tst(width=8, levels=7, indices=True, multi_in=False)
 450
 451     def test_8_levels_7_idxs_t_mi_t(self):
 452         self.tst(width=8, levels=7, indices=True, multi_in=True)
 453
 454     def test_8_levels_8_idxs_f_mi_f(self):
 455         self.tst(width=8, levels=8, indices=False, multi_in=False)
 456
 457     def test_8_levels_8_idxs_f_mi_t(self):
 458         self.tst(width=8, levels=8, indices=False, multi_in=True)
 459
 460     def test_8_levels_8_idxs_t_mi_f(self):
 461         self.tst(width=8, levels=8, indices=True, multi_in=False)
 462
 463     def test_8_levels_8_idxs_t_mi_t(self):
 464         self.tst(width=8, levels=8, indices=True, multi_in=True)
 465
 466     def test_16_levels_16_idxs_f_mi_f(self):
 467         self.tst(width=16, levels=16, indices=False, multi_in=False)
 468
 469
 470 class TestBetterMultiPriorityPicker(TestMultiPriorityPicker):
 471     def make_dut(self, width, levels, indices, multi_in):
 472         if multi_in:
 473             self.skipTest(
 474                 "multi_in are not supported by BetterMultiPriorityPicker")
 475         if indices:
 476             self.skipTest(
 477                 "indices are not supported by BetterMultiPriorityPicker")
 478         dut = BetterMultiPriorityPicker(width=width, levels=levels)
 479         self.assertEqual(width, dut.width)
 480         self.assertEqual(levels, dut.levels)
 481         return dut
 482
 483
 484 if __name__ == "__main__":
 485     unittest.main()