ReadID related Assertion

SystemVerilog
,
1

I have following requirement ::

Once a read has been issued , another read for the same readID cannot be re-issued until a readAck with the same ID has returned

I coded the following :: EDA_LINK

I have 2 questions ::

**I expected the assertion to PASS at TIME : 85 whereas I Observe that the assertion PASSes at TIME : 25 .

[Q1] Any suggestions why is it so ?**

**[Q2] not operator changes the strength as per LRM .

  What's  the  strength  of  the  Consequent  in  the  above  code .**
2

In reply to hisingh:
You do not need the use of the not. State what the what IS rather than what is NOT.


property  CheckRead ;
     int  localID ;
      ($rose( read ) , localID = readID )  |=>     
    !($rose(read) && readID==localID) [*1:$] ##0                       
           $rose(readAck)  &&  readAckID ==  localID;    
  endproperty

My corrections:

BTW, you use too many () and too many spaces; it makes the code unreadable.
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

In reply to ben@SystemVerilog.us:

Hi Ben ,

As you pointed using Unary logical negation operator ( ! ) is the correct way .

However I wanted to know how the assertion behaves using not operator ::


  property  CheckRead ;
       int  localID ;
    
  ( $rose( read ) , localID = readID )  |=>  not( $rose( read )  &&  ( readID == localID ) ) [*1:$]    
    
      ##0  ( 1 , $display("TIME : %2t  Part1  Completes ", $time) )
    
      ##0  ( $rose( readAck )  &&  readAckID ==  localID ) 
    
     ##0  ( 1 , $display("TIME : %2t  Part2  Completes ", $time) ) ; 
    
  endproperty

I observe with the Same Stimulus as Original question , neither of the 2 $display() are executed in the consequent .

The Assertion passes at TIME : 25 even though ##0 ( $rose( readAck ) && readAckID == localID ) isn’t True

[Q1] I am not sure why however

[Q2] Also I would like your take on when to use not operator and when should one use negation !