How to Implement Asynchrous Assertion

SystemVerilog
1

Looking to better understand implementation of asynchronous assertions

reference:

The problem statement goes something like “whenever (i.e. asynchronously) L2TxData==L2ErrorData that L2Abort is asserted”.

    property l2errordata;
        @(L2TxData) // i.e. whenever L2TxData changes -> is this correct?
        (L2TxData == L2ErrorData) -> L2Abort == 1
    endproperty 
    L2Error_Data: assert property(l2errordata);

Is above implementation correct? is “@(L2TxData)” permitted?
I am only used to implementing “@posedge clk” or “@posedge signal_1bit”.

2

In reply to dvier:
requirement: “whenever (i.e. asynchronously) L2TxData==L2ErrorData that L2Abort is asserted”.
Suggested code (Has issues though)


property l2errordata;  // [Ben] has bugs
        @(L2TxData) // i.e. whenever L2TxData changes -> is this correct?
        (L2TxData == L2ErrorData) -> L2Abort == 1
    endproperty 
    L2Error_Data: assert property(l2errordata);

Is above implementation correct? is “@(L2TxData)” permitted?
I am only used to implementing “@posedge clk” or “@posedge signal_1bit”.

@(data) is allowed because every assertion needs a clocking event. The clocking event is typically an edge of a clock, but it could be other variables.
**NOTE:**At the clocking event, all variables used in the property are sampled in the Preponed Region of that clocking event; this is a time slot before any net or variable has changed state (see SVA evaluation - SystemVerilog - Verification Academy for the evaluation regions).
Issue with this property: With @(L2TxData)(L2TxData == L2ErrorData) , if L2TxData changes from 1’b0 to 1’b1 then the sampling value of L2TxData is 1’b0. I don’t believe that this is what is intended here. When doe L2ErrorData changes value?

Generally, you don’t want to use SVA for asynchronous designs; but if you do, you ned to understand the sampling of the various regions.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

Hi Ben,

Appreciate the input but I don’t think the L2TxData and L2ErrorData is intended to be 1bit.
My assumption is that L2TxData and L2ErrorData are bus data.
Ex.
bit [31:0] L2TxData;
bit [31:0] L2ErrorData;

That is why I am confirming if “@(L2TxData)” is acceptable since its not 1 bit.

Reference:

I am trying to better understand what is the best approach if the requirement is to
implement an asynchronous assertion.

4

In reply to dvier:

@(int_var) is legal

In an assertion, see my notes above. The issue is comparing the sampled values of the signal that changed.