The correct assertion basically says that if the clock didn’t rise, then
the signal shouldn’t change either. Further, the correct assertion must
avoid referencing any
$past() values within any assertions on the initial
timestep. Therefore, while the
!$rose(i_clk) example comes the closest,
even this isn’t quite right.
Let’s walk through these choices.
$fell(i_clk) assertion doesn’t capture what we want. You can see this
in Fig. 1 below.
Here, you can see that
$fell(i_clk) is only ever true if the clock falls.
If ever the clock takes more than two formal timesteps, the
be unconstrained as shown in Fig. 1 above. While unconstrained, the solver
is free to make it take on any value.
!$past(i_clk)) assertion is also similarly wrong. This is shown in
Fig. 2 below.
Here you can see that
!$past(i_clk) only constrains our signal over half
the clock period, not the whole clock period. The second, and worse problem,
is that on the one clock period when we do want to allow
signal to change,
!$past(i_clk) is true. A third more subtle problem is that
isn’t constrained on the initial timestep, and neither is the
function upon with
$stable(signal) depends. As a result, our signal is both
over and underconstrained and far from what we want, and guaranteed to fail
But let’s take a closer look at Fig. 2 for a moment. You’ll then notice that
the one and only clock period we want to allow a change from the previous
period is when the expression,
i_clk && !$past(i_clk), is true. This
expression is equivalent to
$rose(i_clk). Therefore we should be able to
signal be stable all other times or, equivalently, whenever
Now we get to the subtle problem. That is, whether you are using
$fell(i_clk), both internally depend upon
is undefined on the first timestep. There are two ways around this.
Using the Symbiotic EDA Suite, this could be eaxpressed simply with,
In this case, the
1 ##1 will cause the solver to skip the first timestep,
and then perform the check on the second time step where
$stable(), etc. will be valid.
The other way around this would be to use an
f_past_valid construct again.
Using these assertions, you should be able to achieve a waveform similar to the one shown in Fig. 3 below.
Do be careful when doing this, however, since the
gbl_clk isn’t the same as the
f_past_valid that would
be appropriate for
i_clk. This is why I labeled the
in the slide above as
f_past_valid_gbl, to indicate that it’s an
f_past_valid type of signal, but specifically defined for the