In reply to ben@SystemVerilog.us:
A very useful comment by a colleague who particularly does not like the use of the first_match.
Ben, providing a solution with parameterized number vld is a good idea, but not using first_match. I recommended not using it previously. Even PSL does not have the operator. It’s implementation is costly and in formal may not be supported.
The consequent w/o first_match might look like this:
(vld[->1] ##0 (v>0, v=v-1))[*1:] ##1 !vld[*1:] ##0 $rose(ack) ;
That update is available at
Ben