Comments (7)
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.
Related Issues (20)
- ABC: execution of command failed return code 139. HOT 3
- Variable Part Selects HOT 5
- ABC: execution of command failed return code 137. HOT 5
- Yosys Optimization Error: Optimization Stuck in PEEPOPT Pass HOT 2
- Yosys Optimization Issue: Process Stuck at OPT_CLEAN Pass HOT 1
- Build issue with abc submodule HOT 2
- Optimization Sequence Induces Synthesis Errors Leading to Simulation Inconsistencies HOT 10
- Optimization Sequence Leads to Functionally Incorrect Synthesis Output in Yosys HOT 1
- Custom Yosys Passes Result in Faulty Synthesis and Simulation Errors HOT 5
- Any plans to add CDC linting? HOT 9
- yosys -sim hangs on multiple writes to the same memory address
- Add support/workaround for flattening `inout` port with tri-state signals HOT 5
- Autoname seems to get stuck in a loop and consume all the memory on the system
- Support quoted strings as arguments to passes HOT 8
- Synchronous-read memory recognized as asynchronous HOT 10
- ERROR: Can't open ABC output file. HOT 3
- memory_libmap creates dangling pins HOT 1
- keep_hierarchy -verbose
- Yosys test segfaults HOT 2
- Preserve `SIGNED` flag on attribute values through RTLIL export/import
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from yosys.