Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Deprecate and remove Past/Rose/Fell/... primitives that are difficult to use correctly #526

Closed
RobertBaruch opened this issue Nov 4, 2020 · 77 comments
Milestone

Comments

@RobertBaruch
Copy link
Contributor

It seems I can write something like m.d.comb += Assert(Past(signal) == 0). If multiclock is off in the sby file, what exactly is Past?

Here's an example. First, example.py:

from nmigen import Signal, Module, Elaboratable, ClockDomain, Mux
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.comb += Cover((example.data_out == 0xAAAAAAAA) & (example.le == 0)
                      & (Past(example.data_out) == 0xBBBBBBBB)
                      & (Past(example.le) == 0))

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

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


if __name__ == "__main__":
    formal()

And, the sby file:

[tasks]
cover
bmc

[options]
bmc: mode bmc
cover: mode cover
depth 10
# With this on, BMC fails.
# With this off, it passes, but cover looks odd.
multiclock on

[engines]
smtbmc z3

[script]
read_ilang toplevel.il
prep -top top

[files]
toplevel.il

This fails BMC when multiclock is on, which kind of makes sense to me, if Past is relative to the last cycle of the global clock. In this case I probably shouldn't be using Past, because really what I want to assert is that data_out is equal to what data_in was, when le was last high.

In that case, do I have to effectively make my own version of Past for the internal clock of the example module?

BMC succeeds when multiclock is off, which also kind of makes sense to me, if signals are not allowed to change except on the positive edge of the global clock. However, now the cover trace looks distinctly odd:

cover

data_out did change on the negative edge of 'le'... but it also changed when le was stable. Is that because I've violated the assumption that there is only one clock in the system and therefore yosys does unspecified behavior?

@whitequark whitequark added the bug label Nov 4, 2020
@whitequark
Copy link
Member

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.

@RobertBaruch
Copy link
Contributor Author

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

@RobertBaruch
Copy link
Contributor Author

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...

@cr1901
Copy link
Contributor

cr1901 commented Nov 5, 2020

@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.

@RobertBaruch
Copy link
Contributor Author

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

@RobertBaruch
Copy link
Contributor Author

RobertBaruch commented Nov 5, 2020

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.

@whitequark
Copy link
Member

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.

@RobertBaruch
Copy link
Contributor Author

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()

@whitequark
Copy link
Member

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

@RobertBaruch
Copy link
Contributor Author

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

@whitequark
Copy link
Member

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

@RobertBaruch
Copy link
Contributor Author

Nope, still fails.

@whitequark
Copy link
Member

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

@RobertBaruch
Copy link
Contributor Author

Indeed!

toplevel.il.zip

@whitequark
Copy link
Member

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.

@RobertBaruch
Copy link
Contributor Author

RobertBaruch commented Nov 5, 2020

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

@whitequark
Copy link
Member

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

@RobertBaruch
Copy link
Contributor Author

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

@whitequark
Copy link
Member

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

@RobertBaruch
Copy link
Contributor Author

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

cover

@RobertBaruch
Copy link
Contributor Author

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!!!

@whitequark
Copy link
Member

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.

@whitequark
Copy link
Member

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

@whitequark whitequark changed the title What is Past relative to when multiclock is off? Past should not be allowed in m.d.comb Nov 5, 2020
@RobertBaruch
Copy link
Contributor Author

No, that fails BMC :(

@whitequark
Copy link
Member

Oh yeah sorry, let me figure out why.

@whitequark
Copy link
Member

@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

@RobertBaruch
Copy link
Contributor Author

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

@whitequark
Copy link
Member

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.

@whitequark
Copy link
Member

@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.

@whitequark
Copy link
Member

whitequark commented Nov 7, 2020

@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
Copy link
Contributor

rroohhh commented Nov 7, 2020

@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.

  1. 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?

@whitequark
Copy link
Member

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.

@awygle
Copy link
Contributor

awygle commented Nov 7, 2020

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.

@whitequark
Copy link
Member

whitequark commented Nov 7, 2020

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.

@rroohhh
Copy link
Contributor

rroohhh commented Nov 7, 2020

@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.

@cr1901
Copy link
Contributor

cr1901 commented Nov 7, 2020

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).

@whitequark
Copy link
Member

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?

@cr1901
Copy link
Contributor

cr1901 commented Nov 7, 2020

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

@whitequark
Copy link
Member

whitequark commented Nov 8, 2020

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)

@anuejn
Copy link
Contributor

anuejn commented Nov 8, 2020

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.

@whitequark
Copy link
Member

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.

@whitequark
Copy link
Member

whitequark commented Jan 31, 2023

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.

@whitequark whitequark changed the title Behavior of Past/Rose/Fell/... is poorly suited for multiclock or asynchronous designs Deprecate and remove Past/Rose/Fell/... primitives that are difficult to use correctly Jan 31, 2023
@whitequark whitequark added this to the 0.4 milestone Jan 31, 2023
@whitequark
Copy link
Member

Deprecated in 0.4; will be removed in 0.5.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

No branches or pull requests

7 participants