In reply to peter:
NO to your question.
first_match(a_sequence) means that when a match occurs, there is no evaluation of other possible matches FOR THAT ä_sequence. The first_match does not address the consequent in your example.
It only addresses the first match of a sequence that is multi-threaded. In your example
first_match (rose(a) ##[2:] b), if the thread ($rose(a) ##[2] b) is a match, then the other threads (e.g., ($rose(a) ##[3] b), … ($rose(a) ##[N] b)) are not evaluated.
The property where the antecedent thread that matches evaluates its consequent.
All those previous antecedent threads that had no match cause the property for those cases to be vacuous.
first_match($rose(a) ##[2:$] b)|=> c; // IS SAME AS
first_match(
($rose(a) ##2 b) or // thread 1 property
($rose(a) ##3 b) or or // thread 2 property
…
($rose(a) ##n b)) |=> c) // thread n
ANALOGY: I have 3 decks of cards and every 3 seconds I show you a new card.
You are looking for the sequence ACE card followed by KING card. Thus, for 30 seconds I show you a new cards with NO ACEs, but some KINGs.
At time 33 I show you an ACE followed at time 36 by a KING card. THAT is your first match because the ACE folloed by KING came up and it meets the match you were looking for. The fact that the decks may have other ACEs or KINGs is of no significance here. Now the ACE/KING sequence is a precondition (antecedent) for you to win the game. After the ACE you need to check the consequent (maybe lunch is served immediately after that ACE/KING sequence?)
If no lunch, the assertion fails.
:)
Read my previous replies.
I address this in my MUST READ paper
Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- 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) Amazon.com
- A Pragmatic Approach to VMM Adoption
http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip
http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar
- Papers:
- Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy - Reflections on Users’ Experiences with SVA
Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy - SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
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/