《IEEE-1850-2005.pdf》由会员分享，可在线阅读，更多相关《IEEE-1850-2005.pdf（153页珍藏版）》请在三一文库上搜索。
1、IEEE Std 1850-2005 1850 TM IEEE Standard for Property Specification Language (PSL) 3 Park Avenue, New York, NY 10016-5997, USA IEEE Computer Society Sponsored by the Design Automation Standards Committee and the IEEE Standards Association Corporate Advisory Group 17 October 2005 Print: SH95358 PDF:
2、SS95358 Copyright The Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without license from IHS -,-,- Copyright The Institute of
3、 Electrical and Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without license from IHS -,-,- IEEE Std 1850-2005 IEEE Standard for Property Specification
4、Language (PSL) Sponsor Design Automation Standards Committee of the IEEE Computer Society and the IEEE Standards Association Corporate Advisory Group Approved 22 September 2005 IEEE-SA Standards Board Copyright The Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under license
5、 with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without license from IHS -,-,- ii Copyright 2005 IEEE. All rights reserved. Grateful acknowledgment is made to Accellera Organization, Inc. for the permission to us
6、e the following source material: Accellera Property Specification Language Reference Manual (version 1.1), Accellera GDL: General Description Language, Accellera, Mar. 2005 Abstract: The IEEE Property Specification Language (PSL) is defined in this standard. PSL is a formal notation for specificatio
7、n of electronic system behavior, compatible with multiple electronic system design languages, including IEEE Std 1076 (VHDL), IEEE Std 1364 (Verilog), IEEE P1666 (SystemC), and IEEE P1800 (SystemVerilog), thereby enabling a common specification and verification flow for multi-language and mixed-lang
8、uage designs. PSL captures design intent in a form suitable for simulation, formal verification, formal analysis, and hybrid verification tools. PSL enhances communication among architects, designers, and verification engineers to increase productivity throughout the design and verification process.
9、 The primary audiences for this standard are the implementors of tools supporting the language and advanced users of the language. Keywords: ABV, assertion, assertion-based verification, assumption, cover, model checking, property, PSL, specification, temporal logic, verification The Institute of El
10、ectrical and Electronics Engineers, Inc. 3 Park Avenue, New York, NY 10016-5997, USA Copyright 2005 by the Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Published 17 October 2005. Printed in the United States of America. IEEE is a registered trademark in the U.S. Paten
11、t +1 978 750 8400. Permission to photocopy portions of any individual standard for educational classroom use can also be obtained through the Copyright Clearance Center. NOTEAttention is called to the possibility that implementation of this standard may require use of subject matter covered by paten
12、t rights. By publication of this standard, no position is taken with respect to the exist- ence or validity of any patent rights in connection therewith. The IEEE shall not be responsible for identifying patents for which a license may be required by an IEEE standard or for conducting inquiries into
13、 the legal valid- ity or scope of those patents that are brought to its attention. Copyright The Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or net
14、working permitted without license from IHS -,-,- iv Copyright 2005 IEEE. All rights reserved. Introduction IEEE Std 1850 Property Specification Language (PSL) is based upon the Accellera Property Specification Language (Accellera PSL), a language for formal specification of electronic system behavio
15、r, which was developed by Accellera, a consortium of Electronic Design Automation (EDA), semiconductor, and system companies. IEEE Std 1850 PSL refines Accellera PSL version 1.1, addressing errata and a few minor technical issues and clarifying how PSL interfaces with various standard electronic sys
16、tem design languages. Notice to users Errata Errata, if any, for this and all other standards can be accessed at the following URL: http:/ standards.ieee.org/reading/ieee/updates/errata/index.html. Users are encouraged to check this URL for errata periodically. Interpretations Current interpretation
17、s can be accessed at the following URL: http:/standards.ieee.org/reading/ieee/interp/ index.html. Patents Attention is called to the possibility that implementation of this standard may require use of subject matter covered by patent rights. By publication of this standard, no position is taken with
18、 respect to the existence or validity of any patent rights in connection therewith. The IEEE shall not be responsible for identifying patents or patent applications for which a license may be required to implement an IEEE standard or for conducting inquiries into the legal validity or scope of those
19、 patents that are brought to its attention. A patent holder or patent applicant has filed a statement of assurance that it will grant licenses under these rights without compensation or under reasonable rates and nondiscriminatory, reasonable terms and conditions to applicants desiring to obtain suc
20、h licenses. The IEEE makes no representation as to the reasonableness of rates, terms, and conditions of the license agreements offered by patent holders or patent applicants. Further information may be obtained from the IEEE Standards Department. This introduction is not part of IEEE Std 1850-2005,
21、 IEEE Standard for Property Specification Language (PSL). Copyright The Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without
22、 license from IHS -,-,- Copyright 2005 IEEE. All rights reserved. v Participants The following is a list of participants in the 1850 PSL Working Group. Harry Foster, Chair and Technical Editor Yaron Wolfsthal, Co-Chair Erich Marschner, Secretary The following members of the individual balloting comm
23、ittee voted on this standard. Balloters may have voted for approval, disapproval, or abstention. The working group gratefully acknowledges the contributions of the following organizations and participants. Without their assistance and dedication, this standard would not have been completed. Organiza
24、tionParticipant AccelleraHarry Foster, Chair Altraverifica Ltd. .Adriana Maggiore CadenceMakarand Joshi Erich Marschner, Secretary Stephen Ward IBMCindy Eisner Dana Fisman Avigail Orni Sitvanit Ruah Yaron Wolfsthal, Co-chair Infineon .Klaus Winkelmann IntelAlex Levin Jasper DA.Johan Alfredsson Johan
25、 Mrtensson Mentor Graphics Stephen Bailey Andrew Seawright Tej Singh NokiaJari Kalinainen Northrop GrummanRichard Wallace Novas Software, Inc.Bassam Tabbara NVidiaJoseph Lu Phillips.Sylvain Boucher ST Microelectronics.Mohamed-Lyes Benalycherif Andrea Fedeli Sun MicrosystemsTom Thatcher SynopsysSurre
26、ndra Dudani Accellera Altraverifica Ltd. Cadence IBM Infineon Intel Jasper DA Mentor Graphics Nokia Novas Software, Inc. NVidia ST Microelectronics Sun Microsystems Synopsys Accellera Cadence IBM Infineon Intel Jasper DA Mentor Graphics Motorola Nokia Synopsys Copyright The Institute of Electrical a
27、nd Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without license from IHS -,-,- vi Copyright 2005 IEEE. All rights reserved. When the IEEE-SA Standards B
28、oard approved this standard on 22 September 2005, it had the following membership: Don Wright, Chair Steve M. Mills, Vice Chair Judith Gorman, Secretary *Member Emeritus Also included are the following nonvoting IEEE-SA Standards Board liaisons: Satish K. Aggarwal, NRC Representative Richard DeBlasi
29、o, DOE Representative Alan Cookson, NIST Representative Jennie Steinhagen IEEE Standards Project Editor Chuck Adams Stephen Berger Mark D. Bowman Joseph A. Bruder Bob Davis Roberto de Marca Boisson Julian Forster* Arnold M. Greenspan Mark S. Halpin Raymond Hapeman Richard J. Holleman Richard H. Hule
30、tt Lowell G. Johnson Joseph L. Koepfinger* Hermann Koch Thomas J. McGean Daleep C. Mohla Paul Nikolich T. W. Olsen Ronald C. Petersen Gary S. Robinson Frank Stone Malcolm V. Thaden Doug Topping Joe D. Watson Copyright The Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under
31、license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without license from IHS -,-,- Copyright 2005 IEEE. All rights reserved. vii Contents 1.Overview 1 1.1 Scope 1 1.2 Purpose. 1 1.2.1Background 1 1.2.2Motivati
32、on 2 1.2.3Goals 2 1.3 Usage . 2 1.3.1Functional specification. 2 1.3.2Functional verification. 3 2.Normative references. 7 3.Definitions, acronyms, and abbreviations 9 3.1 Definitions . 9 3.2 Acronyms and abbreviations . 12 3.3 Special terms 12 4.Organization. 15 4.1 Abstract structure. 15 4.1.1Laye
33、rs. 15 4.1.2Flavors . 15 4.2 Lexical structure 16 4.2.1Identifiers. 16 4.2.2Keywords. 16 4.2.3Operators 17 4.2.4Macros . 22 4.2.5Comments 24 4.3 Syntax 24 4.3.1Conventions . 24 4.3.2HDL dependencies. 25 4.4 Semantics. 29 4.4.1Clocked vs. unclocked evaluation . 29 4.4.2Safety vs. liveness properties.
34、 30 4.4.3Linear vs. branching logic . 30 4.4.4Simple subset. 30 4.4.5Finite-length vs. infinite-length behavior 31 4.4.6The concept of strength 31 5.Boolean layer. 33 5.1 Expression type classes 33 5.1.1Bit expressions. 33 5.1.2Boolean expressions 34 5.1.3BitVector expressions 35 5.1.4Numeric expres
35、sions 35 5.1.5String expressions 36 5.2 Expression forms 36 5.2.1HDL expressions 36 Copyright The Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or ne
36、tworking permitted without license from IHS -,-,- viiiCopyright 2005 IEEE. All rights reserved. 5.2.2PSL expressions. 38 5.2.3Built-in functions. 38 5.2.4Union expressions 44 5.3 Clock expressions 44 5.4 Default clock declaration. 46 6.Temporal layer. 49 6.1 Sequential expressions. 50 6.1.1Sequentia
37、l Extended Regular Expressions (SEREs) . 50 6.1.2Sequences. 57 6.2 Properties. 63 6.2.1FL properties 64 6.2.2Optional Branching Extension (OBE) properties 84 6.2.3Replicated properties . 91 6.3 Property and sequence declarations. 93 6.3.1Parameters 94 6.3.2Declarations . 96 6.3.3Instantiation . 97 7
38、.Verification layer. 101 7.1 Verification directives 101 7.1.1assert 101 7.1.2assume 102 7.1.3assume_guarantee 103 7.1.4restrict 103 7.1.5restrict_guarantee. 104 7.1.6cover. 105 7.1.7fairness and strong_fairness. 105 7.2 Verification units . 106 7.2.1Verification unit binding 107 7.2.2Verification u
39、nit inheritance 109 7.2.3Verification unit scoping rules. 110 8.Modeling layer. 113 8.1 Integer ranges. 113 8.2 Structures. 114 Annex A (normative) Syntax rule summary 115 Annex B (normative) Formal syntax and semantics of IEEE Std 1850 PSL. 129 Annex C (informative) Bibliography. 139 Copyright The
40、Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without license from IHS -,-,- Index 141 Copyright 2005 IEEE. All rights reserv
41、ed.1 IEEE Standard for Property Specification Language (PSL) 1. Overview 1.1 Scope This standard defines the property specification language (PSL), which formally describes electronic system behavior. This standard specifies the syntax and semantics for PSL and also clarifies how PSL interfaces with
42、 various standard electronic system design languages. 1.2 Purpose The purpose of this standard is to provide a well-defined language for formal specification of electronic system behavior, one that is compatible with multiple electronic system design languages, including IEEE Std 1076 (VHDL), IEEE S
43、td 1364 (Verilog), IEEE P18001 (SystemVerilog), and IEEE P1666 (SystemC), to facilitate a common specification and verification flow for multi-language and mixed- language designs. 1.2.1 Background The complexity of Very Large Scale Integration (VLSI) has grown to such a degree that traditional appr
44、oaches have begun to reach their limitations, and verification costs have reached 60%70% of development resources. The need for advanced verification methodology, with improved observability of design behavior and improved controllability of the verification process, has become critical. Over the la
45、st decade, a methodology based on the notion of “properties” has been identified as a powerful verification paradigm that can assure enhanced productivity, higher design quality and, ultimately, faster time to market and higher value to engineers and end-users of electronics products. Properties, as
46、 used in this context, are concise, declarative, expressive and unambiguous specifications of desired system behavior, that are used to guide the verification process. IEEE Std 1850 PSL is a standard language for specifying electronic system behavior using properties. PSL facilitates property-based
47、verification using both simulation and formal verification, thereby enabling a productivity boost in functional verification. 1Numbers preceded by P are IEEE authorized standards projects that were not approved by the IEEE-SA Standards Board at the time this publication went to press. For informatio
48、n about obtaining drafts, contact the Institute of Electrical and Electronics Engineers, Inc. Copyright The Institute of Electrical and Electronics Engineers, Inc. Provided by IHS under license with IEEELicensee=NASA Technical Standards 1/9972545001 Not for Resale, 04/20/2007 10:35:43 MDTNo reproduction or networking permitted without license from IHS -,-,- 2Copyright 2005 IEEE. All rights reserved. IEEE S