I always struggle to know how to formally verify a counter. So often it seems like the logic within it is just plain obvious to me. How do you re-write something that looks obvious?

In the end, I typically build three basic assertions:

  1. Following any reset, the counter should return to zero. Although this counter didn’t have any reset logic, most of the counters I’ve worked with do.
	reg	f_past_valid;

	initial	f_past_valid = 0;
	always @(posedge i_clk)
		f_past_valid <= 1;

	always @(posedge i_clk)
	if (!f_past_valid || $past(i_reset))
		assert(counter <= 0);
  1. Otherwise (and the otherwise is important), if the counter was non-zero then it should be decrementing
	else if ($past(counter) > 0)
		assert(counter == $past(counter)-1);
  1. Don’t forget the induction assertion that the counter never exceeds its bounds!
	always @(*)
		assert(counter <= 21);
  1. Finally, as we are doing here, upon a request the counter should start counting down.
	always @(posedge i_clk)
	if (f_past_valiid && $past(i_start_signal) && $past(counter == 0))
		assert(counter == 21);

Don’t forget to add a reset check if your design includes a reset.

This last assertion could be added to the if-else based assertion above, however you might notice that the more you do so the more the immediate assertion starts to look like the code given above. This isn’t necessarily a good thing, since you might just copy a bug from one place to another. For this reason, I recommend trying to keep your assertions from “looking-like” the logic they are trying to check.

Perhaps the best example that discusses this best on the blog is the example of the ZipTimer. The ZipTimer is a generic timer that I use with the ZipCPU with interrupt generation and even time-sliced multitasking.