
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 |
How can I write an assumption of hold the request till grant in arbiter designs using the above?