In reply to ben@SystemVerilog.us:
Got this interesting response from Ed, a colleague and author of “SVA: The Power of Assertions in SystemVerilog by Eduard Cerny (2014-08-24”
the spec itself is confusing or incomplete. E.g.,
- verify only if start is followed by req then ack does happen until after eop happens? req is after start and strictly before eop?
- does it also have to check for the case when req does not happen, i.e. that eop does happen?
For the first one I think it should be
$rose(start) ##1 req[->1] |=> strong(!ack throughout eop[->1] ##[1:10] ack)
to check for the 2nd case and that eop is a pulse should be done separately
It would be better if liveness could be replaced by some bound on the open-ended interval to make it a safety property.
Ben systemverilog.us