After the feedback I received on this quiz from twitter, I added a reset to the design. Since neither Verilog itself, nor the FPGA implementations built with Verilog, have a problem with `initial statements, the “missing reset” wasn’t the reason why the design would never pass a formal check
No, the problem in this design is the assertion,
If you run the
engine with anything less than
500-22 steps, it will just increment the counter from
a value the design could never reach up to 500 where the assertion
would then fail. This is the reality of
it starts, the registers within your design can have any value that doesn’t
violate your assertions or assumptions.
What you need, shown in the answer above, is a more constraining
assertion, forcing the counter to stay
<= 16'd22. This assertion
will now pass, since it doesn’t let the
engine start in an unreachable state.
This ability of the
engine to start in the middle of a
design, that is to start long after the initial
t=0 time step,
is both a great advantage and a great curse. It’s an advantage because
it allows you to verify designs with extensive timed states within them, such
as this SDRAM
must start with 100uS of idle, in as little as 45 timesteps.
It’s a disadvantage because it requires internal
assertions–to force the design into a valid state.