OR Construct basics in Concurrent Assertions

SystemVerilog
,
4

In reply to hisingh:


a[*1:2]  ##1 b |-> c; // is  equivalent  to  
(a ##1 b )  or  (a ##1 a ##1 b)  |-> c; // also equivalent to 
((a ##1 b ) |-> c) and ((a ##1 a ##1 b)  |-> c);
 Thread1 |-> c and  Thread2 |-> c; // YES
  1. At each clocking event the two threads start at the same time.
  2. All threads of the antecedent must be tested.
  3. An antecedent thread can be a no-match (yielding vacuity “true vacuously” for that thread)
  4. For an assertion to PASS, there can be no failure in any of the attempted threads.
  5. For a nonvacuous PASS, at least one of the threads in nonvacuous.

If you are really serious about understanding these notions, I stronglyurge you to study my paper: -Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy

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/