In reply to Have_A_Doubt:
I wanted to know what is the correct SVA terminology for the following
- When assertion passes, do we say that the consequent is a match OR consequent is true ?
I address the terminologies in my paper, see link below.
When assertion passes, we say that the consequent as a sequence is a match,
but the consequent as a property is true, and the assertion passes or fails.
- When assertion passes, do we say that intersect/within operator was true OR intersect/within operator was a match ?
- When assertion passes, we say that the property with the intersect/within operator was true; also the sequence with the intersect/within operator was a match.
2 Reflections on Users’ Experiences with SVA, part 1
Important concepts on EXPRESSING REQUIREMENTS,
Terminology, threads in ranges and repeats in antecedents, multiple antecedents.
---- From above link
Terminology
Before getting into the topic of threads, a review of key terms when addressing SVA sequences, properties, and assertions is necessary because these terms are often misused. Let’s “speak” SVA using proper words and grammar:
Match: A sequence is either matched or non-matched; that’s it! It is not addressed as pass/success/fail/true/false, though many users consider a match a pass.
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. Thus, there can be vacuously true threads.
Pass/Fail/Active: An assertion either passes or fails or is active (i.e., not yet completed with a determination of its fate). There are two types of “passes”: vacuous pass and nonvacuous pass. Nonvacuous passes are typically counted by tools and can thus be considered covered. A sequence that is interpreted as a property is never vacuous.
Covered: A property/sequence/expression is considered covered if it passes nonvacuously with the cover property, cover sequence, or cover statements. A covered property is evaluated as strong. Tools provide statistics on passed assertions and assumptions, which can be counted as covered.
Thread: A thread is a search path for the property’s success within an evaluation attempt that starts at the leading clocking event of the property. For example, a bus request that is acknowledged within 1 to 2 cycles has 2 threads: request followed by acknowledge in 1st cycle, or a request followed by acknowledge in 2nd cycles. A sequence is multi-threaded if it includes any of the following operators: and, intersect, or, range delay (e.g., ##[1:3] a), consecutive range repetition (e.g., a[*1:3]), and non-consecutive repetition (e.g., a[->1], a[=1]).
Attempt vs. thread: An attempt is a new evaluation of an assertion, and that assertion starts one or more threads. In some posts, I see people talk about attempts as threads interacting with each other; they don’t! The threads from each successful attempt are separate from other launched threads from other attempts.