Basic Assertions Examples Part-2

I hope you started understanding assertions and their operators well with practical examples. Let’s start learning more operators in this post.

Before starting part-2 of assertions operators and their basic examples if you haven’t visited part-1 of basic assertions operators and their examples I highly recommend that please visit that blog post and revise your concepts. https://theartofverification.com/assertions-with-examples/

$stable

$stable(), as the name implies, looks for its expression to be stable between two clock edges (i.e. two sampling edges). It evaluates the expression at the current clock edge and compares it with the value sampled at the immediately preceding clock edge. If both values are the same, the check passes.

Note the use of $stable in a continuous assignment statement. Since continuous assign cannot have an edge behavior, you have to explicitly embed a clocking event with $stable. This is the same rule that applies to other sampled value functions.

property stable_prop;
  @(posedge prop_clk) req |-> $stable(gnt);
endproperty

stable_prop_check : assert property (stable_prop);

Here property stable_prop checks when signal “req” asserts high, it checks for no change in signal “gnt”. It means signal “gnt” should stay as it was in the previous cycle.

In the above example, assertion passes when signal “req” is asserted high and in the same clock cycle, signal “gnt” remains to the same value as in the previous clock cycle.

The assertion fails when signal “req” is asserted high and in the same clock cycle signal, “gnt” is also changed from to 0 to 1 (which is not stable).

Similarly, the assertion would fail if signal “req” is asserted high and in the same clock cycle, signal “gnt” is also changed from 1 to 0 (which is not stable).

$past

While learning the functionality of $stable you might get questions like what if you want to check if the signal has been stable for more than 1 clock? So for that $past () will solve that problem.

$past () is an interesting function. It allows you to go past as many clocks as you wish to. You can check for an ‘expression1’ to have a certain value, the number of clocks (strictly prior time ticks) in the past. Note that number of ticks is optional. If you do not specify it, the default will be to look for ‘expression1’ one clock in the past.

Another caveat that you need to be aware of is when you call $past in the initial time ticks of simulation and there are not enough clocks to go in the ‘past’. For example, you specify “req |-> $past (gnt)” and the antecedent ‘req’ is true at a time ‘0’. There isn’t a clock tick to go in the past. In that case, the assertion will use the ‘initial’ value of ‘gnt’.

property past_prop;
  @(posedge prop_clk) req |-> ($past(gnt,5) == 1'b1);
endproperty

past_prop_check : assert property (past_prop);

Here property past_prop checks when signal “req” asserts high, it checks signal “gnt” was high before 5 clock
cycles. If the second argument is not specified, then by default, $past checks for the signal value in the immediate previous cycle.

In the above example, assertion passes when signal “req” is asserted high and signal “gnt” was asserted high before two clock cycles.

The assertion fails when signal “req” is asserted high and before two clock cycles, signal “b” was not asserted high.

Disable (Property) Operator—‘Disable Iff’

Of course, you need a way to disable a property under conditions when the circuit is not stable (think Reset). That’s exactly what the ‘disable iff’ operator does. It allows you to explicitly disable the property under a given condition. Note that ‘disable iff’ reads as ‘disable if and only if’.

The example is shown below how you can disable an assertion during an active Reset. There is a good chance you will use this Reset based disable method in all your properties throughout the project.

property disable_iff_prop;
  disable iff(prop_rst)
  @(posedge prop_clk) req |-> gnt ;
endproperty

disable_iff_prop_check : assert property (disable_iff_prop);

Here, property disable_iff_prop, remains disabled if signal “prop_rst” is asserted high. If prop_rst is not asserted high, then it checks if signal “req” is asserted high, then in the same cycle, signal “gnt” should also be asserted high.

In the above example, assertion remains disabled as long as prop_rst is asserted high. When prop_rst is not asserted and when signal “req” is asserted high, assertion passes OR fails according to the value of signal “gnt” in the same cycle.

[*m] – Consecutive Repetition Operator

The consecutive repetition operator [*m] sees that the signal/expression associated with the operator stays true for ‘m’ consecutive clocks.

Note that ‘m’ cannot be $ (infinite # of consecutive repetition).

The important thing to note for this operator is that it will match at the end of the last iterative match of the signal or expression.

property consecutive_repetition_prop;
  @(posedge prop_clk) $rose(req) |=> gnt[*5] ##1 enable ;
endproperty

consecutive_repetition_prop_check : assert property (consecutive_repetition_prop);

In the above example property consecutive_repeatation_prop checks when the positive edge is detected on signal “req”, check from next clock onwards, signal “gnt” is asserted high continuously for 5 clock cycles, followed by a high value on signal “enable” in the next cycle.

So, assertion triggers when the positive edge of signal “req” is detected, starting next clock cycle, signal “gnt” is continuously high for 5 clock cycles and in the following clock cycle, signal “enable” is asserted high so assertion finishes with pass status.

An assertion fails as signal “gnt” is asserted low in the cycle following the positive edge on signal “req” and the assertion fails when the positive edge of signal “req” is detected, followed by signal “gnt” asserted high continuously for 5 clock cycles and in the next clock cycle, signal “enable” is not asserted high.

[->m] Non-consecutive GoTo Repetition Operator

This is the so-called non-consecutive goto operator! Very similar to [= m] non-consecutive operator. Note the symbol difference. The goto operator is [->2] acts exactly the same as b[=2]. So, why bother with another operator with the same behavior? It is the qualifying event that makes the difference. Recall that the qualifying event is the one that comes after the non-consecutive or the ‘goto’ non-consecutive operator. I call it qualifying because it is the end event
that qualifies the sequence that precedes for final sequence matching.

In other words, It specifies that an expression matches the number of times specified, not necessarily in the consecutive clock cycles. The matches can be intermittent.

property goto_repetition_prop;
  @(posedge prop_clk) $rose(req) |-> gnt[->5] ##1 enable ;
endproperty

goto_repetition_prop_check : assert property (goto_repetition_prop);

.When the above-mentioned assertion becomes active when the positive edge of signal “req” is detected. It waits for signal “gnt” to be high for 5 clock cycles (not necessarily consecutive cycles), followed by signal “enable” asserted high in the immediate next cycle where assertion passes.

When the positive edge of signal “req” is detected, signal “gnt” is continually (or can be intermediate) high for 5 clocks, but as signal “enable” is not asserted high, following the last occurrence of “b”, the assertion fails.

[=m] – Repetition Non-consecutive operator

Non-consecutive repetition is another useful operator (just as the consecutive operator) and used very frequently. In many applications, we want to check that a signal remains asserted or de-asserted a number of times and that we need not know when exactly these transitions take place

property non_consecutive_repetition_prop;
  @(posedge prop_clk) $rose(req) |-> gnt[=5] ##1 enable ;
endproperty

non_consecutive_repetition_prop_check : assert property (non_consecutive_repetition_prop);

This is very similar to “go to” repetition except that it does not require the last match on the signal repetition to happen in the clock cycle before the end of the entire sequence match.

The assertion will pass in the example when the assertion triggers when the positive edge of signal “req” is detected. It waits for signal “gnt” to be high for 5 clock cycles, followed by signal “enable” asserted high in the next cycle. This behavior is exactly the same as “Go to repetition”.

The assertion will fail in the given example, the assertion triggers when the positive edge of signal “req” is detected. It waits for signal “gnt” to be high for 5 clock cycles, followed by signal “enable” not asserted high, and hence, the assertion fails. This behavior is the same as “Go to repetition”.

There are few more operators remaining which will come in the upcoming posts so stay tuned stay safe and keep sharing knowledge to everyone till than see ya 🙂 

Share this post: on Twitter on Facebook