PSL is a linear-time temporal algebra designed for RTL engineering.
»www.project-veripage.com/psl_tutorial_2.php
The always directive is the most frequently used and it specifies that the following property expression should be checked every clock.
The next directive relates successive state properties, as qualified by the clocking event and qualifying guard.
The eventually! directive is for liveness properties that relate to the future.
For hands-on experience, see a previous ACS exercise: »Dynamic validation using Monitors/Checkers and PSL
9: (C) 2008-13, DJ Greaves, University of Cambridge, Computer Laboratory. |