System Verilog Concurrent Assertions

SystemVerilog
,
1

I am trying to understand how would the following assertion behave give the below scenario:
req signal asserts on the 1st posedge of clock and stays high for 2 clock cycles and the gnt signal asserts for only 5th posedge of clock and then desserts on the 6th clock cycle. For the next 32 cycles gnt does not asserts. Will the following assertion fail?

assert (@(posedge clock) req ##[4:32] gnt )
2

In reply to fenil_shah:
I strongly suggest that you read my papers below as they address the concept of attempt and threads.
Your “assert (@(posedge clock) req ##[4:32] gnt )” is incorrect; You meant a concurrent assertion, like
assert property (@(posedge clock) req ##[4:32] gnt ); For this, you can say:

  • At every clocking event you have an attempt, if req==0 the assertion fails
  • If for every successful attempt (req==1) gnt==1 4 to 32 cycles later, then the assertion passes, else it fails.
  • Every attempt is separate and independent from other attempts, and each attempt has a life of its own. You can think of it as blowing soap bubbles; at every clocking event you emanate a new bubble, and that bubble has a life of its own.

You need to understand the concept of vacuity, and threads; my papers explain those concepts.

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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    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

In reply to ben@SystemVerilog.us:
Yes your are correct, I meant the following assertion

assert property (@(posedge clock) req ##[4:32] gnt );

As per your paper the above assertion fails, right?
According the scenario I stated,
There were will be 2 threads spawned when the req stays high for 2 cycles. And the 1st thread will end when the gnt is first asserted on the 5th clock edge. And the thread 2 will cause the failure as the gnt never asserts.

4

In reply to fenil_shah: At every cycle req==0 the assertion fails.

req 0 1 1 0 0 0 0 0 0 0
gnt 0 0 0 0 0 0 1 0 0
Th1   <---------> PASS ##5
Th2.     <----++> PASS ##4.

You need vacuity

assert property (@(posedge clock) 
              req |-> ##[4:32] gnt);
5

In reply to ben@SystemVerilog.us:
This is exactly what I was suspecting. The expectation is to get gnt signal each time the req signal is high. Can you suggest me what updates will required to catch the issue in the following scenario:

req 0 1 0 1 0 0 0 0 0 0 0
gnt 0 0 0 0 0 0 0 1 0 0 0

With the below assertion, this issue will not get caught, right?

assert property (@(posedge clock) 
              req |-> ##[4:32] gnt);
6

In reply to fenil_shah:

see
https://verificationacademy.com/forums/systemverilog/assertion-req-and-gnt-signals

7

In reply to ben@SystemVerilog.us:

Thanks! that solves all my doubts