In reply to peter:
You DO NOT have 2 antecedents in *first_match(seqa or seqb ) |-> c ,
*You only have ONE antecedent that has 2 sequence threads, both of which start at the same time.
For the property to succeed, the consequent property that follows any of the first matched thread of the antecedent (seqa or seqb) must be true.
If seqa and seqb match in the same cycle, the same thing happens (i.e., the consequent property that follows the any of first matched thread of the antecedent (seqa or seqb) must be true.
Ir does not matter as to which one succeeded first. A tool will short-circuit all other sequence threads evaluation after it found a first match.
In my paper "Reflections on Users’ Experiences with SVA
I describe what a thread is:
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]).
Adding more to the thread definition, that word addresses both: 1) threads in sequences, and 2) threads in properties. That is confusing. Some clarifications:
(seqa or seqb ) |-> c; // property has ONE antecedent and ONE consequent
// * antecedent has 2 sequence threads, seqa and seqb
// * The antecedent is a single sequence (see 1800 as to what represents a sequence)
// * The property has 2 property threads including:
// seqa |-> c, seqb |-> c
// * For the assertion to both property threads must be true and none must fail.
// * A vacuous property is true vacuously
// * For a nonvacuous assertion PASS there must be at least ONE property thread that is
// nonvacuous, and no property thread that fails.
// * A first_march(multithreaded_sequence) picks the first thread and excludes the other threads
// for the evaluation of the property.