Technical Resources

Books and References A Practical Introduction to PSL, (Discount coupon for A Practical Introduction to PSL) Cindy Eisner and Dana Fisman Using PSL/Sugar for Formal and Dynamic Verification 2nd Edition, Ben Cohen, Srinivasan Venkataramanan and Ajeetha Kumari Order book at: http://members.aol.com/vhdlcohen/vhdl/index.html PSL/Sugar Quick Reference Card, VHDL Flavor, Ben Cohen PSL/Sugar Quick Reference Card, Verilog Flavor Ben Cohen PSL Golden Reference Guide from Doulos Designer's Guide To PSL by Doulos PSL Tutorial From Esperan PSL Tutorial from Project-Veripage PSL/Sugar Papers Syntactic Optimizations for PSL Verification, To appear in TACAS 2007. The \top, \bot approach for truncated semantics, Accellera Technical Report 2006. Note on the characterization of Until as a fixed-point under clocked semantics, Weizmann technical report 2006. Efficient automata-based assertion-checkers synthesis of PSL properties, HLDVT 2006. Incorporating efficient assertion checkers into hardware emulation, ICCD 2005. The safety simple subset, IBM Verification Conference 2005. Automata construction for on-the-fly model checking PSL safety simple subset, IBM Research Report H-0234, June 2005. Automata construction for PSL, The Weizmann Institute of Science, Technical Report MCS05-04, May 2005. IEEE 1850 PSL: Overview and Status (Forum on Specification & Design Languages, 30 September 2005) IEEE P1850 PSL: The Next Generation (DVCon 2005) PSL and SVA: Two Standard Assertion Languages, Addressing Complementary Engineerins Needs (DVCon 2005) An Operational Semantics for Weak PSL, (FMCAD 2004) Embedding Finite Automata within Regular Expressions, (ISOLA’04) Basic Results on the Semantics of Accellera PSL 1.1 Foundation Language (Accellera Technical Report) PSL in Action – ABV Experience Report (PSL/Sugar Consortium Meeting in DAC '04) Cross-product Functional Coverage Measurement with Temporal Properties-based Assertions (DATE 2003) A Tag-Augmented Temporal Logic Checker (VLSI Design/CAD Symposium, Taiwan, 2003) Validating the PSL/Sugar Semantics Using Automated Reasoning (To be published in the special issue of the Formal Aspects of Computing Journal on Semantic Foundations of Engineering Design Languages) (expected sometime in 2003) The Definition of a Temporal Clock Operator (ICALP 2003, @ Springer-Verlag)(to appear) Reasoning with Temporal Logic on Truncated Paths (CAV 2003, @ Springer-Verlag) (abstract only, full paper to appear) Using HOL to study Sugar 2.0 semantics (TPHOLs 2002) ps (400 KB) , pdf (158 KB) Executing the formal semantics of the Accellera Property Specification Language by mechanised theorem proving (submitted CHARME 2003) ps (1231 KB) , pdf (175 KB) IP Reuse Hardening via Embedded Sugar Assertions (IP-Based SoC Design 2002). pdf (227 KB) , ppt (91 KB)