System Verilog Assertions - Assertion Overlapping

Assertion Overlapping :

- Assertions are checked at every evaluation point.

- If the start condition is true, a new assertion is triggered.

- Many copies of an assertion may be active simultaneously.

Example :

property A0;

@(negedge CLK) REQ |=> ACK;

endproperty

assert property (A0);





Since, the REQ is still high at second negedge of CLK and it triggers an unexpected second assertion.

Note: Assertions must be carefully written to avoid unexpected failures from overlapping.

How this can be avoid OR how can you code a robust assertion ?

- Use built-in functions for detecting value change.

- $rose() and $fell()

- Useful for making properties edge triggered.

- One way to avoid overlapping - $rose(expr) - True if expr has changed value and it is 1 in the current cycle

- $fell() - True if expr has changed value and it is 0 in the current cycle

- $rose() is true for x->1 and z->1 changes

Example :

property ET;

@(negedge CLK) $rose(REQ) |=> ACK;

endproperty

assert property (ET);







Here, at second negedge of CLK , a new assertion is not getting triggered since there is no change in REQ.


Hope, this blog is helpful to understand assertion overlapping, their cons and how they can be avoided.


Please like/share/comment and follow VLSI Excellence for more such interesting blog posts.

Thanks !!!

-----------------------------------------------------Happy Learning -------------------------------------