src/nmutil/formal/test_queue.py

   1 # SPDX-License-Identifier: LGPL-3-or-later
   2 # Copyright 2022 Jacob Lifshay
   3
   4 import unittest
   5 from nmigen.hdl.ast import (AnySeq, Assert, Signal, Assume, Const,
   6                             unsigned, AnyConst)
   7 from nmigen.hdl.dsl import Module
   8 from nmutil.formaltest import FHDLTestCase
   9 from nmutil.queue import Queue
  10 from nmutil.sim_util import write_il
  11
  12
  13 class TestQueue(FHDLTestCase):
  14     def tst(self, width, depth, fwft, pipe):
  15         assert isinstance(width, int)
  16         assert isinstance(depth, int)
  17         assert isinstance(fwft, bool)
  18         assert isinstance(pipe, bool)
  19         dut = Queue(width=width, depth=depth, fwft=fwft, pipe=pipe)
  20         self.assertEqual(width, dut.width)
  21         self.assertEqual(depth, dut.depth)
  22         self.assertEqual(fwft, dut.fwft)
  23         self.assertEqual(pipe, dut.pipe)
  24         write_il(self, dut, ports=[
  25             dut.level,
  26             dut.r_data, dut.r_en, dut.r_rdy,
  27             dut.w_data, dut.w_en, dut.w_rdy,
  28         ])
  29         m = Module()
  30         m.submodules.dut = dut
  31         m.d.comb += dut.r_en.eq(AnySeq(1))
  32         m.d.comb += dut.w_data.eq(AnySeq(width))
  33         m.d.comb += dut.w_en.eq(AnySeq(1))
  34
  35         index_width = 16
  36         max_index = Const(-1, unsigned(index_width))
  37
  38         check_r_data = Signal(width)
  39         check_r_data_valid = Signal(reset=False)
  40         r_index = Signal(index_width)
  41         check_w_data = Signal(width)
  42         check_w_data_valid = Signal(reset=False)
  43         w_index = Signal(index_width)
  44         check_index = Signal(index_width)
  45         m.d.comb += check_index.eq(AnyConst(index_width))
  46
  47         with m.If(dut.r_en & dut.r_rdy):
  48             with m.If(r_index == check_index):
  49                 m.d.sync += [
  50                     check_r_data.eq(dut.r_data),
  51                     check_r_data_valid.eq(True),
  52                 ]
  53             m.d.sync += [
  54                 Assume(r_index != max_index),
  55                 r_index.eq(r_index + 1),
  56             ]
  57
  58         with m.If(dut.w_en & dut.w_rdy):
  59             with m.If(w_index == check_index):
  60                 m.d.sync += [
  61                     check_w_data.eq(dut.w_data),
  62                     check_w_data_valid.eq(True),
  63                 ]
  64             m.d.sync += [
  65                 Assume(w_index != max_index),
  66                 w_index.eq(w_index + 1),
  67             ]
  68
  69         with m.If(check_r_data_valid & check_w_data_valid):
  70             m.d.comb += Assert(check_r_data == check_w_data)
  71
  72         # 10 is enough to fully test smaller depth queues, larger queues are
  73         # assumed to be correct because the logic doesn't really depend on
  74         # queue depth past the first few values.
  75         self.assertFormal(m, depth=10)
  76
  77     def test_have_all(self):
  78         def bool_char(v):
  79             if v:
  80                 return "t"
  81             return "f"
  82
  83         missing = []
  84
  85         for width in [1, 8]:
  86             for depth in range(8 + 1):
  87                 for fwft in (False, True):
  88                     for pipe in (False, True):
  89                         name = (f"test_{width}_"
  90                                 f"depth_{depth}_"
  91                                 f"fwft_{bool_char(fwft)}_"
  92                                 f"pipe_{bool_char(pipe)}")
  93                         if not callable(getattr(self, name, None)):
  94                             missing.append(f"    def {name}(self):\n"
  95                                            f"        self.tst("
  96                                            f"width={width}, depth={depth}, "
  97                                            f"fwft={fwft}, pipe={pipe})\n")
  98         missing = "\n".join(missing)
  99         self.assertTrue(missing == "", f"missing functions:\n\n{missing}")
 100
 101     def test_1_depth_0_fwft_f_pipe_f(self):
 102         self.tst(width=1, depth=0, fwft=False, pipe=False)
 103
 104     def test_1_depth_0_fwft_f_pipe_t(self):
 105         self.tst(width=1, depth=0, fwft=False, pipe=True)
 106
 107     def test_1_depth_0_fwft_t_pipe_f(self):
 108         self.tst(width=1, depth=0, fwft=True, pipe=False)
 109
 110     def test_1_depth_0_fwft_t_pipe_t(self):
 111         self.tst(width=1, depth=0, fwft=True, pipe=True)
 112
 113     def test_1_depth_1_fwft_f_pipe_f(self):
 114         self.tst(width=1, depth=1, fwft=False, pipe=False)
 115
 116     def test_1_depth_1_fwft_f_pipe_t(self):
 117         self.tst(width=1, depth=1, fwft=False, pipe=True)
 118
 119     def test_1_depth_1_fwft_t_pipe_f(self):
 120         self.tst(width=1, depth=1, fwft=True, pipe=False)
 121
 122     def test_1_depth_1_fwft_t_pipe_t(self):
 123         self.tst(width=1, depth=1, fwft=True, pipe=True)
 124
 125     def test_1_depth_2_fwft_f_pipe_f(self):
 126         self.tst(width=1, depth=2, fwft=False, pipe=False)
 127
 128     def test_1_depth_2_fwft_f_pipe_t(self):
 129         self.tst(width=1, depth=2, fwft=False, pipe=True)
 130
 131     def test_1_depth_2_fwft_t_pipe_f(self):
 132         self.tst(width=1, depth=2, fwft=True, pipe=False)
 133
 134     def test_1_depth_2_fwft_t_pipe_t(self):
 135         self.tst(width=1, depth=2, fwft=True, pipe=True)
 136
 137     def test_1_depth_3_fwft_f_pipe_f(self):
 138         self.tst(width=1, depth=3, fwft=False, pipe=False)
 139
 140     def test_1_depth_3_fwft_f_pipe_t(self):
 141         self.tst(width=1, depth=3, fwft=False, pipe=True)
 142
 143     def test_1_depth_3_fwft_t_pipe_f(self):
 144         self.tst(width=1, depth=3, fwft=True, pipe=False)
 145
 146     def test_1_depth_3_fwft_t_pipe_t(self):
 147         self.tst(width=1, depth=3, fwft=True, pipe=True)
 148
 149     def test_1_depth_4_fwft_f_pipe_f(self):
 150         self.tst(width=1, depth=4, fwft=False, pipe=False)
 151
 152     def test_1_depth_4_fwft_f_pipe_t(self):
 153         self.tst(width=1, depth=4, fwft=False, pipe=True)
 154
 155     def test_1_depth_4_fwft_t_pipe_f(self):
 156         self.tst(width=1, depth=4, fwft=True, pipe=False)
 157
 158     def test_1_depth_4_fwft_t_pipe_t(self):
 159         self.tst(width=1, depth=4, fwft=True, pipe=True)
 160
 161     def test_1_depth_5_fwft_f_pipe_f(self):
 162         self.tst(width=1, depth=5, fwft=False, pipe=False)
 163
 164     def test_1_depth_5_fwft_f_pipe_t(self):
 165         self.tst(width=1, depth=5, fwft=False, pipe=True)
 166
 167     def test_1_depth_5_fwft_t_pipe_f(self):
 168         self.tst(width=1, depth=5, fwft=True, pipe=False)
 169
 170     def test_1_depth_5_fwft_t_pipe_t(self):
 171         self.tst(width=1, depth=5, fwft=True, pipe=True)
 172
 173     def test_1_depth_6_fwft_f_pipe_f(self):
 174         self.tst(width=1, depth=6, fwft=False, pipe=False)
 175
 176     def test_1_depth_6_fwft_f_pipe_t(self):
 177         self.tst(width=1, depth=6, fwft=False, pipe=True)
 178
 179     def test_1_depth_6_fwft_t_pipe_f(self):
 180         self.tst(width=1, depth=6, fwft=True, pipe=False)
 181
 182     def test_1_depth_6_fwft_t_pipe_t(self):
 183         self.tst(width=1, depth=6, fwft=True, pipe=True)
 184
 185     def test_1_depth_7_fwft_f_pipe_f(self):
 186         self.tst(width=1, depth=7, fwft=False, pipe=False)
 187
 188     def test_1_depth_7_fwft_f_pipe_t(self):
 189         self.tst(width=1, depth=7, fwft=False, pipe=True)
 190
 191     def test_1_depth_7_fwft_t_pipe_f(self):
 192         self.tst(width=1, depth=7, fwft=True, pipe=False)
 193
 194     def test_1_depth_7_fwft_t_pipe_t(self):
 195         self.tst(width=1, depth=7, fwft=True, pipe=True)
 196
 197     def test_1_depth_8_fwft_f_pipe_f(self):
 198         self.tst(width=1, depth=8, fwft=False, pipe=False)
 199
 200     def test_1_depth_8_fwft_f_pipe_t(self):
 201         self.tst(width=1, depth=8, fwft=False, pipe=True)
 202
 203     def test_1_depth_8_fwft_t_pipe_f(self):
 204         self.tst(width=1, depth=8, fwft=True, pipe=False)
 205
 206     def test_1_depth_8_fwft_t_pipe_t(self):
 207         self.tst(width=1, depth=8, fwft=True, pipe=True)
 208
 209     def test_8_depth_0_fwft_f_pipe_f(self):
 210         self.tst(width=8, depth=0, fwft=False, pipe=False)
 211
 212     def test_8_depth_0_fwft_f_pipe_t(self):
 213         self.tst(width=8, depth=0, fwft=False, pipe=True)
 214
 215     def test_8_depth_0_fwft_t_pipe_f(self):
 216         self.tst(width=8, depth=0, fwft=True, pipe=False)
 217
 218     def test_8_depth_0_fwft_t_pipe_t(self):
 219         self.tst(width=8, depth=0, fwft=True, pipe=True)
 220
 221     def test_8_depth_1_fwft_f_pipe_f(self):
 222         self.tst(width=8, depth=1, fwft=False, pipe=False)
 223
 224     def test_8_depth_1_fwft_f_pipe_t(self):
 225         self.tst(width=8, depth=1, fwft=False, pipe=True)
 226
 227     def test_8_depth_1_fwft_t_pipe_f(self):
 228         self.tst(width=8, depth=1, fwft=True, pipe=False)
 229
 230     def test_8_depth_1_fwft_t_pipe_t(self):
 231         self.tst(width=8, depth=1, fwft=True, pipe=True)
 232
 233     def test_8_depth_2_fwft_f_pipe_f(self):
 234         self.tst(width=8, depth=2, fwft=False, pipe=False)
 235
 236     def test_8_depth_2_fwft_f_pipe_t(self):
 237         self.tst(width=8, depth=2, fwft=False, pipe=True)
 238
 239     def test_8_depth_2_fwft_t_pipe_f(self):
 240         self.tst(width=8, depth=2, fwft=True, pipe=False)
 241
 242     def test_8_depth_2_fwft_t_pipe_t(self):
 243         self.tst(width=8, depth=2, fwft=True, pipe=True)
 244
 245     def test_8_depth_3_fwft_f_pipe_f(self):
 246         self.tst(width=8, depth=3, fwft=False, pipe=False)
 247
 248     def test_8_depth_3_fwft_f_pipe_t(self):
 249         self.tst(width=8, depth=3, fwft=False, pipe=True)
 250
 251     def test_8_depth_3_fwft_t_pipe_f(self):
 252         self.tst(width=8, depth=3, fwft=True, pipe=False)
 253
 254     def test_8_depth_3_fwft_t_pipe_t(self):
 255         self.tst(width=8, depth=3, fwft=True, pipe=True)
 256
 257     def test_8_depth_4_fwft_f_pipe_f(self):
 258         self.tst(width=8, depth=4, fwft=False, pipe=False)
 259
 260     def test_8_depth_4_fwft_f_pipe_t(self):
 261         self.tst(width=8, depth=4, fwft=False, pipe=True)
 262
 263     def test_8_depth_4_fwft_t_pipe_f(self):
 264         self.tst(width=8, depth=4, fwft=True, pipe=False)
 265
 266     def test_8_depth_4_fwft_t_pipe_t(self):
 267         self.tst(width=8, depth=4, fwft=True, pipe=True)
 268
 269     def test_8_depth_5_fwft_f_pipe_f(self):
 270         self.tst(width=8, depth=5, fwft=False, pipe=False)
 271
 272     def test_8_depth_5_fwft_f_pipe_t(self):
 273         self.tst(width=8, depth=5, fwft=False, pipe=True)
 274
 275     def test_8_depth_5_fwft_t_pipe_f(self):
 276         self.tst(width=8, depth=5, fwft=True, pipe=False)
 277
 278     def test_8_depth_5_fwft_t_pipe_t(self):
 279         self.tst(width=8, depth=5, fwft=True, pipe=True)
 280
 281     def test_8_depth_6_fwft_f_pipe_f(self):
 282         self.tst(width=8, depth=6, fwft=False, pipe=False)
 283
 284     def test_8_depth_6_fwft_f_pipe_t(self):
 285         self.tst(width=8, depth=6, fwft=False, pipe=True)
 286
 287     def test_8_depth_6_fwft_t_pipe_f(self):
 288         self.tst(width=8, depth=6, fwft=True, pipe=False)
 289
 290     def test_8_depth_6_fwft_t_pipe_t(self):
 291         self.tst(width=8, depth=6, fwft=True, pipe=True)
 292
 293     def test_8_depth_7_fwft_f_pipe_f(self):
 294         self.tst(width=8, depth=7, fwft=False, pipe=False)
 295
 296     def test_8_depth_7_fwft_f_pipe_t(self):
 297         self.tst(width=8, depth=7, fwft=False, pipe=True)
 298
 299     def test_8_depth_7_fwft_t_pipe_f(self):
 300         self.tst(width=8, depth=7, fwft=True, pipe=False)
 301
 302     def test_8_depth_7_fwft_t_pipe_t(self):
 303         self.tst(width=8, depth=7, fwft=True, pipe=True)
 304
 305     def test_8_depth_8_fwft_f_pipe_f(self):
 306         self.tst(width=8, depth=8, fwft=False, pipe=False)
 307
 308     def test_8_depth_8_fwft_f_pipe_t(self):
 309         self.tst(width=8, depth=8, fwft=False, pipe=True)
 310
 311     def test_8_depth_8_fwft_t_pipe_f(self):
 312         self.tst(width=8, depth=8, fwft=True, pipe=False)
 313
 314     def test_8_depth_8_fwft_t_pipe_t(self):
 315         self.tst(width=8, depth=8, fwft=True, pipe=True)
 316
 317
 318 if __name__ == "__main__":
 319     unittest.main()