Assigning clock domain to attribute results in failures, radically different RTLIL output #567

RobertBaruch · 2020-12-25T18:57:56Z

The idea here is to create a module that does its thing based on whatever clock domain is passed to its __init__ function.

Here's the minimum viable test:

from nmigen import Signal, Module, Elaboratable, ClockSignal, ResetSignal, ClockDomain
from nmigen.build import Platform
from nmigen.asserts import Assert, Assume, Past, Rose
from nmigen.cli import main_parser, main_runner


class Example(Elaboratable):
    def __init__(self, clk):
        self.clk = clk

        self.d0 = Signal(32)
        self.d1 = Signal(32)
        self.sel = Signal(2)
        self.q = Signal(32)

    def elaborate(self, _: Platform) -> Module:
        m = Module()

        c = self.clk  # Replace with c = m.d.ph to make this work!

        with m.If(self.sel[0]):
            c += self.q.eq(self.d0)
        with m.Elif(self.sel[1]):
            c += self.q.eq(self.d1)
        return m


def formal():
    """Formal verification for the example."""
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    ph = ClockDomain("ph")
    clk = ClockSignal("ph")

    m.domains += ph
    m.submodules.s = s = Example(clk=m.d.ph)

    with m.If(Rose(clk)):
        with m.Switch(~Past(s.sel)):
            with m.Case(0b00):
                m.d.comb += Assert(s.q == Past(s.q))
            with m.Case(0b10):
                m.d.comb += Assert(s.q == Past(s.d0))
            with m.Case(0b01):
                m.d.comb += Assert(s.q == Past(s.d1))

    m.d.sync += clk.eq(~clk)
    m.d.comb += Assume(~ResetSignal("ph"))
    m.d.comb += Assume(s.sel != 0b11)

    main_runner(parser, args, m, ports=[s.d0, s.d1, s.sel, s.q])


if __name__ == "__main__":
    formal()

.sby file:

[tasks]
bmc

[options]
bmc: mode bmc
bmc: depth 10
multiclock on

[engines]
cover: smtbmc boolector
bmc: smtbmc z3

[script]
read_verilog <<END
module \$dff (CLK, D, Q);
  parameter WIDTH = 0;
  parameter CLK_POLARITY = 1'b1;
  input CLK;
  input [WIDTH-1:0] D;
  output reg [WIDTH-1:0] Q;
  \$ff #(.WIDTH(WIDTH)) _TECHMAP_REPLACE_ (.D(D),.Q(Q));
endmodule
END
design -stash dff2ff
read_ilang toplevel.il
proc
techmap -map %dff2ff top/w:clk %co
prep -top top

[files]
toplevel.il

Run as:

$ python3 example.py generate -t il > toplevel.il
$ sby -f ics.sby bmc

Replacing c = self.clk with c = m.d.ph makes the example work. Otherwise, it fails bmc.

We can also see that with c = self.clk, the RTLIL output bad.zip is very different from the output with c = m.d.ph: good.zip

Interestingly, modifying the example to eliminate the Elif makes the example work:

from nmigen import Signal, Module, Elaboratable, ClockSignal, ResetSignal, ClockDomain
from nmigen.build import Platform
from nmigen.asserts import Assert, Assume, Past, Rose
from nmigen.cli import main_parser, main_runner


class Example(Elaboratable):
    def __init__(self, clk):
        self.clk = clk

        self.d0 = Signal(32)
        self.d1 = Signal(32)
        self.sel = Signal(2)
        self.q = Signal(32)

    def elaborate(self, _: Platform) -> Module:
        m = Module()

        c = self.clk

        with m.If(self.sel[0]):
            c += self.q.eq(self.d0)
        # with m.Elif(self.sel[1]):
        #     c += self.q.eq(self.d1)
        return m


def formal():
    """Formal verification for the example."""
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    ph = ClockDomain("ph")
    clk = ClockSignal("ph")

    m.domains += ph
    m.submodules.s = s = Example(clk=m.d.ph)

    with m.If(Rose(clk)):
        with m.Switch(~Past(s.sel)):
            with m.Case(0b00):
                m.d.comb += Assert(s.q == Past(s.q))
            with m.Case(0b10):
                m.d.comb += Assert(s.q == Past(s.d0))
            # with m.Case(0b01):
            #     m.d.comb += Assert(s.q == Past(s.d1))

    m.d.sync += clk.eq(~clk)
    m.d.comb += Assume(~ResetSignal("ph"))
    m.d.comb += Assume(s.sel != 0b11)

    main_runner(parser, args, m, ports=[s.d0, s.d1, s.sel, s.q])


if __name__ == "__main__":
    formal()

The text was updated successfully, but these errors were encountered:

RobertBaruch · 2020-12-25T19:15:46Z

Note, I believe the solution is not to use c = self.clk but c = m.d[self.clk] where self.clk is the name of the domain. However, I'm not sure why I can't pass the domain itself?

whitequark · 2020-12-25T19:18:57Z

In general, you should only pass clock domain names around. (Take a look at how nmigen.lib does it.) If you pass clock domain objects around, you will encounter issues such as this. Whether a diagnostic can be added to detect this case is something I will look into later.

RobertBaruch · 2020-12-25T19:28:58Z

Makes sense. However, when I changed my enormous several thousand line design to use this method (by passing string names around instead of the actual domain, which just resulted in changing maybe 20 lines), I ran into an error that is difficult to debug:

Traceback (most recent call last):
  File "formal_cpu.py", line 1578, in <module>
    main(FormalCPU, filename=filename)
  File "/mnt/f/riscv-reboot/util.py", line 44, in main
    output = rtlil.convert(fragment, ports=ports)
  File "/home/robertbaruch/.local/lib/python3.8/site-packages/nmigen/back/rtlil.py", line 1057, in convert
    fragment = ir.Fragment.get(elaboratable, platform).prepare(**kwargs)
  File "/home/robertbaruch/.local/lib/python3.8/site-packages/nmigen/hdl/ir.py", line 530, in prepare
    new_domains = fragment._propagate_domains(missing_domain)
  File "/home/robertbaruch/.local/lib/python3.8/site-packages/nmigen/hdl/ir.py", line 380, in _propagate_domains
    new_domains = self._create_missing_domains(missing_domain, platform=platform)
  File "/home/robertbaruch/.local/lib/python3.8/site-packages/nmigen/hdl/ir.py", line 356, in _create_missing_domains
    value = missing_domain(domain_name)
  File "/home/robertbaruch/.local/lib/python3.8/site-packages/nmigen/hdl/ir.py", line 526, in <lambda>
    def prepare(self, ports=None, missing_domain=lambda name: ClockDomain(name)):
  File "/home/robertbaruch/.local/lib/python3.8/site-packages/nmigen/hdl/cd.py", line 57, in __init__
    if name.startswith("cd_"):
AttributeError: '_ModuleBuilderDomain' object has no attribute 'startswith'
make: *** [Makefile:57: formal_cpu_op.il] Error 1

whitequark · 2020-12-25T19:31:36Z

That seems like you are misusing the result of m.d[...] as a clock domain name somewhere.

RobertBaruch · 2020-12-25T19:35:35Z

It's true, I am... somewhere. Now I have to track it do--- oh. Yeah. Found it :) I neglected to refactor this one other file.

RobertBaruch · 2020-12-25T19:37:28Z

I'm ok with closing out this question with the answer: don't do that, and instead use clock domain names.

The updated correct example is:

from nmigen import Signal, Module, Elaboratable, ClockSignal, ResetSignal, ClockDomain
from nmigen.build import Platform
from nmigen.asserts import Assert, Assume, Past, Rose
from nmigen.cli import main_parser, main_runner


class Example(Elaboratable):
    def __init__(self, clk: str):
        self.clk = clk

        self.d0 = Signal(32)
        self.d1 = Signal(32)
        self.sel = Signal(2)
        self.q = Signal(32)

    def elaborate(self, _: Platform) -> Module:
        m = Module()

        c = m.d[self.clk]

        with m.If(self.sel[0]):
            c += self.q.eq(self.d0)
        with m.Elif(self.sel[1]):
            c += self.q.eq(self.d1)
        return m


def formal():
    """Formal verification for the example."""
    parser = main_parser()
    args = parser.parse_args()

    m = Module()
    ph = ClockDomain("ph")
    clk = ClockSignal("ph")

    m.domains += ph
    m.submodules.s = s = Example(clk="ph")

    with m.If(Rose(clk)):
        with m.Switch(~Past(s.sel)):
            with m.Case(0b00):
                m.d.comb += Assert(s.q == Past(s.q))
            with m.Case(0b10):
                m.d.comb += Assert(s.q == Past(s.d0))
            with m.Case(0b01):
                m.d.comb += Assert(s.q == Past(s.d1))

    m.d.sync += clk.eq(~clk)
    m.d.comb += Assume(~ResetSignal("ph"))
    m.d.comb += Assume(s.sel != 0b11)

    main_runner(parser, args, m, ports=[s.d0, s.d1, s.sel, s.q])


if __name__ == "__main__":
    formal()

whitequark added the question label Dec 25, 2020

RobertBaruch closed this as completed Dec 25, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Assigning clock domain to attribute results in failures, radically different RTLIL output #567

Assigning clock domain to attribute results in failures, radically different RTLIL output #567

RobertBaruch commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020

whitequark commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020

whitequark commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020 •

edited

Loading

Assigning clock domain to attribute results in failures, radically different RTLIL output #567

Assigning clock domain to attribute results in failures, radically different RTLIL output #567

Comments

RobertBaruch commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020

whitequark commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020

whitequark commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020

RobertBaruch commented Dec 25, 2020 • edited Loading

RobertBaruch commented Dec 25, 2020 •

edited

Loading