Requirement for SVA pass/failure using first_match

SystemVerilog
,
1

Hi All,
I was trying to understand the working of first_match and when does an assertion pass or fail using it .
Here is an example I was trying: edalink

For the first 3 attempts at T:5,15 and 25: first_match( ##[1:5]rdDone) is true at T:35 ( via ##3 rdDone/##2 rdDone/##1 rdDone respectively )

Then after 5 clocks at T:85 , expression (wData == (local_data + 'hFF)) is True. Hence the antecedent has 3 non-vacuous passes at T:85.
As consequent is false , the assertion fails thrice at T:85.

For the 1st attempt at T:5, out of its 5 threads( t1 to t5 ), ##[1:5]rdDone is true for t3,t4 and t5.
For all of t3,t4 and t5: ##5(wData == (local_data + 'hFF)) is true at T:85,95 and 105 resp.

However, the consequent is true only for t5. Yet there is no pass at T:105

Does this mean that using first_match, the consequent is checked only for the 1st non-vacuously true thread ?
i.e Even if another thread has a matching consequent , it goes unnoticed ( eg: t5 for 1st attempt at T:5 )

For the 5th attempt at T:45, the antecedent has 1st non-vacuous pass at T:105.
As the consequent is true at T:105 for the 1st thread, the assertion passes.

So to summarize the working of first_match, can I state the following:
The assertion pass/failure is based Only on the 1st non-vacuously true antecedent.
If the consequent has a match then the assertion passes (eg: attempt at T:45) else it fails (eg: attempts at T:5,15,25,35 )

2

In reply to MICRO_91:

When you use the first_match() function then after the first match of a multithreaded sequence the consequent is tested at the same matching cycle (with the |->) or after one cycle (with the |=>).
If the consequent property is true then the assertion passes, else it fails.
NO OTHER matches are considered after the first match.

On a separate note, it is important to understand the SVA “lingo”. You expressed the following: “…##[1:5]rdDone is true for t3,t4 and t5.”
The correct terminology should be "##[1:5]rdDone is a match for t3,t4 and t5.

I suggest that you read my paper Reflections on Users’ Experiences with SVA, part 1
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva
Important concepts on EXPRESSING REQUIREMENTS,
Terminology, threads in ranges and repeats in antecedents, multiple antecedents.

My other papers also contain lots of important info.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog