src/ieee754/test_partitioned_signal_tester.py

   1 # SPDX-License-Identifier: LGPL-3-or-later
   2 # See Notices.txt for copyright information
   3
   4 from nmigen.hdl.ast import AnyConst, Assert, Assume, Signal
   5 from nmigen.hdl.dsl import Module
   6 from ieee754.partitioned_signal_tester import (
   7     SimdSignalTester, Layout, Lane, formal)
   8 import unittest
   9
  10
  11 class TestFormal(unittest.TestCase):
  12     def test_formal(self):
  13         m = Module()
  14         a = Signal(10)
  15         b = Signal(10)
  16         m.d.comb += a.eq(AnyConst(10))
  17         m.d.comb += b.eq(AnyConst(10))
  18         m.d.comb += Assume(a * b == 1021 * 1019)
  19         m.d.comb += Assert((a == 1021) | (a == 1019))
  20         formal(self, m)
  21
  22     @unittest.expectedFailure
  23     def test_formal_fail(self):
  24         m = Module()
  25         a = Signal(10)
  26         b = Signal(10)
  27         m.d.comb += a.eq(AnyConst(10))
  28         m.d.comb += b.eq(AnyConst(10))
  29         m.d.comb += Assume(a * b == 1021 * 1019)
  30         m.d.comb += Assert(a == 1021)
  31         formal(self, m)
  32
  33
  34 class TestLayout(unittest.TestCase):
  35     maxDiff = None
  36
  37     def test_repr(self):
  38         self.assertEqual(repr(Layout({3: False, 7: True}, 16)),
  39                          "Layout((0, 3, 7, 16), width=16)")
  40         self.assertEqual(repr(Layout({7: False, 3: True}, 16)),
  41                          "Layout((0, 3, 7, 16), width=16)")
  42         self.assertEqual(repr(Layout(range(0, 10, 2), 10)),
  43                          "Layout((0, 2, 4, 6, 8, 10), width=10)")
  44         self.assertEqual(repr(Layout(range(0, 10, 2))),
  45                          "Layout((0, 2, 4, 6, 8), width=8)")
  46         self.assertEqual(repr(Layout(())),
  47                          "Layout((0,), width=0)")
  48         self.assertEqual(repr(Layout((1,))),
  49                          "Layout((0, 1), width=1)")
  50
  51     def test_cast(self):
  52         a = Layout.cast((1, 2, 3))
  53         self.assertEqual(repr(a),
  54                          "Layout((0, 1, 2, 3), width=3)")
  55         b = Layout.cast(a)
  56         self.assertIs(a, b)
  57
  58     def test_part_signal_count(self):
  59         a = Layout.cast(())
  60         b = Layout.cast((1,))
  61         c = Layout.cast((1, 3))
  62         d = Layout.cast((0, 1, 3))
  63         e = Layout.cast((1, 2, 3))
  64         self.assertEqual(a.part_signal_count, 0)
  65         self.assertEqual(b.part_signal_count, 0)
  66         self.assertEqual(c.part_signal_count, 1)
  67         self.assertEqual(d.part_signal_count, 1)
  68         self.assertEqual(e.part_signal_count, 2)
  69
  70     def test_lanes(self):
  71         a = Layout.cast(())
  72         self.assertEqual(list(a.lanes()), [])
  73         b = Layout.cast((1,))
  74         self.assertEqual(list(b.lanes()), [Lane(0, 1, b)])
  75         c = Layout.cast((1, 3))
  76         self.assertEqual(list(c.lanes()),
  77                          [Lane(0, 1, c),
  78                           Lane(1, 2, c),
  79                           Lane(0, 3, c)])
  80         d = Layout.cast((1, 4, 5))
  81         self.assertEqual(list(d.lanes()),
  82                          [Lane(0, 1, d),
  83                           Lane(4, 1, d),
  84                           Lane(1, 3, d),
  85                           Lane(0, 4, d),
  86                           Lane(1, 4, d),
  87                           Lane(0, 5, d)])
  88         e = Layout(range(0, 32, 8), 32)
  89         self.assertEqual(list(e.lanes()),
  90                          [Lane(0, 8, e),
  91                           Lane(8, 8, e),
  92                           Lane(16, 8, e),
  93                           Lane(24, 8, e),
  94                           Lane(0, 16, e),
  95                           Lane(8, 16, e),
  96                           Lane(16, 16, e),
  97                           Lane(0, 24, e),
  98                           Lane(8, 24, e),
  99                           Lane(0, 32, e)])
 100
 101     def test_is_compatible(self):
 102         a = Layout.cast(())
 103         b = Layout.cast((1,))
 104         c = Layout.cast((1, 2))
 105         d = Layout.cast((4, 5))
 106         e = Layout.cast((1, 2, 3, 4))
 107         f = Layout.cast((8, 16, 24, 32))
 108         compatibility_classes = {
 109             a: 0,
 110             b: 1,
 111             c: 2,
 112             d: 2,
 113             e: 4,
 114             f: 4,
 115         }
 116         for lhs in compatibility_classes:
 117             for rhs in compatibility_classes:
 118                 with self.subTest(lhs=lhs, rhs=rhs):
 119                     self.assertEqual(compatibility_classes[lhs]
 120                                      == compatibility_classes[rhs],
 121                                      lhs.is_compatible(rhs))
 122
 123     def test_translate_lanes_to(self):
 124         src = Layout((0, 3, 7, 12, 13))
 125         dest = Layout((0, 8, 16, 24, 32))
 126         src_lanes = list(src.lanes())
 127         src_lanes.sort(key=lambda lane: lane.start)
 128         dest_lanes = list(dest.lanes())
 129         dest_lanes.sort(key=lambda lane: lane.start)
 130         self.assertEqual(len(src_lanes), len(dest_lanes))
 131         for src_lane, dest_lane in zip(src_lanes, dest_lanes):
 132             with self.subTest(src_lane=src_lane, dest_lane=dest_lane):
 133                 self.assertEqual(src_lane.translate_to(dest), dest_lane)
 134                 self.assertEqual(dest_lane.translate_to(src), src_lane)
 135
 136
 137 class TestLane(unittest.TestCase):
 138     def test_is_active(self):
 139         layout = Layout((0, 8, 16, 24, 32))
 140         def do_test(part_starts, expected_lanes):
 141             with self.subTest(part_starts=part_starts,
 142                               expected_lanes=expected_lanes):
 143                 for lane in layout.lanes():
 144                     expected = (lane.start, lane.size) in expected_lanes
 145                     with self.subTest(lane=lane):
 146                         self.assertEqual(lane.is_active(part_starts),
 147                                          expected)
 148
 149         _0 = False
 150         _1 = True
 151         do_test((_1, _0, _0, _0, _1),
 152                 {(0, 32)})
 153         do_test((_1, _0, _0, _1, _1),
 154                 {(0, 24), (24, 8)})
 155         do_test((_1, _0, _1, _0, _1),
 156                 {(0, 16), (16, 16)})
 157         do_test((_1, _0, _1, _1, _1),
 158                 {(0, 16), (16, 8), (24, 8)})
 159         do_test((_1, _1, _0, _0, _1),
 160                 {(0, 8), (8, 24)})
 161         do_test((_1, _1, _0, _1, _1),
 162                 {(0, 8), (8, 16), (24, 8)})
 163         do_test((_1, _1, _1, _0, _1),
 164                 {(0, 8), (8, 8), (16, 16)})
 165         do_test((_1, _1, _1, _1, _1),
 166                 {(0, 8), (8, 8), (16, 8), (24, 8)})
 167
 168     def test_as_slice(self):
 169         slice_target = tuple(range(8))
 170         layout = Layout((0, 2, 4, 6, 8))
 171         slices = list(slice_target[lane.as_slice()]
 172                       for lane in layout.lanes())
 173         self.assertEqual(slices,
 174                          [(0, 1),
 175                           (2, 3),
 176                           (4, 5),
 177                           (6, 7),
 178                           (0, 1, 2, 3),
 179                           (2, 3, 4, 5),
 180                           (4, 5, 6, 7),
 181                           (0, 1, 2, 3, 4, 5),
 182                           (2, 3, 4, 5, 6, 7),
 183                           (0, 1, 2, 3, 4, 5, 6, 7)])
 184
 185
 186 class TestSimdSignalTester(unittest.TestCase):
 187     def test_sim_identity(self):
 188         m = Module()
 189         SimdSignalTester(m,
 190                                 lambda inputs: inputs[0],
 191                                 lambda lane, inputs: inputs[0],
 192                                 (0, 8, 16, 24, 32)).run_sim(self)
 193
 194     def test_formal_identity(self):
 195         m = Module()
 196         SimdSignalTester(m,
 197                                 lambda inputs: inputs[0],
 198                                 lambda lane, inputs: inputs[0],
 199                                 (0, 8, 16, 24, 32)).run_formal(self)
 200
 201     def test_sim_pass_through_input(self):
 202         for which_input in range(0, 2):
 203             m = Module()
 204             SimdSignalTester(m,
 205                                     lambda inputs: inputs[which_input],
 206                                     lambda lane, inputs: inputs[which_input],
 207                                     (0, 8, 16, 24, 32),
 208                                     (0, 1, 2, 3, 4)).run_sim(self)
 209
 210     def test_formal_pass_through_input(self):
 211         for which_input in range(0, 2):
 212             m = Module()
 213             SimdSignalTester(m,
 214                                     lambda inputs: inputs[which_input],
 215                                     lambda lane, inputs: inputs[which_input],
 216                                     (0, 8, 16, 24, 32),
 217                                     (0, 1, 2, 3, 4)).run_formal(self)
 218
 219
 220 if __name__ == '__main__':
 221     unittest.main()