search

YosysHQ / yosys

Yosys Open SYnthesis Suite
https://yosyshq.net/yosys/
ISC License
3.3k stars 860 forks source link

formal: Produced traces make it look like asserts trigger a clock step too late #4426

Open NikLeberg opened 3 weeks ago

NikLeberg commented 3 weeks ago

Version

Yosys 0.41 (git sha1 c1ad37779, g++ 13.2.0-23ubuntu4 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

Have SystemVerilog module foo.sv:

module foo (
  input wire clk
);

  (* anyseq *) wire a;

  initial begin
    assume(a == 1'b1);
  end

  always @(posedge clk) begin
    assert(a == 1'b1);
  end

endmodule

and try to run formal verification with sby script foo.sby:

[tasks]
bmc2
bmc3

[options]
mode bmc
bmc2: depth 2
bmc3: depth 3

[engines]
smtbmc --progress yices

[script]
read -formal foo.sv
prep -top foo

[files]
foo.sv

Run the script with sby -f foo.sby bmc2

Expected Behavior

The unconstrained internal signal a is in the first clock (initial block) assumed to be 1. In this initial clock 0, the assume holds. In subsequent steps, the assume is no longer valid (as it's only an initial). The solver can choose a diverent value for a because it is unconstrained with anyseq.

So I expect the formal verification to fail at clock step 1 where the solver could choose the value 0.

Actual Behavior

The verification (when only ran for two steps bmc depth 2 does not fail.

`sby -f foo.sby bmc2` output: ``` sby -f foo.sby bmc2 SBY 11:33:33 [foo_bmc2] Copy '/foo.sv' to '/foo_bmc2/src/foo.sv'. SBY 11:33:33 [foo_bmc2] engine_0: smtbmc --progress yices SBY 11:33:33 [foo_bmc2] base: starting process "cd foo_bmc2/src; yosys -ql ../model/design.log ../model/design.ys" SBY 11:33:33 [foo_bmc2] base: finished (returncode=0) SBY 11:33:33 [foo_bmc2] prep: starting process "cd foo_bmc2/model; yosys -ql design_prep.log design_prep.ys" SBY 11:33:33 [foo_bmc2] prep: finished (returncode=0) SBY 11:33:33 [foo_bmc2] smt2: starting process "cd foo_bmc2/model; yosys -ql design_smt2.log design_smt2.ys" SBY 11:33:33 [foo_bmc2] smt2: finished (returncode=0) SBY 11:33:33 [foo_bmc2] engine_0: starting process "cd foo_bmc2; yosys-smtbmc -s yices --presat --unroll -t 2 --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2" SBY 11:33:33 [foo_bmc2] engine_0: ## 0:00:00 Solver: yices SBY 11:33:33 [foo_bmc2] engine_0: ## 0:00:00 Checking assumptions in step 0.. SBY 11:33:33 [foo_bmc2] engine_0: ## 0:00:00 Checking assertions in step 0.. SBY 11:33:33 [foo_bmc2] engine_0: ## 0:00:00 Checking assumptions in step 1.. SBY 11:33:33 [foo_bmc2] engine_0: ## 0:00:00 Checking assertions in step 1.. SBY 11:33:33 [foo_bmc2] engine_0: ## 0:00:00 Status: passed SBY 11:33:33 [foo_bmc2] engine_0: finished (returncode=0) SBY 11:33:33 [foo_bmc2] engine_0: Status returned by engine: pass SBY 11:33:33 [foo_bmc2] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0) SBY 11:33:33 [foo_bmc2] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0) SBY 11:33:33 [foo_bmc2] summary: engine_0 (smtbmc --progress yices) returned pass SBY 11:33:33 [foo_bmc2] summary: engine_0 did not produce any traces SBY 11:33:33 [foo_bmc2] DONE (PASS, rc=0) ```

When running for three steps, it fails as expected.

`sby -f foo.sby bmc3` output: ``` SBY 11:38:45 [foo_bmc3] Copy '/foo.sv' to '/foo_bmc3/src/foo.sv'. SBY 11:38:46 [foo_bmc3] engine_0: smtbmc --progress yices SBY 11:38:46 [foo_bmc3] base: starting process "cd foo_bmc3/src; yosys -ql ../model/design.log ../model/design.ys" SBY 11:38:46 [foo_bmc3] base: finished (returncode=0) SBY 11:38:46 [foo_bmc3] prep: starting process "cd foo_bmc3/model; yosys -ql design_prep.log design_prep.ys" SBY 11:38:46 [foo_bmc3] prep: finished (returncode=0) SBY 11:38:46 [foo_bmc3] smt2: starting process "cd foo_bmc3/model; yosys -ql design_smt2.log design_smt2.ys" SBY 11:38:46 [foo_bmc3] smt2: finished (returncode=0) SBY 11:38:46 [foo_bmc3] engine_0: starting process "cd foo_bmc3; yosys-smtbmc -s yices --presat --unroll -t 3 --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2" SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Solver: yices SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Checking assumptions in step 0.. SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Checking assertions in step 0.. SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Checking assumptions in step 1.. SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Checking assertions in step 1.. SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Checking assumptions in step 2.. SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Checking assertions in step 2.. SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 BMC failed! SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Assert failed in foo: foo.sv:12.5-12.22 (_witness_.check_assert_foo_sv_12_3) SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Writing trace to VCD file: engine_0/trace.vcd SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Writing trace to Verilog testbench: engine_0/trace_tb.v SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Writing trace to constraints file: engine_0/trace.smtc SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Writing trace to Yosys witness file: engine_0/trace.yw SBY 11:38:47 [foo_bmc3] engine_0: ## 0:00:00 Status: failed SBY 11:38:47 [foo_bmc3] engine_0: finished (returncode=1) SBY 11:38:47 [foo_bmc3] engine_0: Status returned by engine: FAIL SBY 11:38:47 [foo_bmc3] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:01 (1) SBY 11:38:47 [foo_bmc3] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0) SBY 11:38:47 [foo_bmc3] summary: engine_0 (smtbmc --progress yices) returned FAIL SBY 11:38:47 [foo_bmc3] summary: counterexample trace: foo_bmc3/engine_0/trace.vcd SBY 11:38:47 [foo_bmc3] summary: failed assertion foo._witness_.check_assert_foo_sv_12_3 at foo.sv:12.5-12.22 in step 2 SBY 11:38:47 [foo_bmc3] DONE (FAIL, rc=2) ```

The produced trace trace.vcd seems to hint IMHO that it could trigger the assert one clock earlier. But it doesnt. image

An equivalent testbench in VHDL+PSL, ran with the ghdl plugin does stop as expected at clock step 1.

NikLeberg commented 3 weeks ago

Same behaviour with just a simple reset:

module foo(
  input wire reset,
  input wire clk
);

  initial begin
    assume(reset);
  end

  always @(posedge clk) begin
    assert(reset);
  end
endmodule

image

jix commented 3 weeks ago

This is the intended behavior for an assert in an always @(posedge clk) block as the effects of such a block affect the following cycle. You can use asserts in an always @* block if you want an assertion to trigger immediately and not with the next clock edge.

georgerennie commented 3 weeks ago

You can also use chformal -assert -early to move assertions that are on the output of an FF like this early.

Having said this it has never been clear to me why Yosys does add a flop to the assertion for this case, it seems to me it should act as a blocking assignment in a clocked block does and trigger at the point that it is reached.

16.3 in the LRM (1800-2023) says

The immediate assertion statement is a test of an expression performed when the statement is executed in the procedural code. The expression is nontemporal and is interpreted the same way as an expression in the condition of a procedural if statement. In other words, if the expression evaluates to x, z, or 0, then it is interpreted as being false, and the assertion statement is said to fail. Otherwise, the expression is interpreted as being true, and the assertion statement is said to pass or, equivalently, to succeed.

There are two modes of immediate assertions, simple immediate assertions and deferred immediate assertions. In a simple immediate assertion, pass and fail actions take place immediately upon assertion evaluation.

Which to me suggests that really it should be evaluated at that point rather than flopped. This would bring the semantics in line with simulation where the assertion would be evaluated at the earlier point too

jix commented 3 weeks ago

But it does trigger at the point it is reached, if you remove one full time step from the traces in this issue report, there would be no rising clock edge left for which the assertion fails. The reason the trace looks different from a simulation trace is that a single FV step corresponds to a full cycle consisting of the clock's rising edge, it being high for half a period, a falling edge and it being low for half a period. In particular a FV step does not include a final rising edge.

If the assertion wouldn't be flopped, including when running chformal -assert -early, you can get incorrect results, as the assertion then triggers even when there is no clock edge for the duration of which the assert condition is false. The easiest way to observe this is with the multiclock on SBY option corresponding to the clk2fflogic yosys pass, which changes a FV step to consist of optional arbitrary clock edges followed by being stable for one period. With this you can have FV steps without clock edges but where the condition of the assertion changes multiple times in the middle of a clock cycle. (In multiclock mode the emitted trace would look slightly different, but still be longer than for an event based simulation but only by half a clock cycle, i.e. you would have the rising clock edge that triggers the assertion followed by the high period, but no falling clock edge.)

I think the main UX issue is that event based simulations exit as soon as the assertion is violated and with that they can end on a clock edge while FV traces always show full steps with signals changing only at the start of the step (with exception of the global clock in single clock mode which falls in the middle of the step to be able to rise again at the start of the next step).

One solution would be to always shorten the last emitted FV step in traces to only include any signal edges at the start, but not any following stable period. This would match what you get from event based simulation, that aborts during an assertion, but also makes it harder to see those final signal edges.

I think a better approach would be to partially shorten the last emitted FV step in the trace, so it doesn't include the implicit falling global clock edge, but still the period where the global clock is high making it easy to read the post-rising-clock-edge signal values, and then also include an event for each assertion in the trace that shows the time when an assertion is violated. This would also be useful if you use the option to append further steps after a failing assertion or for cover traces where multiple covers might be reached at different times.

georgerennie commented 3 weeks ago

Ahh yes I see your point about multiclock. It seems like this is an issue because the $assert etc cells don't store a trigger event so by adding a flop you are synchronising them to the flop's clock I guess. I don't see why this couldn't be avoided in the general case but I do get why it isn't feasible with these current cells (I had also thought that clk2fflogic worked by feeding FFs the global clock gated by free-running enables for each real clock, rather than by detecting rising edges in free-running clocks).

I would agree about those UX solutions (having an event for assertion failure in particular is nice I think), although perhaps even just having clearer documentation on this being a thing would be enough.

NikLeberg commented 1 week ago

With the given rationale, this if fine for me. I'd like it to be documented somewhere. Albeit having this issue here makes it discoverable for others with the same observation.

For me this could be closed. Feel free to do so.

jix commented 1 week ago

Even with this working as currently intended, I think this behavior is confusing enough for new users that I'll keep this issue open until we addressed this in some way. This might end up being better documentation, but I think there is likely more that can be done to improve the overall user experience.