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

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.

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

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

One Comment

Leave a Reply

Your email address will not be published. Required fields are marked *