APracticalIntroductiontoPSL

一种面向硬件开发与验证人员的用于硬件设计代码描述和验证的特性描述语言。Cindy eisnerDana fismanA Practical Introduction to PSLpringerTo the memory of my mother, Ruth Sorin RosYour loving kindness and generosity of spiritwill stay with me foreverCETo Dr. Elsa Meryn Fisman, my mother and my guideYour endless love and devotion paved the wayfor me to be the person I am todayDFForewordFunctional verification is hard. Period. No disagreement here. But why is thisso? Consider todays design flow: much of it is more or less automated, fromrTL to netlist to layout to silicon. But all this automation depends uponhaving correct RTL input to start with, and there is little or no automationto help with RTL creation. It is hard enough for a designer to decide whatRTL model he wants to build. and then to describe that RTL model correctlin a hardware description language. It is even more difficult for a verificationengineer, who cant read the designer's mind, to verify that what the designercreated not only represents the rTl model he had conceived, but also thatthe RTL model is an appropriate one for the problem at handWhat makes RTL modeling and verification difficult is concurrency. Iteasy to teach an engineer how to write procedural code that conforms tothe synthesizable subset of a hardware description language. What is hard isunderstanding how the engineer's procedural code interacts with other components in the design over time. In fact, until recently we lacked effectivelanguages to describe concurrent behaviorsThe IEEE 1850 Property Specification Language(PSL) is a language forthe formal specification of concurrent systems. The language is particularlyapplicable for writing assertions about hardware designs. PSL supports multiple verification paradigms- including formal analysis, simulation, and accel-eration/emulation. Furthermore, PSL assertions can be reused across multiplehierarchies of the design, ranging from block-level to system-level, providingverification consistencyPSL is not just another assertion language; it is the industry's first andforemost standard property specification language-the result of over 5 yearsof intense collaboration among verification experts and practitioners. Basedupon the Sugar language from IBM, PSL was initially developed in the ac-celera Formal Verification Technical Committee(FVTC) and became an Ac-celera Standard in May 2003. The language was further refined within theIEEE 1850 Property Specification Language Working Group, resulting in thefirst ieee standard assertion language, IEEE Std 1850M-2005 PSL, in SepViII Forewordtember 2005. The only assertion language formally defined for multiple andmixed design language applications, PSL is widely used for assertion-basedverification todayAssertions are not just used for verification; they act as specifications aswell. Today, assertions in design IP convey information about the usage re-quirements of that IP. Tomorrow, we can expect assertions to become morewidely used in verification planning, as a means of specifying design featuresto test. And in the future, we can expect assertions to be used for definingthe design itself. Just as gate-level design grew out of abstractions used toverify transistor-level netlists, and RTL design grew out of abstractions usedto verify gate-level netlists, assertion-based design is likely to evolve out ofassertion-based verification. So this book can help you understand not onlyone of today's leading-edge verification methodologies, but also the founda-tions for the design methodology of the futureCindy Eisner and Dana Fisman were the two key people who turned IBMSugar into PSL. Their deep understanding of PsLs formal semantics wasinstrumental in both the Accellera and IEEe Psl standardization effortsCindy and Dana have now created the most authoritative source for infor-mation about psl, designed to introduce the language incrementally in aneasily understood fashion. A Practical Introduction to PSL provides a solicfoundation for getting started with PSL todayHarry FosterChair, Accellera Formal Verification Technical Committee(FVTC)Chair, IEEE 1850 Property Specification Language(PSL) Working GroupPrincipal Engineer, Mentor Graphics CorporationErich marschnerCo-Chair, Accellera Formal Verification Technical Committee(FVTC)Secretary, IEEE 1850 Property Specification Language(PSL) Working GroupSenior Architect, Cadence Design SystemsPrefaceThis book describes the Property Specification Language PSL, recently standardized as IeEE Std 1850-2005. PSL provides a way to express properties ofa design. For instance. we can state that every request receives an acknowl-edge, that every acknowledged request receives a grant within four to sevencycles unless the request is canceled first, that two consecutive writes shouldnot be to the same address, or that when we see a read request with tag equalto i, then on the next four data transfers we expect to see a tag of iThe primary audience is engineers involved in the design and verificationof hardware, and we assume some familiarity with the basic vocabulary ofhardware design, including such terms as signal and clock cycle, and withtiming diagrams. Most of the examples are given in the Verilog favor of PSL,but lack of familiarity with Verilog should not interfere with understandingthe examples, which are only slightly affected by the favor and are explainedin detailPSL is a temporal logic, and a secondary audience is students of temporal logic. We expect that the intuitive descriptions of the temporal operatorsprovided in the body of the book will make the formal semantics given in Ajpendix B accessible to beginning students, and that the illustrated examplesead to a deeper understanding of the underlying issuesAcknowledgmentsWe would like to thank Harry Foster, Erich Marschner and Yaron Wolfsthalfor conceiving the idea of this book, and for their help and encouragementduring the course of its writingMany people have contributed to our understanding of the underlyingsues involved in defining a property specification language. For interesting andsometimes provocative discussions over the years, thank you to Roy ArmoniIlan Beer, Shoham Ben-David, John Havlicek, Yoad Lustig, Anthony McIsaacPrefaceErich Marschner, Johan Martensson, Avigail Orni, Amir Pnueli, Ishai rabi-novitz. Yoav Rodeh. Sitvanit Ruah. David Van Campenhout, Moshe Vardiand Karen forayWe thank the members of the Verification Guild for their excellent questions, many of which prompted text in this bookFor the generous contribution of their time reading and providing feedback on early drafts of this book, we would like to thank Andrea FedeliOded Fuhrmann, Anthony McIsaac, Amir Nahir, Dejan Nickovic, avigailOrni, Dmitry Pidan, Michal Rimon, Karen Yorav and Emmanuel ZarpasResponsibility for any errors that might remain belongs of course to us. Ifoufind such an error, please let us know. We would also welcome other commentsand/or criticisms from readersThanks also to Janick Bergeron, Roderick Bloem, Doron Bustan, MikeGordon. Oded Kahana. Avner Landver. Orna Lichtenstein. Enrico MasalaTama Mittleman. Nissim Ofek. Nir Piterman. Sivan Rabinovich. ChaniSacharen. Ohad Shacham. Ellen Yoffa and Avi ZivFor the enormous amount of work they collectively contributed to drivingthe standard that ultimately became PSL, we would like to thank HarryFoster. Erich Marschner and the members of the accellera formal verificationTechnical Committee and of the IEEE-1850 PSL working groupThank you to the ieeE for permission to reprint the BNF and the formalsemantics of Psl from the ieee std 1850-2005We would like to acknowledge the support of the iBM Haifa researchLaboratory, where both of us are currently employed, and of the WeizmannInstitute of Science. where Dana Fisman is a phD studentThank you to our editor Carl Harris, to Deborah Doherty and the rest ofthe author support staff at springer, and to Melissa guasch for her excellentcopyeditingFinally, we would like to thank our families for their patience and supportduring the writing of this bookHaifa, IsraelCindy eisnerRehovot IsraelDana fismanMay 2006Appendices a and b reprinted with permission from IEEE Std 1850-2005IEEE Standard for Property Specification Language(PSL), by IEEE. TheiEEE disclaims any responsibility or liability resulting from the placementand use in the described manner