Note, I'm generating assert_fail.sv via python3 assert_fail.py generate > assert_fail.sv

Just a quick check, what happens if you use generate -t il >assert_fail.il and then use that in your sby file? This is not currently documented anywhere (yet), but when using nMigen with Yosys (as opposed to vendor toolchains) going through Verilog should generally be avoided.

(That doesn't change anything.)

I'm afraid I do not know, and can't find, how to use Symbiyosys with an rtlil file.

Replace read ... with read_ilang assert_fail.il, that's all.

Still passes the assert, when it shouldn't.

Yep, see above comment. Looking at it now.

I think the problem is that:

reg [7:0] cycle = 0;
always @(posedge clk) begin
    cycle <= cycle + (cycle != 255);
end

is not the same as:

cycle = Signal(8)
m.d.pos += cycle.eq(cycle + (cycle != 255))

Specifically, the cycle register, like everything else in the "pos" clock domain, will be reset when the domain reset signal rises. If you make that cycle = Signal(8, reset_less=True) the two snippets behave the same.

Ah, ok. Yeah, that makes sense. It isn't exactly the same, though, is it? Because then the nMigen source doesn't specify that cycle is zeroed out at init time.

Really what I want is something like

initial assume(cycle == 0);

Because then the nMigen source doesn't specify that cycle is zeroed out at init time.

It does: nMigen doesn't have x, and on FPGAs, reset_less signals still get their reset value (in this case, 0, the default) on bitstream load.

Oh and initial assume(cycle == 0); can be expressed with with m.If(Initial()): m.d.comb += Assume(cycle == 0)

Hmm, what's the equivalent of the Yosys-specific

assume property (x == $initstate);

Is it just

m.d.comb += Assume(x == Initial())

Yes, Initial() is exactly the same thing as initstate.

Hmm, that seems to lead to an error from sby:

SBY 15:38:16 [failme_bmc] base: ERROR: Module `\$initstate' referenced in module `\failme' in cell `\$1' is not part of the design.

It seems to translate

m.d.comb += Assume(rst == Initial())

to

  wire init;
  (* src = "assert_fail.py:37" *)
  input rst;
  \$initstate  \$1  (
    .Y(init)
  );
  assign \$2  = rst == (* src = "assert_fail.py:18" *) init;

Are you still going through SystemVerilog, or are you feeding RTLIL directly to SymbiYosys?

Through SV. I did try it with RTLIL and it was ok, so now I have to add back my tests...

OK, here are the next two pairs that seem equivalent but aren't. We have a do_reset which is set to 1 initially, then 0. There is a cycle_reg which is 1 as long as do_reset is 1, or increments up to 255 otherwise. Finally, cycle is 0 as long as do_reset is 1, or cycle_reg otherwise.

We want rst to remain high while cycle < 2.

The SV source correctly passes, while the nMigen source seems to fail with a warmup failure. Maybe it's because rst has some hidden assumption I don't know about?

nMigen:

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

        do_reset = Signal(reset_less=True)
        cycle_reg = Signal(8, reset_less=True)
        cycle = Signal(8, reset_less=True)
        rst = ResetSignal("pos")

        m.d.comb += Assume(do_reset == Initial())

        with m.If(do_reset):
            m.d.comb += cycle.eq(0)
            m.d.pos += cycle_reg.eq(1)
        with m.Else():
            m.d.comb += cycle.eq(cycle_reg)
            m.d.pos += cycle_reg.eq(cycle_reg + (cycle_reg != 255))

        m.d.comb += Assume(rst == (cycle < 2))
        with m.If(rst == 0):
            m.d.comb += Assert(cycle >= 2)

        return m

SV:

reg do_reset;

assume property (do_reset == $initstate);

reg [7:0] cycle_reg = 0;
wire [7:0] cycle = do_reset ? 0 : cycle_reg;

always @(posedge clk) begin
    cycle_reg <= do_reset ? 1 : cycle_reg + (cycle_reg != 255);
end

always @(*) begin
    assume(rst== cycle < 2);
    if (!rst) assert(cycle >= 2);
end

You can reproduce the Warmup failed if you replace reg do_reset; in your SV code with reg do_reset = 0;

I'm not sure exactly what you're trying to do, so I'm not sure which solution would be appropriate here. Obviously, assigning Initial() to do_reset would work just fine, as would be replacing do_reset with Initial().

Ah, ok, so that's the contradiction in assumptions that's going on: do_reset = Signal(reset_less=True) will have do_reset equal to zero initially, but the Assume(do_reset == Initial()) also requires it to be 1, which causes the warmup failure.

do_reset is simply a convenience to cause all signals to be reset to certain values: cycle to 0, cycle_reg to 1. But if nMigen generates the right thing, then possibly I don't even need a do_reset signal.

Yes. You might want to use m.d.comb += ResetSignal().eq(Initial()) or something like that.

Argh. According to this, rst is never set to 0. The goal here is to force rst to 1 for several cycles, then force it to 0.

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


class Failme(Elaboratable):
    def __init__(self):
        pass

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

        cycle = Signal(8, reset=0)
        rst = ResetSignal("pos")

        m.d.comb += rst.eq(cycle < 2)
        m.d.pos += cycle.eq(cycle + (cycle != 255))

        with m.If(rst == 0):
            m.d.comb += Assert(False)

        return m


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

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

    failme = Failme()

    m = Module()
    m.domains.pos = pos
    m.submodules.failme = failme

    main(m, ports=[clk, rst], platform="formal")

In fact, none of these lines force the failure:

        m.d.comb += rst.eq(cycle < 2)
        # m.d.comb += ResetSignal("pos").eq(cycle < 2)
        # m.d.comb += Assume(ResetSignal("pos") == (cycle < 2))

Yes. You can't drive a domain reset signal from the very domain that it resets, at least not without making the cycle register reset_less.

Ah, yes, that makes sense. Making cycle resetless now works, and all three alternatives above succeed! Thanks for the deep-dive!