Basic Assertions Examples Part-2

If you have not seen part one, start with basic assertions examples part 1 for ##, implication, delay ranges, and edge detectors. This assertions post builds on those with the operators you reach for once the basics click.

A simple way to picture it

Imagine watching a traffic light on a timer. $stable is checking “the light did not change since the last tick.” $past is asking “what colour was it five ticks ago?” disable iff is the maintenance switch that pauses all the rules while a worker services the light. And the repetition operators are counting rules: [*m] is “green for five ticks in a row,” [=m] is “green five times, gaps allowed,” and [->m] is the same as [=m] but it also cares about what happens right after the fifth green.

$stable: no change between two edges

$stable(expr) is true when the sampled value of expr at the current clock edge equals its value at the previous edge. It is a sampled-value function, so in a continuous context you must give it a clocking event.

property p_stable;
  @(posedge clk) req |-> $stable(gnt);
endproperty
a_stable: assert property (p_stable);

It passes when req is high and gnt holds the same value it had last cycle. It fails when req is high but gnt changed, either 0 to 1 or 1 to 0.

$past: look back in time

$past(expr, N) returns the value expr had N clock ticks ago. The number of ticks is optional; if you leave it out, it defaults to one cycle back. A caveat: near time zero there may not be enough history, in which case the tool uses the initial value.

property p_past;
  // gnt must have been high 5 cycles before req
  @(posedge clk) req |-> ($past(gnt, 5) == 1'b1);
endproperty
a_past: assert property (p_past);

It passes when req is high and gnt was high five cycles earlier. It fails when req is high but gnt was not high five cycles earlier.

disable iff: pause a property during reset

Read disable iff as “disable if and only if.” It switches a property off while a condition holds, which is almost always reset. You will likely use this reset guard in nearly every property on a project, because a property should not fire while the circuit is not yet stable.

property p_disable;
  disable iff (rst)
  @(posedge clk) req |-> gnt;
endproperty
a_disable: assert property (p_disable);

While rst is high the property is disabled and cannot pass or fail. When rst is low, it behaves normally: if req is high, gnt must be high the same cycle, otherwise it fails.

[*m]: consecutive repetition

The consecutive repetition [*m] requires the expression to stay true for m clock cycles in a row. The match completes at the last of those cycles. Note that m cannot be an infinite $ for consecutive repetition.

property p_consec;
  @(posedge clk) $rose(req) |=> gnt[*5] ##1 enable;
endproperty
a_consec: assert property (p_consec);

It passes when a rising edge on req is followed by gnt high for five consecutive cycles, then enable high in the next cycle. It fails if gnt drops during those five cycles, or if enable is not high in the cycle after.

[->m]: goto (non-consecutive) repetition

The goto operator [->m] requires m matches that need not be consecutive, and the sequence ends exactly on the m-th match. The difference from [=m] is subtle: the goto ends right at the qualifying m-th match, so what comes next is checked immediately after it.

property p_goto;
  @(posedge clk) $rose(req) |-> gnt[->5] ##1 enable;
endproperty
a_goto: assert property (p_goto);

It passes when, after a rising edge on req, gnt is high five times (gaps allowed) and enable is high in the cycle right after the fifth gnt. It fails if enable is not high immediately after that fifth match.

[=m]: non-consecutive repetition

The non-consecutive [=m] also allows gaps, but it does not force the last match to be right before the end of the sequence. Extra idle cycles can sit between the m-th match and what follows, which is the key difference from the goto form.

property p_nonconsec;
  @(posedge clk) $rose(req) |-> gnt[=5] ##1 enable;
endproperty
a_nonconsec: assert property (p_nonconsec);

It passes when gnt is high five times (gaps allowed) after a rising edge on req, then enable follows. It fails when enable does not follow the required matches.

Quick reference table

Common mistakes to avoid

• Using $stable or $past without a clocking event in a continuous context; sampled-value functions need one.
• Calling $past(e,N) too early in simulation and being surprised it returns the initial value; there is not enough history yet.
• Forgetting disable iff (rst), so properties fire during reset.
• Mixing up [->m] and [=m]; the goto ends exactly on the m-th match, the non-consecutive may trail idle cycles.
• Trying to use $ as the count in [*m] consecutive repetition, which is not allowed.

Expected output, in plain words

For each property, a failing attempt prints its label and, if provided, your message, tagged with the cycle where the attempt started; passing and disabled attempts stay quiet. Note: these pass and fail descriptions come from reading the IEEE 1800 semantics, not from a captured simulator run, and log wording varies by tool. Verify on your own simulator.

These operators complete the everyday assertion vocabulary. Revisit part 1 for the basics, see immediate vs concurrent assertions to choose the right kind, and why assertions help for the payoff. More in the interview questions and SystemVerilog category.

Frequently asked questions

Share this post: on Twitter on Facebook