Basic Assertions Examples Part-1

System Verilog assertions always help to speed up the verification process and it’s very powerful and widely used in the ASIC verification. Identifying the right set of checkers in the verification plan and implementing them using effective SV assertions helps to quickly catch the design bugs and ultimately helps in high-quality design.

With the ever-increasing complexity of logic design, the test benches are getting ever so complex as well. How can assertions help in designing testbench logic? Let us assume that you need to drive certain traffic to a DUT input under certain conditions. You can design an assertion to check for that condition and upon its detection the FAIL action block triggers, which can be used to drive traffic to the DUT. Checking for a condition is far easier with assertions language than with SystemVerilog alone. Second benefit is to place assertions on verification logic itself. Since verification logic (in some cases) is even more complex than the design logic, it makes sense to use assertions to check testbench logic also.

Let’s start with the basic examples of the Assertions.

1. ## delay assertion:

property hash_delay_prop;
  @(posedge prop_clk) req ##5 gnt;
endproperty

hash_delay_check: assert property (hash_delay_prop);

In above example it checks and passes for the cases such as

1. Signal “req” is asserted high on each clock cycle
2. If “req” is high in a cycle after five clock cycles, signal “gnt” has to be asserted high.

It’s more important to know when your assertion will FAIL. So this ##delay assertion will fail in two conditions when

1. Signal “req” is not asserted high in any clock cycle.
2. Signal “req” asserts high and after five clock cycles signal “gnt” is not asserted high.

2. Single (Overlapped) Implication Operator:

The way to ‘read’ the implication operator is “if there is a match on the antecedent that the consequent will be executed”. If there is no match, consequent(RHS) will not fire and the assertion will continue to wait for a match on the antecedent. The ‘implication’ operator also determines the time duration that will lapse between the antecedent(LHS) match and the consequent execution

property single_implication_prop;
  // Also known as overlapped implication operator
  @(posedge prop_clk) req |-> gnt;
endproperty

single_implication_check: assert property (single_implication_prop);

Referring to the code, the property shows the use of a single (overlapping) implication operator. Note its symbol (|->), which differs from that of the non-overlapping operator (|=>). Overlapping means that when the antecedent(LHS) is found to be true, that the consequent(RHS) will start its execution (evaluation) at the ‘same’ prop_clk cycle.

In the above example, Assertion passes when signal “req” is high and in the same clock cycle, signal “gnt” is high. Assertion remains in an “Inactive” state when signal “a” is not asserted high.

The assertion fails only when signal “req” is asserted high and in the same clock cycle signal “gnt” is not asserted high.

3. Double (Non-Overlapped) Implication Operator:

In contrast, non-overlapping means that when the antecedent(LHS) is found to be true that the consequent(RHS) should start its execution, one clk later.

property double_implication_prop;
  // Also known as non-overlapped implication operator
  @(posedge prop_clk) req |=> gnt;
endproperty

double_implication_check: assert property (double_implication_prop);

Here in the above code If the antecedent(LHS) condition (“req”==1) of the double implication “|=>” is true, check the consequent(RHS) condition (“gnt” == 1) in the next cycle.

The equivalence between overlapping and non-overlapping operators. ‘|=>’ is equivalent to ‘|-> ##1’. Note that ##1 is not the same as Verilog’s #1 delay. ##1 means one clock edge (sampling edge). Hence
‘|-> ##1’ means the same as ‘|=>’.

4. ##[m : n] Clock Delay Ranges:

Since it is quite necessary for a signal or expression to be true in a given range of clocks (as opposed to fix number of clocks), we need an operator that does just the same.

##[m:n] allows the range of sampling clock edges in which to check for the expression that follows it. The below code explains the rules governing the operator.

Note that here also, m and n need to be constants. They cannot be variables.

parameter MIN_DELAY = 1;
parameter MAX_DELAY = 3;

property single_implication_prop;
  // Also known as overlapped implication operator
  @(posedge prop_clk) req |-> ##[MIN_DELAY : MAX_DELAY]gnt;
endproperty

single_implication_check: assert property (single_implication_prop);

Here in the code when signal “req” is asserted high, within given range it checks assertion of signal “gnt”.

Hence, assertion passes when signal “req” is asserted high and within 1 to 3 (MIN_DELAY : MAX_DELAY) clock cycles, signal “gnt” asserts high.

The assertion fails when signal “req” is asserted high and within 1 to 3 clock cycles, signal “gnt” does not assert high.

5. $rose – Edge detector in Property/Sequence:

property rose_prop;
  @(posedge prop_clk) req |-> $rose(gnt);
endproperty

rose_check: assert property (rose_prop);

property ‘rose_prop’ in the above code will PASS because both the ‘req’ and ‘gnt’ signals meet the required behavior of $rose. However, the logic fails because while req meets the requirement of $rose, ‘gnt’ does not change from ‘0’ to ‘1’ between the two clock edges.

In other words, assertion passes when signal “req” is asserted high and in the same clock cycle, a positive edge on signal “gnt” is detected. However, Assertion fails when signal “req” is asserted high, but in the same clock cycle, a positive edge on signal “gnt” is not detected.

6. $fell – Edge Detector in Property/Sequence

property fell_prop;
  @(posedge prop_clk) req |-> $fell(gnt);
endproperty

fell_check: assert property (fell_prop);

Property fell_prop checks when signal “a” asserts high, in the same cycle, it also detects negative edge-on signal “b”.

In the above code, assertion passes when signal “req” is asserted high and in the same clock cycle, negative edge on signal “gnt” is detected.

The assertion fails when signal “req” is asserted high and in the same clock cycle, negative edge on signal “gnt” is not detected.

There are many more operators in the coming posts so stay tuned stay safe and keep sharing knowledge to everyone till than see ya 🙂

Share this post: on Twitter on Facebook