What you're hitting is definitely a bug. I'll need a bit of time to dig into it and figure out exactly what's happening.

I'm grateful that you're looking into this. Thank you!!! <3

BTW, I suspect that what should be happening is that Past, Fell, Rose, Stable, and Sample should be forbidden in the combinatorial domain, based on Claire's documentation for SymbiYosys:

• always @(posedge <clock>)
The second form of immediate assertion is one within a clocked always block. This form of assertion is required
when attempting to use the $past, $stable, $changed, $rose, or $fell SystemVerilog functions discussed in the next section.

As for Past relative to local clocks, I think I should be using the gclk attribute is called for, as in the SymbiYosys docs:

Accessing the formal timestep becomes important when verifying code in any asynchronous context...
All of this requires the multiclock on line in the SBY options section.
It also requires the (* gclk *) attribute.
To use (* gclk *), define a register with that attribute...

I remember that there was a way to specify signal attributes in nMigen, but I can't for the life of me remember how...

@RobertBaruch You may find this helpful as to "how does the presence/lack of multiclk interact with a single/multiple clocks"?

I don't know offhand if it helps with your specific problem, but I do remember having a lot of qs about multiclk so I wrote down my notes.

@cr1901 It's pretty much what I concluded. At issue here is, I think, nMigen, not SymbiYosys, although I could be wrong.

BTW, I replaced m.d.comb with m.d.sync for the cover and asserts, and then I generated the verilog via generate -t v, and manually edited the file to include (* gclk *) just before input clk;. The thing then passed verification under multiclock on, as expected.

I replaced m.d.comb with m.d.sync for the cover and asserts

Past doesn't really work inside m.d.comb, since it takes the domain for the inner register from m.d.<domain>. That's either a part of this bug, or its entirety. I thought I emitted a diagnostic for that, but evidently not.

Yes, that was also my conclusion. So aside from outputting that diagnostic, the second issue here is that we need a way to specify the gclk annotation for the default sync domain. If I could do that without editing the output file ;) I would be unblocked.

Here is the updated python example. Note I replaced one of the Pasts with Past(..., 2) which is correct when using the global verification clock.

from nmigen import Signal, Module, Elaboratable, ClockDomain, Mux, ClockSignal
from nmigen.build import Platform
from nmigen.asserts import Assert, Fell, Past, Cover
from nmigen.cli import main_parser, main_runner


# Simple example that clocks data in into data out when the
# independent signal -- assumed to be asynchrnous with any
# other clock in the system -- has a negative edge.
#
# Run with:
#
#   python example.py generate -t il > toplevel.il
#   sby -f example.sby
class Example(Elaboratable):
    def __init__(self):
        self.data_in = Signal(32)
        self.data_out = Signal(32)
        self.le = Signal()

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

        internal_clk = ClockDomain("internal_clk", clk_edge="neg", local=True)
        m.domains.internal_clk = internal_clk
        internal_clk.clk = self.le

        m.d.internal_clk += self.data_out.eq(self.data_in)

        return m


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

    m = Module()
    m.submodules.example = example = Example()

    m.d.sync += Cover((example.data_out == 0xAAAAAAAA) & (example.le == 0)
                      & (Past(example.data_out) == 0xBBBBBBBB)
                      & (Past(example.le, 2) == 0))

    with m.If(Fell(example.le)):
        m.d.sync += Assert(example.data_out == Past(example.data_in))

    main_runner(parser, args, m, ports=[
        example.data_in,
        example.le,
    ])


if __name__ == "__main__":
    formal()

Maybe put setattr -set gclk 1 w:clk in your Yosys script for the time being?

Hmm, did I put it in the right place? BMC is still failing:

[tasks]
cover
bmc

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

[engines]
smtbmc z3

[script]
read_ilang toplevel.il
prep -top top
setattr -set gclk 1 w:clk

[files]
toplevel.il

Sorry, I forgot you're in a design context. Try setattr -set gclk 1 top/w:clk.

Nope, still fails.

Can you upload your IL so I can directly try with that?

Indeed!

toplevel.il.zip

I think the command I suggested works correctly; it's more that the annotation doesn't seem to help. Try adding attribute \gclk 32'1 before wire width 1 input 2 \clk in the IL file; that still doesn't pass BMC for me.

Hmm. Here's the .v file if that helps, along with the sby for that. Adding (* gclk *) before the clk signal causes BMC to pass.

[tasks]
cover
bmc

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

[engines]
smtbmc z3

[script]
read -formal toplevel.v
prep -top top

[files]
toplevel.v

toplevel.v.zip

Yeah, I can reproduce that. It's really confusing! Are you sure it passes correctly when you go through Verilog?

I'm not sure how I could tell. I do know that the Cover trace looks absolutely correct.

Ok so this is something about Verilog. This is incredibly stupid, but works:

[tasks]
cover
bmc

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

[engines]
smtbmc z3

[script]
read_ilang toplevel.il
setattr -set gclk 1 top/w:clk
write_verilog toplevelx.v
design -reset
read_verilog -sv toplevelx.v
prep -top top

[files]
toplevel.il

Yikes. There are a lot of intermediate wires in the cover trace now... but I guess I'll take it? Oof!

Also, special thanks to you. I hope this does get fixed without having to do a rewrite, but in the meantime I am definitely unblocked. Thank you!!!

Yikes. There are a lot of intermediate wires in the cover trace now... but I guess I'll take it? Oof!

To be clear this isn't actually a solution I suggest. (Though I think if you use write_verilog -norename the traces will become more bearable.) There's definitely an insidious bug somewhere.

Okay, I figured it out. The gclk attribute causes the Yosys AST frontend to change the netlist such that $dff cells connected to that clock become $ff cells.

Try this:

[script]
read_ilang toplevel.il
prep -top top
clk2fflogic top/w:clk %co

No, that fails BMC :(

Oh yeah sorry, let me figure out why.

@RobertBaruch Ok well that took longer than expected...

[tasks]
cover
bmc

[options]
bmc: mode bmc
cover: mode cover
depth 10
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

Oof. Well, it does work. This is still a workaround, though, right?

Indeed, and a remarkably gross one. Basically what you want is to do s/posedge \clk/global/ in the input RTLIL file (try it, that would work...) The (*gclk*) attribute, $global_clock and all that stuff does nothing whatsoever on RTLIL level.

However it's not entirely clear to me yet what is to be done on nMigen language level. Maybe the sync clock domain on the formal platform should translate in a way that it uses the global clock.

@rroohhh Okay, so there are two problems with this plan, besides the fact that implementing it is a monumental amount of work that would delay usable multiclock formal for at least a year.

1. Nothing else in the language works like that. We never guess the domains of anything; if you don't specify a domain, it's sync.
2. Imagine you are verifying a DUT. Suppose you have an assertion on Past(dut.out). Your suggestion would synthesize (and use one clock domain or some other depending on what happens inside of the DUT!) if dut.out is eventually driven by synchronous logic. But it would become an error if dut.out is tied to a constant inside of DUT. This means the default behavior you are suggesting is effectively useless for any formal spec not written against a closed set of modules.

@awygle

Each signal must be driven from a single domain (right?), and throwing away that information seems potentially ill-advised. See #6 for example as another potentially relevant issue.

This is certainly the case (it is required for soundness, in fact!) but I don't believe it is relevant to the issue at hand.

@rroohhh Okay, so there are two problems with this plan, besides the fact that implementing it is a monumental amount of work that would delay usable multiclock formal for at least a year.

Understood. I don't think this is so important that it would warrant such a large amount of work. I guess I can just try and implement it out of tree.

1. Nothing else in the language works like that. We never guess the domains of anything; if you don't specify a domain, it's sync.

I guess I think always using sync (in Past,...) is so unintuitive to me, that this would not be a problem, but this could be different for others.

2. Imagine you are verifying a DUT. Suppose you have an assertion on Past(dut.out). Your suggestion would synthesize (and use one clock domain or some other depending on what happens inside of the DUT!) if dut.out is eventually driven by synchronous logic. But it would become an error if dut.out is tied to a constant inside of DUT. This means the default behavior you are suggesting is effectively useless for any formal spec not written against a closed set of modules.

Well it could handle constants and signals seperate to avoid that problem, right?

Well it could handle constants and signals seperate to avoid that problem, right?

Right now, nMigen values have a single property that determines how they behave when used in expressions: their shape. Although the shape of expressions generally depends on the shape of all of their arguments, it is ultimately rooted in the shape of signals, and in most statements, you only have to look up the immediate arguments of any expression to figure out where its shape is derived from. The interface of an Elaboratable consists (by convention, though it will become enforceable after #243) of signals, so in the worst case, you have to trace any expression back to its enclosing module.

With your proposal, values gain two more such properties: their domain and their constness. Domain/constness of an expression would depend on domain/constness of every argument, but unlike shape, it does not terminate once you reach a signal. In fact, it does not terminate on any boundary. Given a single module that is a part of a large design, domain/constness of an arbitrary value in it, in the worst case, depends on every other part of the design.

Note that the issue with Past is very different from what's discussed in #6. #6 proposes a correctness check: once implemented, the behavior of designs that pass the check would be exactly the same as before. By considering the design in its entirety, #6 allows me to think less about clock domains. Your proposal, however, changes behavior, so suddenly I have to think more, and not only more but more by an unbounded amount.

Nothing else in the language works like that. We never guess the domains of anything; if you don't specify a domain, it's sync.

[Each signal must be driven from a single domain] is certainly the case (it is required for soundness, in fact!) but I don't believe it is relevant to the issue at hand.

I argue that because each signal must be driven from a single domain, we wouldn't be guessing - it would be completely determined.

Imagine you are verifying a DUT. Suppose you have an assertion on Past(dut.out). Your suggestion would synthesize (and use one clock domain or some other depending on what happens inside of the DUT!) if dut.out is eventually driven by synchronous logic. But it would become an error if dut.out is tied to a constant inside of DUT. This means the default behavior you are suggesting is effectively useless for any formal spec not written against a closed set of modules.

Just because you use the source domain by default doesn't mean you can't specify a domain. I'm also not sure what the alternative to this is that makes sense and doesn't give you (essentially) metastable behavior.

Just because you use the source domain by default doesn't mean you can't specify a domain.

If you have to specify a domain explicitly in order to get local behavior instead of global behavior that depends on the DUT itself, it follows that any well-written formal specification (at least one that can be used against an open set of DUTs) would specify a domain explicitly. In which case there's no point in having the implicit behavior in first place.

This is like if Rust had a safe { } annotation.

@whitequark Ok, I agree, unless other compelling places are found where it would be useful to add constness and the domain to the properties of a expression that determine the behaviour it does not seem worth it to just add that for this.
While it might be intuitive when using Past/Rose/Fell/... on their own the ability to using them in compound statements means it affects every other part of nmigen aswell.

Why do we need to detect that?

My opinion is that if you don't need to add the "force forward progress" assumes, you shouldn't (to ensure the SMT solver checks the maximum number of states for counterexamples).

My opinion is that if you don't need to add the "force forward progress" assumes, you shouldn't (to ensure the SMT solver checks the maximum number of states for counterexamples).

Could you illustrate this with an example?

I'll see what I can do re: converting multiclk.v to nmigen as an example.

Summarizing IRC discussion with @awygle:

• I believe that a specification sub-language that is built around a local transformation (syntactic sugar for sampling an expression's value in a given domain) as a good fit for the core language. I believe that a global analysis that affects behavior is not a good fit for any part for the core language.
• I see Past as a primitive that samples an expression's value in a given domain. That is, Past's control set is determined locally at the point of use.
• @awygle sees Past as a pritimive that samples a signal's value in its own domain. That is, Past's control set is determined globally at the primary inputs of its input cone.
• I agree that @awygle's interpretation is essentially reasonable, and I agree with him that many people will likely arrive at a similar mental model. I believe that implementing such a primitive would be a serious mistake.
• I propose to resolve this by removing Past entirely and replacing it with Sampled (sic!). Sampled would be syntactic sugar for constructing an FF chain driven by the domain specified by its domain= argument. If not specified, the domain is sync.

We currently have Past as an alias to Sample (sic), and Rose/Fell implemented in terms of Sample as well. But Sample doesn't read right in assertions. Compare:

m.d.comb += Assert(cnt == Sample(cnt) + 1)

to:

m.d.comb += Assert(cnt == Sampled(cnt) + 1)

Maybe this is out of scope for this Issue but I think that it would be nice to have the ability to implement something like Sample in downstream code.

Maybe this is out of scope for this Issue but I think that it would be nice to have the ability to implement something like Sample in downstream code.

Completely out of scope. I agree that it would be great to have, but I also think that practically speaking, it is one of the hardest problems to solve in a nice way.

I've discussed this on the Chipflow team meeting on 2023-01-30. We considered that complex SVA assertions are also quite hard to use correctly in Verilog, and that $past/$rose/... functions in Verilog have the same pitfalls as their Amaranth equivalents do.

Given that the conclusion in 2020 was that Past/... should be removed and replaced with something else, and that the currently implemented poor design for Past/... is one of the things I currently consider a blocker for shipping formal as a first-class feature, I think that a reasonable way forward is to remove these primitives (and their associated IR transformations) entirely.

In this case, Amaranth developers looking to use formal property verification can use Assert and Assume by explicitly writing out the controlling expressions in a formal testbench (or in any other code), avoiding the pitfalls described in this issue.

I'm planning to deprecate these primitives in 0.4 and remove them in 0.5.

Deprecated in 0.4; will be removed in 0.5.