Another example of RTLIL failing BMC while Verilog succeeds.

[RobertBaruch]

I have a case which MAY be caused by bad use of Initial and Assume. If this is a bad use, I'd kind of expect a complaint to be shown. Instead, I get a BMC trace that shows a signal is changed not on its clock.

My goal is to have a test Signal, saved_data which is initialized to the value of another Signal, mem (assumed to be randomly initialized on startup by formal) on startup. I use an Initial and Assume in the comb domain for this. However, the test Signal then should change on the positive edge of my clock signal.

Is that the wrong way to do what I want?

The code:

from nmigen import Signal, Module, Elaboratable, ClockDomain
from nmigen.asserts import Assert, Assume, Initial, Stable
from nmigen.back import rtlil
from nmigen.hdl import Fragment


class Buggy(Elaboratable):
    def __init__(self):
        self.data_in = Signal(32)
        self.do_write = Signal()
        self.mem = Signal(32)

    def elaborate(self, _):
        m = Module()

        with m.If(self.do_write):
            m.d.ph2 += self.mem.eq(self.data_in)

        return m

    @classmethod
    def formal(cls):
        m = Module()
        buggy = Buggy()
        m.submodules += buggy

        # Generate the ph1 and ph2 clocks:
        #           ________          ________
        #    ph1  _|        |________|        |________|
        #         _____________     _____________     __
        #    ph2               |___|             |___|
        #
        cycle_count = Signal(8, reset=0, reset_less=True)
        phase_count = Signal(3, reset=0, reset_less=True)

        ph2 = ClockDomain("ph2")

        m.domains += ph2

        m.d.sync += phase_count.eq(phase_count + 1)
        with m.Switch(phase_count):
            with m.Case(0, 1, 2, 3):
                m.d.comb += ph2.clk.eq(1)
            with m.Case(4):
                m.d.comb += ph2.clk.eq(0)
            with m.Case(5):
                m.d.comb += ph2.clk.eq(1)
                m.d.sync += phase_count.eq(0)
                m.d.sync += cycle_count.eq(cycle_count + 1)

        # This is how we expect to use the thing. data_in and
        # do_write only change on cycle pos edges.
        with m.If(phase_count == 5):
            for i in range(0, 5):
                m.d.comb += [
                    Assume(Stable(buggy.do_write, i)),
                    Assume(Stable(buggy.data_in, i)),
                ]

        # We expect that the data in mem does not change,
        # except when it is written to.
        saved_data = Signal(32)

        with m.If(buggy.do_write):
            m.d.ph2 += saved_data.eq(buggy.data_in)

        with m.If(Initial()):
            m.d.comb += Assume(saved_data == buggy.mem)
        with m.Else():
            m.d.comb += Assert(saved_data == buggy.mem)

        return m, [buggy.do_write, buggy.data_in, buggy.mem, saved_data, ph2.clk]


if __name__ == "__main__":
    design, ports = Buggy.formal()
    fragment = Fragment.get(design, None)
    output = rtlil.convert(fragment, ports=ports)
    with open("toplevel.il", "w") as f:
        f.write(output)

The sby:

[tasks]
bmc

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

[engines]
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

The toplevel.il: toplevel.il.zip

Assert fails in line 70 (m.d.comb += Assert(saved_data == buggy.mem))

The anomalous trace:

[whitequark]

I have a case which MAY be caused by bad use of Initial and Assume. If this is a bad use, I'd kind of expect a complaint to be shown.

I haven't looked yet at the rest of your issue but just to be clear: formal integration in nMigen is immature and it's fairly likely that you will find more cases like this.

[RobertBaruch]

Oh, no worries -- I am pretty happy with the state of formal right now. I've been able to formally verify two processors (6800, Z80) just through nMigen. I just found this one case where I'm pretty sure I should be doing one thing, when I'm actually doing another.

[RobertBaruch]

Hmm... I pared down the clock generation a little and reduced the signal size from 32 to 1 to make the RTLIL smaller and easier to understand.

from nmigen import Signal, Module, Elaboratable, ClockDomain
from nmigen.asserts import Assert, Assume
from nmigen.back import rtlil
from nmigen.hdl import Fragment


class Buggy(Elaboratable):
    def __init__(self):
        self.data_in = Signal()
        self.do_write = Signal()
        self.mem = Signal()

    def elaborate(self, _):
        m = Module()

        with m.If(self.do_write):
            m.d.ph2 += self.mem.eq(self.data_in)

        return m

    @classmethod
    def formal(cls):
        m = Module()
        buggy = Buggy()
        m.submodules += buggy

        ph2 = ClockDomain("ph2")

        m.domains += ph2
        m.d.sync += ph2.clk.eq(~ph2.clk)

        # We expect that the data in mem does not change,
        # except when it is written to.
        saved_data = Signal()
        # Apparently "initial" is a reserved word, so I changed this to "fafa"
        fafa = Signal(reset=1, reset_less=True)
        m.d.sync += fafa.eq(0)

        with m.If(buggy.do_write):
            m.d.ph2 += saved_data.eq(buggy.data_in)

        with m.If(fafa):
            m.d.comb += Assume(saved_data == buggy.mem)
        with m.Else():
            m.d.comb += Assert(saved_data == buggy.mem)

        return m, [buggy.do_write, buggy.data_in, buggy.mem, saved_data, ph2.clk]


if __name__ == "__main__":
    design, ports = Buggy.formal()
    fragment = Fragment.get(design, None)
    output = rtlil.convert(fragment, ports=ports)
    with open("toplevel.il", "w") as f:
        f.write(output)

We get this trace:

So I wanted to know why saved_data$next was 1 when it shouldn't be. Well, it should, but only when we're about to see the positive edge of ph2, and we don't have that.

Here's toplevel.il.zip.

  process $group_2
    assign \saved_data$next \saved_data
    attribute \src "buggy.py:38"
    switch { \do_write }
      attribute \src "buggy.py:38"
      case 1'1
        assign \saved_data$next \data_in
    end
    attribute \src "/home/robertbaruch/.local/lib/python3.8/site-packages/nmigen/hdl/xfrm.py:519"
    switch \ph2_rst
      case 1'1
        assign \saved_data$next 1'0
    end
    sync init
      update \saved_data 1'0
    sync posedge \ph2_clk
      update \saved_data \saved_data$next
  end

So saved_data should never get updated from saved_data$next unless there's a positive edge on ph2_clk. However, we have no such positive edge. Nevertheless, it did get updated, and that is the thing that makes no sense.

[RobertBaruch]

Interestingly, generating to Verilog (and adding (* gclk *) to before input clk;) causes BMC to succeed. So we have another example of RTLIL failing BMC while Verilog succeeds.

[whitequark]

Looks like there's some fundamental misunderstanding I have about the way SymbiYosys works. Unfortunately its internals are effectively undocumented.

[RobertBaruch]

:< The real reason I'm generating to RTLIL is that you told me once that the translation to Verilog when doing formal wasn't accurate or didn't work or something. I could just stick to generating to Verilog and editing to add (* gclk *) as a workaround.

[whitequark]

That means things will remain subtly broken in a way that happens to pass BMC for you, not that it will actually fix everything. What's necessary is to figure out why the behavior differs, not to switch to the easiest workaround without understanding why it appears to work.

[daveshah1]

Looks to me like the problem here is %co* selects the fanout cone not just of clk but also all the cells driven by clk, and so on, recursively, blasting too many $dffs to $ffs.

I think %co not %co* is what you want here but I'm not 100% sure.

[RobertBaruch]

BTW, I changed back to generating RTLIL, but without the sby workaround provided in #526, and then BMC passed.

[RobertBaruch]

Looks to me like the problem here is %co* selects the fanout cone not just of clk but also all the cells driven by clk, and so on, recursively, blasting too many $dffs to $ffs.

I think %co not %co* is what you want here but I'm not 100% sure.

I verified that both this example and the example in #526 work correctly with %co, and that this example does not work with %co* (while the example of #526 still did).

[whitequark]

@RobertBaruch Yeah, @daveshah1 is right. The proper fix to this is to not use sketchy workarounds but address #505.

[RobertBaruch]

@whitequark It's true! I'm not enough of an expert to help, but I can send you support, sympathy, thanks, and some currency if you want :D

[whitequark]

@RobertBaruch After the recent discussion of multiclock, I actually think that getting multiclock to work is easier than I expected. The Past issue however seems like it would result in some of the worst bikeshedding we had so far. :(

[RobertBaruch]

@RobertBaruch After the recent discussion of multiclock, I actually think that getting multiclock to work is easier than I expected. The Past issue however seems like it would result in some of the worst bikeshedding we had so far. :(

Høly Ødin, you weren't wrong there :<