1、raising standards worldwideNO COPYING WITHOUT BSI PERMISSION EXCEPT AS PERMITTED BY COPYRIGHT LAWBSI Standards PublicationIEEE standard for property specification language (PSL)BS IEC 62531:2012National forewordThis British Standard is the UK implementation of IEC 62531:2012. It super-sedes BS IEC 6
2、2531:2007 which is withdrawn.The UK participation in its preparation was entrusted to Technical CommitteeGEL/93, Design automation.A list of organizations represented on this committee can be obtained onrequest to its secretary.This publication does not purport to include all the necessary provision
3、s of acontract. Users are responsible for its correct application. The British Standards Institution 2012Published by BSI Standards Limited 2012ISBN 978 0 580 77672 4ICS 25.040.01; 35.060Compliance with a British Standard cannot confer immunity fromlegal obligations.This British Standard was publish
4、ed under the authority of the StandardsPolicy and Strategy Committee on 31 August 2012.Amendments issued since publicationAmd. No. Date Text affectedBRITISH STANDARDBS IEC 62531:2012IEC 62531Edition 2.0 2012-06INTERNATIONAL STANDARD Property Specification Language (PSL) INTERNATIONAL ELECTROTECHNICA
5、L COMMISSION XHICS 25.040; 35.060 PRICE CODEISBN 978-2-83220-106-0Warning! Make sure that you obtained this publication from an authorized distributor. IEEE Std 1850BS IEC 62531:2012Copyright 2010 IEEE. All rights reserved. ixContents1. Overview 11.1 Scope 11.2 Purpose. 11.2.1 Background 21.2.2 Moti
6、vation 21.2.3 Goals 21.3 Usage . 21.3.1 Functional specification.31.3.2 Functional 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
7、. 154.1.2 Flavors . 154.2 Lexical structure 164.2.1 Identifiers . 164.2.2 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. 3
8、04.4.3 Linear vs. branching logic . 304.4.4 Simple subset . 304.4.5 Finite-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 express
9、ions 355.1.5 String expressions 365.2 Expression forms 365.2.1 HDL expressions36 ii IEC 62531:2012 IEEE Std 1850-2010BS IEC 62531:20125.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 Sequ
10、ential expressions. 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
11、declarations. 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.
12、2.1 Verification 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 Direc
13、t and indirect 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. 167Annex D (innullIEC 62531:2012 IEEE Std 1850-2010 iii BS IEC 62531:2012Property
14、Specification Language (PSL) FOREWORD 1) The International Electrotechnical Commission (IEC) is a worldwide organization for standardization comprising all national electrotechnical committees (IEC National Committees). The object of IEC is to promote international co-operation on all questions conc
15、erning standardization in the electrical and electronic fields. To this end and in addition to other activities, IEC publishes International Standards, Technical Specifications, Technical Reports, Publicly Available Specifications (PAS) and Guides (hereafter referred to as “IEC Publication(s)”). The
16、ir preparation is entrusted to technical committees; any IEC National Committee interested in the subject dealt with may participate in this preparatory work. International, governmental and non-governmental organizations liaising with the IEC also participate in this preparation. IEEE Standards doc
17、uments are developed within IEEE Societies and Standards Coordinating Committees of the IEEE Standards Association (IEEE-SA) Standards Board. IEEE develops its standards through a consensus development process, which brings together volunteers representing varied viewpoints and interests to achieve
18、the final product. Volunteers are not necessarily members of IEEE and serve without compensation. While IEEE administers the process and establishes rules to promote fairness in the consensus development process, IEEE does not independently evaluate, test, or verify the accuracy of any of the inform
19、ation contained in its standards. Use of IEEE Standards documents is wholly voluntary. IEEE documents are made available for use subject to important notices and legal disclaimers (see http:/standards.ieee.org/IPR/disclaimers.html for more information). IEC collaborates closely with IEEE in accordan
20、ce with conditions determined by agreement between the two organizations. 2) The formal decisions of IEC on technical matters express, as nearly as possible, an international consensus of opinion on the relevant subjects since each technical committee has representation from all interested IEC Natio
21、nal Committees. The formal decisions of IEEE on technical matters, once consensus within IEEE Societies and Standards Coordinating Committees has been reached, is determined by a balanced ballot of materially interested parties who indicate interest in reviewing the proposed standard. Final approval
22、 of the IEEE standards document is given by the IEEE Standards Association (IEEE-SA) Standards Board. 3) IEC/IEEE Publications have the form of recommendations for international use and are accepted by IEC National Committees/IEEE Societies in that sense. While all reasonable efforts are made to ens
23、ure 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 misinterpretation by any end user. 4) In order to promote international uniformity, IEC National Committees undertake to apply IEC Publications (i
24、ncluding IEC/IEEE Publications) transparently to the maximum extent possible in their national and regional publications. Any divergence between any IEC/IEEE Publication and the corresponding national or regional publication shall be clearly indicated in the latter. 5) IEC and IEEE do not provide an
25、y attestation of conformity. Independent certification bodies provide conformity assessment services and, in some areas, access to IEC marks of conformity. IEC and IEEE are not responsible for any services carried out by independent certification bodies. 6) All users should ensure that they have the
26、 latest edition of this publication. 7) No liability shall attach to IEC or IEEE or their directors, employees, servants or agents including individual experts and members of technical committees and IEC National Committees, or volunteers of IEEE Societies and the Standards Coordinating Committees o
27、f the IEEE Standards Association (IEEE-SA) Standards Board, for any personal injury, property damage or other damage of any nature whatsoever, whether direct or indirect, or for costs (including legal fees) and expenses arising out of the publication, use of, or reliance upon, this IEC/IEEE Publicat
28、ion or any other IEC or IEEE Publications. 8) Attention is drawn to the normative references cited in this publication. Use of the referenced publications is indispensable for the correct application of this publication. 9) Attention is drawn to the possibility that implementation of this IEC/IEEE P
29、ublication may require use of material covered by patent rights. By publication of this standard, no position is taken with respect to the existence or validity of any patent rights in connection therewith. IEC or IEEE shall not be held responsible for identifying Essential Patent Claims for which a
30、 license may be required, for conducting inquiries into the legal validity or scope of Patent Claims or determining whether any licensing terms or conditions provided in connection with submission of a Letter of Assurance, if any, or in any licensing agreements are reasonable or non-discriminatory.
31、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 entirely their own responsibility. iv IEC 62531:2012 IEEE Std 1850-2010BS IEC 62531:2012International Standard IEC 62531/ IEEE Std 1850-2010 has been
32、processed through IEC technical committee 93: Design automation, under the IEC/IEEE Dual Logo 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 R
33、eport on voting IEEE Std 1850-2010 93/319/FDIS 93/326/RVD Full information on the voting for 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 wi
34、ll remain unchanged until the stability date indicated on the IEC web site under “http:/webstore.iec.ch“ in the data related to the specific publication. At this date, the publication will be reconfirmed, withdrawn, replaced by a revised edition, or amended. IEC 62531:2012 IEEE Std 1850-2010 v BS IE
35、C 62531:2012IEEE Std 1850TM-2010(Revision ofIEEE Std1850-2005)IEEE Standard for Property Specification Language (PSL)SponsorDesign Automation Standards Committeeof theIEEE Computer Societyand theIEEE Standards Association Corporate Advisory GroupApproved 25 March 2010IEEE-SA Standards Board vi IEC 6
36、2531:2012 IEEE Std 1850-2010BS IEC 62531:2012Grateful 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. 20
37、05Abstract: The IEEE Property Specification Language (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 18
38、00 (SystemVerilog), thereby enabling a common 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
39、, designers, and verification engineers to increaseproductivity 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, assu
40、mption, cover, model checking,property, PSL, specification, temporal logic, verificationIEEE, 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 expres
41、sions and 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
42、 first 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;
43、ack;!cancel 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
44、be verified.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 ca
45、n also 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 simulatedalongsi
46、de the design; or by analyzing the traces produced during simulation.For instance, the following PSL property:IEC 62531:2012 IEEE Std 1850-2010 3 BS IEC 62531:2012IEEEStd 1850-2010 IEEE STANDARD FOR4 Copyright 2010 IEEE. All rights reserved.Property 1: always (req - next !req) states that signal req
47、 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 Figure 1.Figure 1A simple (deterministic) FSM that c
48、hecks 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 development is a time-consuming task. Instead, a PSL spec
49、ification 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 subset.)For
