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 i_reset. This reset signal could be either synchronous or asynchronous. For our purposes below, we’ll use a synchronous one. Once you define the i_reset signal, you’d then want to adjust the design to use this signal,

always @(posedge i_clk)
if (i_reset)
	counter <= 0;
else if ((i_start_signal)&&(counter == 0))
	counter <= MAX_AMOUNT - 1'b1;
else if (counter != 0)
	counter <= counter - 1;

The design now has only one initial value, and that for a new f_past_valid signal that we’ll need. We’ll use this signal to calculate whether or not we are examining the first clock tick or not.

`ifdef	FORMAL
	reg	f_past_valid;
	initial	f_past_valid = 0;
	always @(posedge i_clk)
		f_past_valid = 1;

If this is the first clock tick, we assume the reset signal is active.

	always @(*)
	if (!f_past_valid)

Otherwise, if this is not the first clock tick then our assertion is checked as before.

	always @(*)
	if (f_past_valid)
		assert(counter < MAX_AMOUNT);

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.