Quiz #4: If this counter is never triggered, can we prove it'll never leave zero?

Click here for the answer.

Let’s come back to our simple counter example again (no pun intended at first, enjoyed ever since), and let’s build a quiz from it again.

This time we’ve fixed the issue with the initial value, we’ve chosen to ignore the ASIC designers who will insist our counter requires an initial reset signal (it wouldn’t fit on the slide with a reset, but you can add one if to the puzzle above if it makes you feel better), and we’ve asserted that our counter will never meet or exceed 24. (You may assume the counter has enough of a bit width to reach 24 …) We’ve also brought back the i_start_signal, which will trigger our counter.

Today, though, we want to assume that the start signal is never raised, and having assumed that we want to prove that the counter will remain zero.

Will the assertion below prove that?

always @(posedge i_clk)
	assert($past(counter == 0));