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