Always, s_always property examples

In reply to Rahul Patel:

These are mainly used for liveness and safety properties in formal verification. See https://www.win.tue.nl/~jschmalt/teaching/2IMF20/SvaFvTutorialHVC2013.pdf