from nmigen import *
from nmigen.cli import main
from nmigen.asserts import *


class TestCase(Elaboratable):
    def __init__(self):
        self.unf = Signal()
        self.value = Signal(4)

    def elaborate(self, platform):
        m = Module()
        m.d.pos += self.value.eq(self.value + 1)
        m.d.neg += self.unf.eq(~self.unf)
        return m


if __name__ == "__main__":
    clk = Signal()
    rst = Signal()

    pos = ClockDomain()
    pos.clk = clk
    pos.rst = rst

    neg = ClockDomain(clk_edge="neg")
    neg.clk = clk
    neg.rst = rst

    testcase = TestCase()

    m = Module()
    m.domains.pos = pos
    m.domains.neg = neg
    m.submodules.testcase = testcase

    count = Signal.range(0, 61, reset_less=True)

    with m.If(count < 60):
        m.d.pos += count.eq(count + 1)

    m.d.comb += Assume(rst == (count < 4))

    m.d.comb += Cover(testcase.value == 5)

    #    main(m, ports=[clk, rst, testcase.unf, testcase.value])
    main(m, ports=[clk, rst, testcase.value])