formal: Produced traces make it look like asserts trigger a clock step too late about yosys HOT 7 OPEN

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.

from yosys.

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

from yosys.

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.

from yosys.

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

from yosys.

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.

from yosys.

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.

from yosys.

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.

from yosys.