A simple assertion; req implies ack; does not fail

In reply to a72:

  1. *$rose(req) |=> !req[1:10] ##1 ack ##1 !ack;

//  !req[*1:10] ##1 ack ##1 !ack; has many threads
!req[*1] ##1 ack ##1 !ack;
!req[*2] ##1 ack ##1 !ack;
..
!req[*10] ##1 ack ##1 !ack;
// If any of those thread you have the sequence (ack ##1 ack)
// the simulator tries the other threads.
// You may want to consider the use of the first_match().  Thus
$rose(req) |=> first_match(!req[*1:10] ##1 ack) ##1 !ack;
  1. *rose(req) |=> !req[1:10] until ack ##1 !ack;
    I got failures, See Edit code - EDA Playground
    I replaced the req with “a”, and the ack with “b”.
  2. until, s_until
    The Conditions for True Outcome for P1 until P2 are:
    See the table from my SVA book at http://systemverilog.us/vf/until_conditions.png

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
  1. 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/