From: Jacob Lifshay <programmerjake@gmail.com>
Date: Thu, 7 Apr 2022 02:48:57 +0000 (-0700)
Subject: work around yosys bug with Switch() over high-bit-width Value instances
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9e79d78771f183bedbbebf07cf11c4146d74c97;p=nmigen-gf.git

work around yosys bug with Switch() over high-bit-width Value instances

https://github.com/YosysHQ/yosys/issues/3268
---

diff --git a/src/nmigen_gf/hdl/test/test_cldivrem.py b/src/nmigen_gf/hdl/test/test_cldivrem.py
index 69ed013..5929f67 100644
--- a/src/nmigen_gf/hdl/test/test_cldivrem.py
+++ b/src/nmigen_gf/hdl/test/test_cldivrem.py
@@ -63,18 +63,22 @@ class TestEqualLeadingZeroCount(FHDLTestCase):
         m.submodules.dut = dut
         m.d.comb += dut.a.eq(AnyConst(width))
         m.d.comb += dut.b.eq(AnyConst(width))
+        # use a bunch of Value.matches() and boolean logic rather than a
+        # giant Switch()/If() to avoid
+        # https://github.com/YosysHQ/yosys/issues/3268
+        expected_v = False
+        for leading_zeros in range(width + 1):
+            pattern = '0' * leading_zeros + '1' + '-' * width
+            pattern = pattern[0:width]
+            a_has_count = Signal(name=f"a_has_{leading_zeros}")
+            b_has_count = Signal(name=f"b_has_{leading_zeros}")
+            m.d.comb += [
+                a_has_count.eq(dut.a.matches(pattern)),
+                b_has_count.eq(dut.b.matches(pattern)),
+            ]
+            expected_v |= a_has_count & b_has_count
         expected = Signal()
-        with m.Switch(Cat(dut.a, dut.b)):
-            with m.Case('0' * (2 * width)):
-                # `width` leading zeros
-                m.d.comb += expected.eq(1)
-            for i in range(width):
-                # `i` leading zeros
-                pattern = '0' * i + '1' + '-' * (width - i - 1)
-                with m.Case(pattern * 2):
-                    m.d.comb += expected.eq(1)
-            with m.Default():
-                m.d.comb += expected.eq(0)
+        m.d.comb += expected.eq(expected_v)
         m.d.comb += Assert(dut.out == expected)
         self.assertFormal(m)
 
@@ -87,10 +91,8 @@ class TestEqualLeadingZeroCount(FHDLTestCase):
     def test_3(self):
         self.tst(3, full=True)
 
-    def test_formal_16(self):
-        # yosys crashes with 32 or 64
-        # https://github.com/YosysHQ/yosys/issues/3268
-        self.tst_formal(16)
+    def test_formal_64(self):
+        self.tst_formal(64)
 
     def test_formal_8(self):
         self.tst_formal(8)