In general, Verilog imposes no ordering on when
always @(*) blocks are
executed. The only required ordering is that the statements within an
always @(*) block must be executed in order.
This becomes a problem during formal verification, since you typically only want to apply any formal properties to an expression after it has settled, not while it might still be settling.
SystemVerilog provides a solution to this by using “deferred assertions”. These are immediate assertions that also include the “final” keyword to specify that it shall only be applied after everything else has settled.
SymbiYosys takes the extra step of applying “final” to all assertions, so the user never notices this problem. That is, unless you do something crazy like the design above.
In addition, Yosys is not really a simulator but rather a synthesis engine.
As a result, when you assign multiple values to
as in the block above, Yosys gives each of these values its own net–since
each of the wires within the design would be physically different.
Given that SymbiYosys is built on top of Yosys, you’ll get the same renaming
In the design above, the always block is executed in order–statement by
statement. As a result, the assertion is evaluated within the block but
between the assignments before it and the assignments following it.
From the synthesis standpoint, the assertion is applied to the intermediate
network, not the final one. Hence, when the assertion is applied,
counter == 2. A following value of
counter is given the value of
5. This following value isn’t tested, but rather only the
counter == 2.
As a result of all of the above, this design will not pass a formal check.