SVA: throughout vs until

SystemVerilog
, ,
2

In reply to moogyd:

…
There is also the property operator “until_with”. I tried to re-write the above property as

property AP_req_ack ;
$rose(req_i) |-> req_i until_with ack_o ##1 !req_i ;
endproperty : AP_req_ack

However, this doesn’t behave in the same way. The req_i until ack_o seems to work OK, but it doesn’t then check !req_i.

The until_with is a property operator:
property_expr until_with property_expr

An until property of one of the overlapping forms (i.e., until_with, s_until_with) 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, and including a clock tick at which property_expr2 evaluates to true. Thus, for

 (req_i throughout ack_o[->1]) ##1 !req_i

You are requiring that the property (which is a sequence in this case, but a sequence can be a property)req_i==1 until the property (ack_o[->1]) ##1 !req_i) completes. Thus, you are requiring that req_i==1 when it completes AND also in that SAME last cycle req_i==0. Sorry,but that ain’t going to happen!!!
The req_i until ack_o seems to work OK because in the last cycle there is no test for req_i.
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
:)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us