SVA: throughout vs until

In reply to moogyd:

Thanks a lot Ben!
The observed behavior makes more sense now. Although it also shows that I only have quite a superficial understanding of SVA :-(
Steven
p.s. Just out of interest, the example https://www.edaplayground.com/x/39YH behaves differently with Incisive and Riviera Pro. There are different messages in the log.

The different messages is because Riviera displays all messages, vacuous and non-vacuous, whereas Incisive displays only the non-vacuous passes. There should be a switch for Riviera to suppress the vacuous pass action blocks.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us