The trick with verifying asynchronous assertions in a synchronous context is that you need to check if the assertion is enabled at the current time. Hence, the inclusion of if (!i_areset_n) at the beginning of the check.

We could go one further if we wanted. Since i_areset_n is low (i.e. asserted) on the initial time step, we don’t really need to check both f_past_valid and $past(i_areset_n). In essence, we just checked f_past_valid on the first check of this process. That would leave us with:

	always @(posedge i_clk)
	if (!i_areset_n)
		assert(a == 0);
	else if ($past(i_areset_n))
		assert(a == $past(something));

Let me also caution you about using the initial assume(!i_areset_n);. Not all tools can handle this. I often find myself instead writing:

	always @(*)
	if (!f_past_valid)
		assume(!i_areset_n);

I don’t normally use asynchronous resets myself. However, since writing this quiz question and its answer, I’ve been given an ASIC design to work on. This design not only requires an asynchronous reset, but it also requires that I not use any initial statements.

My first approach was to verify the design with the initial statements present, and then to remove them on release. This approach did not work at all. The first team to examine the design quickly made it produce ‘x values all over. (This was partially due to my love of Verilator that doesn’t use ‘x at all …) The design would’ve worked, given that actual digital logic only uses ‘0 or ‘1 values. However, ‘x doesn’t act like either ‘0 or ‘1. This forced me to start resetting all of the registers within my design–whether I felt they needed it or not.

A consequence of this is the fact that I started adding reset checks to all of my assertions:

	always @(posedge clk)
	if (i_areset_n)
		assert(whatever);

This new assertion form only checks values when the reset isn’t asserted. Therefore it only checks values after the first time step, and only after any values have been initialized.

This quiet adjustment has worked quite well for me so far–with the one exception above. That exception is that, when needing to check for a $past() value, I still need to check whether or not the reset was active on the last cycle or not.