The key to understanding what’s going on here lies in understanding how $stable and $past work.

$past, for example, works like a simple registered value.

	reg	_past_o_value;

	always @(posedge i_clk)
		_past_o_value <= o_value;

There’s a couple of things to note in this implementation.

  1. _past_o_value has no initial value. This is why I use an f_past_valid register–to force checks to only take place after the first clock that has given _past_o_value a valid value.

  2. With any temporal property, such as $past, understanding the clock edge is relevant. In this case, $past(o_value) is defined by the clock edge posedge i_clk. If o_value is not synchronous with i_clk, this edge will probably not make any sense–as you can see from the example above.

Now that we know how $past works, let’s go back and look at the quiz question. If you look carefully, you’ll see that just prior to every clock edge I carefully made certain that o_value would be high. That means that every $past(o_value) expression (equivalent to _past_o_value above) would be a constant high value–once the first clock edge had passed.

The next key piece to this quiz is that $stable(X) is equivalent to X == $past(X). Hence, we might rewrite this assertion as:

	always @(posedge i_clk)
	if (f_past_valid)
		assert(o_value == _past_o_value);

using our definition of _past_o_value above.

The final piece is the check register used within the formal engine itself. In this case, that check register would look like:

	reg	assertion_success;

	initial	assertion_success = 1;
	always @(posedge i_clk)
	begin
		assertion_success <= 1;
		if (f_past_valid)
			assertion_success <= (o_value == _past_o_value);
	end

The formal tool will then use this assertion_success register on every time step. If the assertion_success register, associated with a given assertion, is ever zero, then the assertion fails.

	always @(*)
		assert(assertion_success);

Herein lies the problem: the assertion_success register is only ever set on a positive edge of the clock. Just before that edge, the value is always high. Therefore the assertion passes even though o_value changes between clock periods!

If you want to guarantee a value that’s always stable, you might wish instead to use the formal time step for your checks.

	(* gclk *) reg formal_timestep_clock;

	always @(posedge formal_timestep_clock)
	if (f_past_valid)
		assert($stable(o_value));

That should cover everything except how f_past_valid relates. For example, should f_past_valid be set on i_clk or formal_timestep_clock? I’ll leave that last piece, though, as an exercise for the student.