SVA Properties IV : Until Property

A property is called “until property” if it uses one of the below until operators.

• until
• s_until
• until_with
• s_until_with

Until properties are categorized as Overlapped & Non-overlapped and Strong & Weak. So overall four different forms of until properties exist.

Weak & Non-Overlapping	until	property_expr1 until property_expr2
Strong & Non-Overlapping	s_until	property_expr1 s_until property_expr2
Weak & Overlapping	until_with	property_expr1 until_with property_expr2
Strong & Overlapping	s_until_with	property_expr1 s_until_with property_expr2

Overlapping and Non-overlapping forms

 
property_expr1 until property_expr2 
property_expr1 s_until property_expr2

Non-overlapping form evaluates to true, if property_expr1 evaluates to true at every clock tick until one clock tick before property_expr2 evaluates to true.
Overlapping form evaluates to true, if property_expr1 evaluates to true at every clock tick until property_expr2 evaluates to true.

 
property_expr1 until_with property_expr2 
property_expr1 s_until_with property_expr2

In both cases, property_expr1 evaluation starts from the first clock tick of the evaluation attempt.

Strong and Weak forms

For strong until property, a current or future clock tick exist at which property_expr2 evaluates to true.
Weak until property evaluates to true if property_expr1 evaluates to true at each clock tick, even if property_expr2 never holds.

Until Property Features

Until property types	Weak & Non-overlapping en until out;	Strong & Non-overlapping en s_until out;	Weak & Overlapping en until out;	Strong & Overlapping en s_until out;
The property evaluates to true if ‘en’ is true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until clock tick at which ‘out’ is true	Yes, But not necessarily including that clock tick	Yes, But not necessarily including that clock tick	Yes	Yes
There exists a current or future clock tick at which ‘out’ is true	If not, ‘en’ should be true for every clock tick	Yes	If not, ‘en’ should be true for every clock tick	Yes
If ‘out’ is true at the starting clock tick of the evaluation attemppt, then ‘en’ need not be true at that clock tick	Yes	Yes	Yes	Yes