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.

always @(*)
	assert final(something);

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 counter 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 here.

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 2+3 or 5. This following value isn’t tested, but rather only the counter when counter == 2.

As a result of all of the above, this design will not pass a formal check.