In reply to VE:
Ib the 2 papers mentioned below (see Link to the list of papers and books that I wrote, many are now donated. http://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
or Links_to_papers_books - Google Docs )
True/False: A property is either true or false. There is also the concept of vacuity, and a vacuously true property is considered ‘true’ in the sense that it is not ‘false’.
Consider the following property that has three property threads:
a ##[1:3] b |-> c. For this property to succeed,
- we need at least one thread to succeed nonvacuously and
- no thread to fail.
- there can be vacuously true threads.
a[*1:3] |-> b); // is equivalent to
a[*1] or a[*2] or a[*3] |-> b
so if a is only triggered once before b i.e a |-> b then the assertion ap_3athenb failed ? according LRM a[*1:3] is same as a OR a[*2] OR a[*3]. Does it mean any of a |-> b, a[*2] |->b, a[*3] |-> b in this assertion is true then assertion successes.
The 3 threads are
a[*1] |-> b // of a==1, then b must be 1 or assertion fails
a[*2] |-> b // if a==1 and ##1 a==0, the antecedent is vacuous
// and this thread if vacuously true
a[*3] |-> b / if a==1 and ##1 a==0 and ##2 a==0, the antecedent is vacuous
// and this thread if vacuously true
// Thus, for success you need a, or a##1 a, or a ##1 a ##1 a with b==1
// A vacuous antecedent yields a true (though vacuous) thread.
From my papers:
1 Understanding the SVA Engine Using the Fork-Join Model
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.
2 Reflections on Users’ Experiences with SVA, part 1
Important concepts on EXPRESSING REQUIREMENTS,
Terminology, threads in ranges and repeats in antecedents, multiple antecedents.
I really encourage you to red thru all my papers; they are the results of actual users like you.
BEn