Answer to Quiz #10

The problem with assertions about the $past() is their value prior to the first clock tick. For this reason, we add the check for f_past_valid.

	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(o_REQUEST) && $past(i_STALL))
		// ...

That’s not enough, however, since the reset might’ve been active in the past as well. In the case of a reset, o_REQUEST should then be false. We might therefore rewrite this assertion as,

	always @(posedge i_clk)
	if (!f_past_valid || $past(i_reset))
	begin
		assert(!o_REQUEST);
	else if ($past(o_REQUEST) && $past(i_STALL))
	begin
		assert(o_REQUEST);
		assert($stable(o_REQUEST_DETAILS));
	end

As the slide above points out, you could also do this with a concurrent assertion instead of with immediate assertions. The following concurrent assertion (without the f_past_valid would (just about) check the same thing.

	assert property (@(posedge i_clk)
		(!i_reset)&&(o_REQUEST)&&(i_STALL)
		|=> o_REQUEST && $stable(o_REQUEST_DETAILS));

The slide above recommends using disable iff. This would work as well, although there is a subtle difference when using it. Can you tell what that difference would be? If not, we’ll come back to the topic in Quiz 19.