Click here for the answer.

Sometimes I get so used to dealing with synchronous assertions that I forget there’s a large portion of the community that uses asynchronous assertions. In many ways, asynchronous assertions are easier to deal with formally than synchronous ones. Check out the logic above, and see what you think you might do.

One note: f_past_valid is defined like I normally define it:

	reg	f_past_valid;

	initial	f_past_valid = 1'b0;
	always @(posedge i_clk)
		f_past_valid <= 1'b1;