Since posting this question on twitter, several individuals have commented to me that initial values are not synthesizable.
This is not necessarily true.
Whether or not initial values are synthesizable depends upon the hardware you are working with. Initial values are very much synthesizable in FPGAs. They are not synthesizable in ASIC design.
If you wanted to adjust this counter so that this assertion would pass in
an ASIC context, you’d need to add a reset signal. Let’s call it
This reset signal could be either synchronous or asynchronous. For our
purposes below, we’ll use a synchronous one. Once you define the
signal, you’d then want to adjust the design to use this signal,
The design now has only one initial value, and that for a new
signal that we’ll need. We’ll use this signal to calculate whether or not we
are examining the first clock tick or not.
If this is the first clock tick, we assume the reset signal is active.
Otherwise, if this is not the first clock tick then our assertion is checked as before.
You can also use Yosys to delay all assertions by a cycle and so avoid needing this check, or even to remove the initial values from within a design, but those are discussions for another day.