In reply to plin317:
- The requirements were 100 cycles of no errors, thus the [*1:100] is not correct.
- OK for: $rose(start) |-> done[=1] intersect !error[*100];
- NO on: $rose(start) |-> done[=1] within !error[*100]; // DO NOT USE
NO, that will not woek!
I explain this in my paper Understanding SVA Degeneracy, link below.
In the paper, I presented an actual user case where the requirements stated that between two rises of req starting from the next cycle, there should be one and only one new gnt. Intuitively, or perhaps naively, one would write something like the following property: $rose(req) |=> $rose(gnt)[=1] within $rose(req)[->1]// BAD
Simulation of the above property showed that if failed to throw an assertion error when 2 or more new occurrences of gnt occurred. But why? The culprit is the Nonconsecutive repetition operator [= in combination with the within operator.
https://systemverilog.us/vf/Degeneracy111923Ben.pdf
Ben Cohen