1、 IEC 62531 Edition 2.0 2012-06 INTERNATIONAL STANDARD Property Specification Language (PSL) IEC 62531:2012(E)IEEE Std1850-2010IEEE Std 1850THIS PUBLICATION IS COPYRIGHT PROTECTED Copyright 2010 IEEE All rights reserved. IEEE is a registered trademark in the U.S. Patent 35.060 PRICE CODEISBN 978-2-83
2、220-106-0Warning! Make sure that you obtained this publication from an authorized distributor. IEEE Std 1850Copyright 2010 IEEE. All rights reserved. ixContents1. Overview 11.1 Scope 11.2 Purpose. 11.2.1 Background 21.2.2 Motivation 21.2.3 Goals 21.3 Usage . 21.3.1 Functional specification.31.3.2 Fu
3、nctional verification. 32. Normative references. 73. Definitions, acronyms, and abbreviations 93.1 Definitions . 93.2 Acronyms and abbreviations . 123.3 Special terms 124. Organization. 154.1 Abstract structure. 154.1.1 Layers. 154.1.2 Flavors . 154.2 Lexical structure 164.2.1 Identifiers . 164.2.2
4、Keywords . 164.2.3 Operators 174.2.4 Macros . 224.2.5 Comments 244.3 Syntax 244.3.1 Conventions . 244.3.2 HDL dependencies. 254.4 Semantics . 294.4.1 Clocked vs. unclocked evaluation . 294.4.2 Safety vs. liveness properties. 304.4.3 Linear vs. branching logic . 304.4.4 Simple subset . 304.4.5 Finite
5、-length vs. infinite-length behavior 314.4.6 The concept of strength 315. Boolean layer . 335.1 Expression type classes 335.1.1 Bit expressions. 335.1.2 Boolean expressions 345.1.3 BitVector expressions 355.1.4 Numeric expressions 355.1.5 String expressions 365.2 Expression forms 365.2.1 HDL express
6、ions36g177g3g76g76g3g177g44g40g38g3g25g21g24g22g20g29g21g19g20g21g3g44g40g40g40g3g54g87g71g3g20g27g24g19g16g21g19g20g19g35.2.2 PSL expressions. 395.2.3 Built-in functions . 395.2.4 Union expressions455.3 Clock expressions 455.4 Default clock declaration . 476. Temporal layer. 496.1 Sequential expres
7、sions. 506.1.1 Sequential Extended Regular Expressions (SEREs) . 506.1.2 Sequences. 576.2 Properties . 636.2.1 FL properties 636.2.2 Optional Branching Extension (OBE) properties 846.2.3 Replicated properties . 906.3 Local variables. 936.4 Procedural blocks. 976.5 Property and sequence declarations.
8、 1036.5.1 Parameters 1046.5.2 Declarations . 1066.5.3 Instantiation . 1077. Verification layer . 1117.1 Verification directives 1117.1.1 assert 1117.1.2 assume 1127.1.3 restrict 1137.1.4 restrict! . 1137.1.5 cover. 1157.1.6 fairness and strong_fairness. 1167.2 Verification units . 1177.2.1 Verificat
9、ion unit binding 1217.2.2 Verification unit instantiation 1217.2.3 Verification unit inheritance 1227.2.4 Overriding assignments . 1248. Modeling layer. 1298.1 Integer ranges. 1298.2 Structures . 1309. Scope and visibility rules. 1319.1 Immediate scope 1319.2 Extended scope 1319.3 Direct and indirec
10、t name references 132Annex A (normative) Syntax rule summary 135Annex B (normative) Formal Syntax and Semantics of IEEE Std 1850 Property Specification Language(PSL) 149Annex C (informative) Bibliography. 167g36g81g81g72g91g3g39g3g11g76g81g73g82g85g80g68g87g76g89g72g12g3g47g76g86g87g3g82g73g3g44g40g
11、40g40g3g51g68g85g87g76g70g76g83g68g81g87g86g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g17g1
12、7g17g17g20g25g28g3g44g40g38g3g25g21g24g22g20g29g21g19g20g21g3g44g40g40g40g3g54g87g71g3g20g27g24g19g16g21g19g20g19 g177g3g76g76g76g3g177g3Property Specification Language (PSL) FOREWORD 1) The International Electrotechnical Commission (IEC) is a worldwide organization for standardization comprising al
13、l national electrotechnical committees (IEC National Committees). The object of IEC is to promote international co-operation on all questions concerning standardization in the electrical and electronic fields. To this end and in addition to other activities, IEC publishes International Standards, Te
14、chnical Specifications, Technical Reports, Publicly Available Specifications (PAS) and Guides (hereafter referred to as “IEC Publication(s)”). Their preparation is entrusted to technical committees; any IEC National Committee interested in the subject dealt with may participate in this preparatory w
15、ork. International, governmental and non-governmental organizations liaising with the IEC also participate in this preparation. IEEE Standards documents are developed within IEEE Societies and Standards Coordinating Committees of the IEEE Standards Association (IEEE-SA) Standards Board. IEEE develop
16、s its standards through a consensus development process, which brings together volunteers representing varied viewpoints and interests to achieve the final product. Volunteers are not necessarily members of IEEE and serve without compensation. While IEEE administers the process and establishes rules
17、 to promote fairness in the consensus development process, IEEE does not independently evaluate, test, or verify the accuracy of any of the information contained in its standards. Use of IEEE Standards documents is wholly voluntary. IEEE documents are made available for use subject to important noti
18、ces and legal disclaimers (see http:/standards.ieee.org/IPR/disclaimers.html for more information). IEC collaborates closely with IEEE in accordance with conditions determined by agreement between the two organizations. 2) The formal decisions of IEC on technical matters express, as nearly as possib
19、le, an international consensus of opinion on the relevant subjects since each technical committee has representation from all interested IEC National Committees. The formal decisions of IEEE on technical matters, once consensus within IEEE Societies and Standards Coordinating Committees has been rea
20、ched, is determined by a balanced ballot of materially interested parties who indicate interest in reviewing the proposed standard. Final approval of the IEEE standards document is given by the IEEE Standards Association (IEEE-SA) Standards Board. 3) IEC/IEEE Publications have the form of recommenda
21、tions for international use and are accepted by IEC National Committees/IEEE Societies in that sense. While all reasonable efforts are made to ensure that the technical content of IEC/IEEE Publications is accurate, IEC or IEEE cannot be held responsible for the way in which they are used or for any
22、misinterpretation by any end user. 4) In order to promote international uniformity, IEC National Committees undertake to apply IEC Publications (including IEC/IEEE Publications) transparently to the maximum extent possible in their national and regional publications. Any divergence between any IEC/I
23、EEE Publication and the corresponding national or regional publication shall be clearly indicated in the latter. 5) IEC and IEEE do not provide any attestation of conformity. Independent certification bodies provide conformity assessment services and, in some areas, access to IEC marks of conformity
24、. IEC and IEEE are not responsible for any services carried out by independent certification bodies. 6) All users should ensure that they have the latest edition of this publication. 7) No liability shall attach to IEC or IEEE or their directors, employees, servants or agents including individual ex
25、perts and members of technical committees and IEC National Committees, or volunteers of IEEE Societies and the Standards Coordinating Committees of the IEEE Standards Association (IEEE-SA) Standards Board, for any personal injury, property damage or other damage of any nature whatsoever, whether dir
26、ect or indirect, or for costs (including legal fees) and expenses arising out of the publication, use of, or reliance upon, this IEC/IEEE Publication or any other IEC or IEEE Publications. 8) Attention is drawn to the normative references cited in this publication. Use of the referenced publications
27、 is indispensable for the correct application of this publication. 9) Attention is drawn to the possibility that implementation of this IEC/IEEE Publication may require use of material covered by patent rights. By publication of this standard, no position is taken with respect to the existence or va
28、lidity of any patent rights in connection therewith. IEC or IEEE shall not be held responsible for identifying Essential Patent Claims for which a license may be required, for conducting inquiries into the legal validity or scope of Patent Claims or determining whether any licensing terms or conditi
29、ons provided in connection with submission of a Letter of Assurance, if any, or in any licensing agreements are reasonable or non-discriminatory. Users of this standard are expressly advised that determination of the validity of any patent rights, and the risk of infringement of such rights, is enti
30、rely their own responsibility. g177g3g76g89g3g177g44g40g38g3g25g21g24g22g20g29g21g19g20g21g3g44g40g40g40g3g54g87g71g3g20g27g24g19g16g21g19g20g19g3International Standard IEC 62531/ IEEE Std 1850-2010 has been processed through IEC technical committee 93: Design automation, under the IEC/IEEE Dual Log
31、o Agreement. This second edition cancels and replaces the first edition, published in 2007, and constitutes a technical revision. The text of this standard is based on the following documents: IEEE Std FDIS Report on voting IEEE Std 1850-2010 93/319/FDIS 93/326/RVDFull information on the voting for
32、the approval of this standard can be found in the report on voting indicated in the above table. The IEC Technical Committee and IEEE Technical Committee have decided that the contents of this publication will remain unchanged until the stability date indicated on the IEC web site under “http:/webst
33、ore.iec.ch“ in the data related to the specific publication. At this date, the publication will be g135 reconfirmed, g135 withdrawn, g135 replaced by a revised edition, or g135 amended. g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3
34、g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g44g40g38g3g25g21g24g22g20g29g21g19g20g21g3g44g40g40g40g3g54g87g71g3g20g27g24g19g16g21g19g20g19 g177g3g89g3g177g3IEEE Std 1850TM-2010(Revision ofIEEE Std1850-2005)IEEE Standard for Property Specification Lang
35、uage (PSL)SponsorDesign Automation Standards Committeeof theIEEE Computer Societyand theIEEE Standards Association Corporate Advisory GroupApproved 25 March 2010IEEE-SA Standards Board g177g3g89g76g3g177g44g40g38g3g25g21g24g22g20g29g21g19g20g21g3g44g40g40g40g3g54g87g71g3g20g27g24g19g16g21g19g20g19g3
36、Grateful acknowledgment is made to Accellera Organization, Inc. for the permission to use thefollowing source material:Accellera Property Specification Language Reference Manual (version 1.1), AccelleraGDL: General Description Language, Accellera, Mar. 2005Abstract: The IEEE Property Specification L
37、anguage (PSL) is defined. PSL is a formal notationfor specification of electronic system behavior, compatible with multiple electronic system designlanguages, including IEEE Std 1076 (VHDL), IEEE Std 1354 (Verilog), IEEE Std 1666(SystemC), and IEEE Std 1800 (SystemVerilog), thereby enabling a common
38、 specificationand verification flow for multi-language and mixed-language designs. PSL captures design intentin a form suitable for simulation, formal verification, formal analysis, and hybrid verification tools.PSL enhances communication among architects, designers, and verification engineers to in
39、creaseproductivity throughout the design and verification process. The primary audiences for thisstandard are the implementors of tools supporting the language and advanced users of thelanguage. Keywords: ABV, assertion, assertion-based verification, assumption, cover, model checking,property, PSL,
40、specification, temporal logic, verificationg3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3g3IEEE, 802, and POSIX are registered trademarks in the U.S. Patent sequential expressions, which can describe multi-cycle behavior; and temporal operators, which describetemporal relationships among Boolean expressions a
41、nd sequences. For example, consider the followingVerilog Boolean expression: ena | enbThis expression describes a cycle in which at least one of the signals ena and enb are asserted. The PSLsequential expression req; ack; !canceldescribes a sequence of cycles, such that req is asserted in the first
42、cycle, ack is asserted in the secondcycle, and cancel is deasserted in the third cycle. The following property, obtained by applying thetemporal operators always and |= to these expressions, always req;ack;!cancel |= (ena | enb)means that always (that is, in every cycle), if the sequence req;ack;!ca
43、ncel occurs, then either enaor enb is asserted one cycle after the sequence ends. Adding the directive assert as follows:assert always req;ack;!cancel |= (ena | enb);completes the specification, indicating that this property is expected to hold in the design and that thisexpectation needs to be veri
44、fied.1.3.2 Functional verificationPSL can also be used as input to verification tools, for both verification by simulation, as well as formalverification using a model checker or a theorem prover. Each of these is discussed in the subclauses thatfollow.1.3.2.1 SimulationA PSL specification can also
45、be used to automatically generate checks of simulated behavior. This can bedone, for example, by directly integrating the checks in the simulation tool; by interpreting PSL properties ina testbench automation tool that drives the simulator; by generating HDL monitors that are simulatedalongside the
46、design; or by analyzing the traces produced during simulation.For instance, the following PSL property:g44g40g38g3g25g21g24g22g20g29g21g19g20g21g3g44g40g40g40g3g54g87g71g3g20g27g24g19g16g21g19g20g19 g177g3g22g3g177g3IEEEStd 1850-2010 IEEE STANDARD FOR4 Copyright 2010 IEEE. All rights reserved.Proper
47、ty 1: always (req - next !req) states that signal req is a pulsed signal, i.e., if it is high in some cycle, then it is low in the following cycle.Such a property can be easily checked using a simulation checker written in some HDL that has thefunctionality of the finite state machine (FSM) shown in
48、 Figure 1.Figure 1A simple (deterministic) FSM that checks Property 1For properties more complicated than the property shown in Figure 1, manually writing a correspondingchecker is painstaking and error-prone, and maintaining a collection of such checkers for a constantly chang-ing design under deve
49、lopment is a time-consuming task. Instead, a PSL specification can be used as input toa tool that automatically generates simulatable checkers.Although in principle, all PSL properties can be checked for finite paths in simulation, the implementationof the checks is often significantly simpler for a subset called the simple subset of PSL. Informally, in thissubset, composition of temporal properties is restricted to ensure that time moves forward from left to rightthrough a property, as it does in a timing diagram. (See 4.4.4 for the formal definition of the simple
