amaranth
amaranth copied to clipboard
amaranth-lang
Behavior of Past/Rose/Fell/... is poorly suited for multiclock or asynchronous designs
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:
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?
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.
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$fellSystemVerilog 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.combwithm.d.syncfor 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.
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
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
@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
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.
@RobertBaruch Per discussion with @cr1901, the tentative nMigen platform level solution would be to avoid exposing the global clock at all, but instead add an assumption that at least one clock signal of every unbound (i.e. left to the mercy of the platform) clock domain changes state per global clock cycle.
Something like this Verilog pseudocode:
wire [N:0] clocks_curr = {clk1,clk2,clk3,...,clkN};
reg [N:0] clocks_prev;
always @($global_clock)
clocks_prev <= clocks_curr;
assume (|(clocks_curr^clocks_prev));
Hmm. I'm not sure I follow? In my example, really the only clock I had was that local clock, so it isn't exposed to the top-level module. The other clock was the default clock (sync), which was tied to the global clock. So in the above, you can't assume that the local clock changes state on every global clock cycle. What I really wanted to write was something like:
m.d.global_clock += Assert(something something Past(something) Fell(something) something)