Hi
what is the significance of using the $rose statement with the goto operator [->1].
for example:
this is an answer from Ben for an older question
initial ap_a_once_ever: assert property(@ (posedge clk)
rose(a) [->1] |=> strong(a[*1:]) );
rose means check for transition from 0 to 1, and a[->1] means !a[*0:] ##1 a
seems like use of one or the other construct is sufficient to evaluate a changing from 0 to 1. so y need both?
In reply to rlraj_2020:
You are correct, instead of $rose(a) [->1] I could have used a[->1].
As to why I wrote it that way, perhaps because of habit in that I am very cautious in checking that I get the very first instance of a sequence in an antecedent, thus avoiding multiple instances. The $rose(expr) tends to do that when ranges are involved. But you are correct, it is not needed here and a[->1] would be sufficient and even better here since $rose(expr) needs the previous value of the expression.
1800’2017: When these functions are called at or before the simulation time step in which the first clocking event occurs, the results are computed by comparing the sampled value of the expression with its default sampled value
Thanks for bringing this up.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…