In reply to peter:
In reply to ben@SystemVerilog.us:
I am confused the meaning of " evaluation attempt". Would you explain to me?
And what is assertion property attempt?
Attempt : When the assertion is attempted at its leading clocking event, it is considered as a start event. In essence, an attempt is the start of an evaluation of an assertion. Assertion statements are started (attempted) at every leading clocking event, unless they are disabled or if they are turned off. If the attempt succeeds, one or more threads for that successful attempt are started, and those threads are independent from previous or future attempts. If the attempt fails, that assertion for that attempt is either vacuous if the property has an implication operator, or it fails if there is no implication in the property.
In summary: An assertion statement starts a new evaluation at every leading every clocking event of the property. Each evaluation is considered an attempt, which is sometimes referred to as “the start”. There is a single attempt of an assertion statement per leading clocking event; thus, each attempt has a life and fate of its own, and it is independent from other attempts.
1800 talks about “evaluation attempt of property expr1”
…there is a clock event in which either the evaluation attempt of property_expr1 or the evaluation attempt of property_expr2 is nonvacuous,
[Ben] This means an evaluation attempt of a property within an assertion. Yes, it is a bit confusing because we generally talk about attempts of assertions, not properties.
[1800]An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.
Consider the property (##1 b ##1 a until c );
When 1800 says … property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.
That means
The “at every clock tick”, you have an evaluation attempt of (##1 b ##1 a)
@t0 evaluate ##1 b ##1 a
@t1 evaluate ##1 b ##1 a
…
@tn evaluate ##1 b ##1 a
and all of these p1 must evaluate to true (vacuously or nonvacuously) until p2 is true (vacuously or nonvacuously). The outcome is based on the values of these evaluations, as addressed in my table.
My take on the until: I would avoid it and replace it with other constructs that are more easy to understand.