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.
There’s a couple of things to note in this implementation.
_past_o_valuehas no initial value. This is why I use an
f_past_validregister–to force checks to only take place after the first clock that has given
_past_o_valuea valid value.
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_valueis 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:
using our definition of
The final piece is the
check register used within the formal engine itself.
In this case, that check register would look like:
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.
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
If you want to guarantee a value that’s always stable, you might wish instead to use the formal time step for your checks.
That should cover everything except how
f_past_valid relates. For
f_past_valid be set on
I’ll leave that last piece, though, as an exercise for the student.