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.

The $fell(i_clk) assertion doesn’t capture what we want. You can see this in Fig. 1 below.

Fig 1. $fell(i_clk) doesn't capture when the signal needs to be stable

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 signal will be unconstrained as shown in Fig. 1 above. While unconstrained, the solver is free to make it take on any value.

The !$past(i_clk)) assertion is also similarly wrong. This is shown in Fig. 2 below.

Fig 2. !$past(i_clk) doesn't do it either

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 !$past(i_clk) isn’t constrained on the initial timestep, and neither is the $past(signal) 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 any assertion.

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 insist that signal be stable all other times or, equivalently, whenever !$rose(i_clk).

Now we get to the subtle problem. That is, whether you are using $rose(i_clk) or $fell(i_clk), both internally depend upon $past(i_clk)–something that is undefined on the first timestep. There are two ways around this.

Using the Symbiotic EDA Suite, this could be eaxpressed simply with,

(* gclk *) reg gbl_clk;

assert property (@(posedge gbl_clk)
	1 ##1 !$rose(i_clk) |-> $stable(signal);

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 $rose(), $stable(), etc. will be valid.

The other way around this would be to use an f_past_valid construct again.

(* gclk *) reg gbl_clk;
reg	f_past_valid;

initial	f_past_valid = 0;
always @(posedge gbl_clk)
	f_past_valid <= 1;

always @(posedge gbl_clk)
if (f_past_valid && !$rose(i_clk))

Using these assertions, you should be able to achieve a waveform similar to the one shown in Fig. 3 below.

Fig 3. The correctly constrained behavior

Do be careful when doing this, however, since the f_past_valid that’s appropriate for gbl_clk isn’t the same as the f_past_valid that would be appropriate for i_clk. This is why I labeled the f_past_valid used 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 gbl_clk timestep.