amaranth-lang / amaranth

A modern hardware definition language and toolchain based on Python
https://amaranth-lang.org/docs/amaranth/
BSD 2-Clause "Simplified" License
1.58k stars 174 forks source link

Time-0 race condition for simulation #594

Open RobertBaruch opened 3 years ago

RobertBaruch commented 3 years ago

Minimal test case. simbug.zip

Summary: The Verilog that nMigen outputs can contain time-0 race conditions which cause problems for simulation.

Details:

I'm running through the Zero to Asic course using nMigen. The digital design part assumes you're writing Verilog, runs the code through Icarus Verilog, and then simulates/tests using cocotb. Everything is fine, except I managed to stumble into a Verilog simulation subtlety. Best explained by the Icarus Verilog FAQ:

My "always" statement doesn't trigger at time 0. Is Icarus Verilog broken?

In this case, the bug is most likely in your program, and is probably the most common and unnoticed error in the entire history of Verilog use. Your program probably looks something like this:

reg [7:0] a, b, c;
always @(a or b) c = a + b;
initial begin a = 1; b = 2; end

This is in fact a race condition at time zero. James Lee has this to say:

[T]he bug is the race between the always at time zero getting to the @ and the initial setting the values. A #1 in the initial block before changing a or b should do the trick. I think that most verilog simulators have some sort of trick to catch the changes at time zero. The IEEE 1364-1995 standard is also clear on this issue: the given example leaves c with an unpredictable value at time 0. This is a frightfully common mistake, we've all done it. It often goes unnoticed because compilers often start threads from first (in the source file) to last. It just so happens that Icarus Verilog, by a detail of implementation, starts threads from last to first.

What people don't typically realize is that #0 <statement> has a well defined meaning. I suggest that you preceed statements in your initial processes with a #0 to eliminate the race, like so:

reg [7:0] a, b, c;
always @(a or b) c = a + b;
initial #0 begin a = 1; b = 2; end

This improved version doesn't have a time-0 race--if the initial block is scheduled ahead of the always block, the ``#0'' will tell the scheduler to first yield to all other threads, then continue.

The Verilog generated by nMigen is something like this:

reg [3:0] a = 4'h0;
...
always @* begin
  ... use a here
end

This results in the time-0 race described above. While not synthesizable, manually altering the Verilog resolves the problem:

reg [3:0] a;
initial #0 begin a = 4'h0; end
...
always @* begin
  ... use a here
end

You'd think that you could use a reset signal to reset registers to known states, but that doesn't fix the problem.

I emphasize that this is a simulation issue, not a synthesis issue. I'm honestly not sure what the solution here is. I don't really want to see initial #0 in Verilog for synthesis.

whitequark commented 3 years ago

This is a well known issue. There is a workaround for it that's supposed to be firing here, but doesn't. I'll look into it.

whitequark commented 3 years ago

Wait, no, this is a different, much less well known issue. I've actually never seen this before, but it makes sense:

[T]he bug is the race between the always at time zero getting to the @ and the initial setting the values. A [#0] in the initial block before changing a or b should do the trick.

I don't really want to see initial #0 in Verilog for synthesis.

Why not? I believe that most, possibly all, synthesizers ignore it, to solve exactly this kind of issue. Alternatively, we could guard its use with `ifdef SYNTHESIS.

RobertBaruch commented 3 years ago

Oh, I didn't know that synthesizers would ignore it -- I thought they'd yell and scream about non-synthesizable statements. In that case it's fine to put it in there!

You mean something like this?

`ifndef SYNTHESIS
  initial #0 begin ... end
`endif
RobertBaruch commented 3 years ago

BTW, I found that in the generated Verilog, this will not pass the test:

  (* src = "simbug.py:12" *)
  reg _b = 1'h0;
  initial #0 begin _b = 1'h0; end

But this does:

  (* src = "simbug.py:12" *)
  reg _b;
  initial #0 begin _b = 1'h0; end

As does this:

  (* src = "simbug.py:12" *)
  reg _b;
  initial begin _b = 1'h0; end

Are the last two equivalent?

RobertBaruch commented 3 years ago

Another interesting data point. If I compile simbug.py to rtlil, then use yosys to convert that to verilog via:

yosys> read_ilang simbug.il
yosys> proc
yosys> write_verilog simbug.v

Then the test passes. Presumably because there are no always @* in the output? I dunno.

akukulanski commented 3 years ago

Hi, I ran into this a year ago and I thought it was a bug in Icarus Verilog (my bad), so I reported it here.

There are two possible workarounds that, while none of them is a clean solution, may help someone until this is solved: