Property Specification Language: Difference between revisions

Revision as of 19:03, 27 December 2022

Latest revision as of 15:33, 7 August 2025

(2 intermediate revisions by 2 users not shown)

Line 1:

{{Short description|Temporal logic}}

'''Property Specification Language''' ('''PSL''') is a [[temporal logic]] extending [[linear temporal logic]] with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of [[regular expressions]] and syntactic sugaring. It is widely used in the hardware design and verification industry, where [[formal verification]] tools (such as [[model checking]]) and/or [[logic simulation]] tools are used to prove or refute that a given PSL formula holds on a given design.

Line 254 ⟶ 255:

*{{Cite book| title = 1850-2010 – IEEE Standard for Property Specification Language (PSL)| doi = 10.1109/IEEESTD.2010.5446004| year = 2010| isbn = 978-0-7381-6255-3}}

**IEC 62531:2012 {{Cite book| title = 62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL)| doi = 10.1109/IEEESTD.2012.6228486| year = 2012| isbn = 978-0-7381-7299-6}}

*{{cite book|doi=10.1007/978-3-540-45069-6_3|chapter=Reasoning with Temporal Logic on Truncated Paths|title=[[Computer Aided Verification]]|volume=2725|pages=27|series=Lecture Notes in Computer Science|year=2003|last1=Eisner|first1=Cindy|last2=Fisman|first2=Dana|author2-link=Dana Fisman|last3=Havlicek|first3=John|last4=Lustig|first4=Yoad|last5=McIsaac|first5=Anthony|last6=Van Campenhout|first6=David|isbn=978-3-540-40524-5|chapter-url=http://www.research.ibm.com/people/e/eisner/papers/cav49.pdf}}

*{{cite book|doi=10.1007/3-540-45061-0_67|chapter=The Definition of a Temporal Clock Operator|title=Automata, Languages and Programming|volume=2719|pages=857|series=Lecture Notes in Computer Science|year=2003|last1=Eisner|first1=Cindy|last2=Fisman|first2=Dana|author2-link=Dana Fisman|last3=Havlicek|first3=John|last4=McIsaac|first4=Anthony|last5=Van Campenhout|first5=David|isbn=978-3-540-40493-4|chapter-url=http://www.cis.upenn.edu/~fisman/documents/EFHMV_ICALP03_full.pdf}}

==External links==

* [http://www.eda.org/ieee-1850 IEEE 1850 working group]

* [https://web.archive.org/web/20051210035642/http://standards.ieee.org/announcements/pr_1850psl.html IEEE Announcement September 2005]

* [http://www.accellera.org/ Accellera]

* [http://www.project-veripage.com/psl_tutorial_1.php Property Specification Language Tutorial]

Line 266 ⟶ 267:

===Books on PSL===

* [http://www.systemverilog.us/psl_info.html Using PSL/Sugar for Formal and Dynamic Verification 2nd Edition, Ben Cohen, Ajeetha Kumari, Srinivasan Venkataramanan]

* [https://www.springer.com/engineering/circuits+%26+systems/book/978-0-387-35313-5 A Practical Introduction to PSL], Cindy Eisner, and [[Dana Fisman]]

{{Programmable Logic}}