Basic Assertions Examples Part-1

Good assertions speed up debug because they point straight at the moment a rule breaks. The trick is knowing exactly what each operator promises. Below, every example spells out both the passing case and the failing case, since knowing when an assertion fails is what makes it useful.

A simple way to picture it

Think of assertions as rules for a relay race. The delay operator ## is “wait N handoffs, then check.” Implication |-> is “if the first runner starts, the second must be ready now.” Non-overlapping |=> is “if the first runner starts, the second must be ready on the next handoff.” A delay range ##[m:n] is “the baton must arrive somewhere between the m-th and n-th handoff.” And $rose and $fell are the judges who only care about the exact moment a runner goes from standing to sprinting, or the reverse.

1. The ## delay operator

The ##N operator means “N sampling clock edges later.” It lets a sequence require that something happens a fixed number of cycles after something else. Note that ##1 is one clock edge, which is not the same as Verilog’s #1 time delay.

property p_delay;
  @(posedge clk) req ##5 gnt;
endproperty
a_delay: assert property (p_delay);

This says: whenever req is sampled high, then exactly five cycles later gnt must be high. It passes when req is high and gnt is high five cycles on. It fails if req was never high (no attempt matched), or req was high but gnt was low at cycle five.

2. Overlapping implication |->

Read |-> as “if the left side (antecedent) matches, then the right side (consequent) must hold in the same cycle.” If the antecedent does not match, the assertion is simply inactive for that attempt, not a failure.

property p_overlap;
  @(posedge clk) req |-> gnt;   // same-cycle check
endproperty
a_overlap: assert property (p_overlap);

It passes when req is high and gnt is high in that very cycle. It stays inactive when req is low. It fails only when req is high but gnt is low in the same cycle.

3. Non-overlapping implication |=>

The |=> operator moves the check one cycle later: “if the antecedent matches, the consequent must hold on the next cycle.” A useful identity to memorize: |=> is the same as |-> ##1.

property p_nonoverlap;
  @(posedge clk) req |=> gnt;   // next-cycle check
endproperty
a_nonoverlap: assert property (p_nonoverlap);

It passes when req is high and gnt is high on the following cycle. It fails when req is high but gnt is low on the next cycle.

4. Delay ranges ##[m:n]

Real protocols rarely respond in a fixed number of cycles. The range operator ##[m:n] allows a window: the consequent must become true somewhere from m to n cycles after the antecedent. Both m and n must be constants, not variables.

parameter MIN_DELAY = 1;
parameter MAX_DELAY = 3;

property p_range;
  @(posedge clk) req |-> ##[MIN_DELAY:MAX_DELAY] gnt;
endproperty
a_range: assert property (p_range);

It passes when req is high and gnt becomes high at any cycle from 1 to 3 later. It fails when req is high but gnt never goes high within that 1-to-3 window. You can also use ##[1:$] for “eventually”, though that needs care so it does not hang forever.

5. $rose edge detector

The $rose function is true only on the cycle where its argument changed from 0 to 1 between the previous and current sampling edges. It checks a transition, not a level. This matters: a signal that is already high is not “rising”.

property p_rose;
  @(posedge clk) req |-> $rose(gnt);
endproperty
a_rose: assert property (p_rose);

It passes when req is high and gnt just transitioned from 0 to 1 on that edge. It fails when req is high but gnt did not make a 0-to-1 change, even if gnt happens to be high already.

6. $fell edge detector

The mirror image of $rose. The $fell function is true only on the cycle where its argument changed from 1 to 0. Use it to catch de-assertions, such as a busy flag dropping.

property p_fell;
  @(posedge clk) req |-> $fell(gnt);
endproperty
a_fell: assert property (p_fell);

It passes when req is high and gnt just transitioned from 1 to 0 on that edge. It fails when req is high but gnt did not make a 1-to-0 change.

Quick reference table

Common mistakes to avoid

• Confusing ##1 (one clock edge) with #1 (a time delay). Assertions use clock edges.
• Expecting |-> to fail when the antecedent is low. With no antecedent match the attempt is inactive, not failed.
• Using a variable inside ##[m:n]. The bounds must be constants.
• Assuming $rose is true whenever a signal is high. It is true only on the 0-to-1 transition cycle.
• Leaving off the clocking event @(posedge clk), so the tool has no sampling reference.

Expected output, in plain words

For each property, a failing attempt prints the assertion label and, if you added one, your $error message, tagged with the cycle where the attempt started. Passing and inactive attempts stay quiet unless you add a pass action. 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 are the vocabulary for larger checks. To pick the right assertion kind, see immediate vs concurrent assertions, and to attach checks without editing RTL see SVA bind. For revision, browse the interview questions and the full SystemVerilog category.

Frequently asked questions

Share this post: on Twitter on Facebook