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)
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)