IEC 62531:2007

Standard for Property Specification Language (PSL)

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 various standard electronic system design languages.

General Information

• Status: Published
• Publication Date: 06-Nov-2007
• ICS: 25.040.01 - Industrial automation systems in general
• Technical Committee: TC 91 - Electronics assembly technology
• Drafting Committee: WG 13 - TC 91/WG 13
• Current Stage: DELPUB - Deleted Publication
• Start Date: 21-Jun-2012
• Completion Date: 26-Oct-2025

Relations

• Revised: IEC 62531:2012 - Property Specification Language (PSL)
• Effective Date: 05-Sep-2023

Overview

IEC 62531:2007 - also published as IEEE Std 1850 - is the international standard for the Property Specification Language (PSL). It formally defines the syntax and semantics of PSL to describe electronic-system behavior and clarifies how PSL interfaces with standard electronic design languages. IEC 62531 organizes PSL into layers (Boolean, Temporal, Verification, Modeling) and provides normative formal syntax and semantics for use in assertion-based verification and formal analysis.

Key topics and technical requirements

• Language definition: normative specification of PSL lexical structure (identifiers, keywords, operators, macros, comments) and concrete syntax rules.
• Semantics: formal treatment of clocked vs. unclocked evaluation, safety vs. liveness properties, linear vs. branching semantics, finite- vs. infinite-length behavior, and the concept of strength for competing properties.
• Boolean layer: bit, boolean, bitvector, numeric and string expression types; HDL expression integration and built-in functions.
• Temporal layer: Sequential Extended Regular Expressions (SEREs), sequences, properties, optional branching extensions, and replication-used to express temporal patterns and behaviors.
• Verification layer: verification directives and semantics for assert, assume, assume_guarantee, restrict, cover, and fairness constructs; verification unit binding, inheritance and scoping rules.
• Modeling layer: support for integer ranges, structures and parameterized declarations to enable re-usable property definitions.
• Normative annexes: formal syntax summary and rigorous semantic definitions to ensure tool interoperability.

Practical applications and users

• Assertion-based verification: write precise assertions and monitors for simulation, formal model checking, and emulation.
• Formal verification: express properties for model checkers and equivalence checking using PSL’s temporal operators and SEREs.
• Hardware design verification: integrate PSL assertions with HDL designs (e.g., VHDL, Verilog/SystemVerilog) to verify RTL, IP blocks, and SoC interfaces.
• Runtime monitoring and coverage: generate monitors and coverage points from PSL properties to validate functional behavior during simulation or hardware-in-the-loop.
• Typical users: verification engineers, formal-methods specialists, EDA tool vendors, system architects and QA engineers involved in digital IC/FPGA/SoC verification.

Related standards

• IEEE Std 1850 (equivalent document) - joint IEC/IEEE Dual Logo publication.
• HDL standards (integration context): VHDL, Verilog, SystemVerilog (PSL defines how to interface with standard HDLs).

Keywords: IEC 62531, PSL, Property Specification Language, IEEE 1850, assertion-based verification, SERE, temporal logic, assert, assume, cover, HDL integration, formal verification.

Standards Content (Sample)

IEC 62531
Edition 1.0 2007-11
™
IEEE 1850
INTERNATIONAL
STANDARD
Standard for Property Specification Language (PSL)

All rights reserved. IEEE is a registered trademark in the U.S. Patent & Trademark Office, owned by the Institute of
Electrical and Electronics Engineers, Inc.
Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means,
electronic or mechanical, including photocopying and microfilm, without permission in writing from the IEC Central Office.
Any questions about IEEE copyright should be addressed to the IEEE. Enquiries about obtaining additional rights
to this publication and other information requests should be addressed to the IEC or your local IEC member National
Committee.
IEC Central Office The Institute of Electrical and Electronics Engineers, Inc
3, rue de Varembé 3 Park Avenue
CH-1211 Geneva 20 US-New York, NY10016-5997
Switzerland USA
Email: [e-mail] Email: [e-mail]
Web: www.iec.ch Web: www.ieee.org

About the IEC
The International Electrotechnical Commission (IEC) is the leading global organization that prepares and publishes
International Standards for all electrical, electronic and related technologies.

About IEC publications
The technical content of IEC publications is kept under constant review by the IEC. Please make sure that you have the
latest edition, a corrigenda or an amendment might have been published.
ƒ Catalogue of IEC publications: www.iec.ch/searchpub
The IEC on-line Catalogue enables you to search by a variety of criteria (reference number, text, technical committee,…).
It also gives information on projects, withdrawn and replaced publications.
ƒ IEC Just Published: www.iec.ch/online_news/justpub
Stay up to date on all new IEC publications. Just Published details twice a month all new publications released. Available
on-line and also by email.
ƒ Electropedia: www.electropedia.org
The world's leading online dictionary of electronic and electrical terms containing more than 20 000 terms and definitions
in English and French, with equivalent terms in additional languages. Also known as the International Electrotechnical
Vocabulary online.
ƒ Customer Service Centre: www.iec.ch/webstore/custserv
If you wish to give us your feedback on this publication or need further assistance, please visit the Customer Service
Centre FAQ or contact us:
Email: [e-mail]
Tel.: [phone]
Fax: [phone]
IEC 62531
Edition 1.0 2007-11
™
IEEE 1850
INTERNATIONAL
STANDARD
Standard for Property Specification Language (PSL)
INTERNATIONAL
ELECTROTECHNICAL
COMMISSION
PRICE CODE
XG
ICS 25.040 ISBN 2-8318-9352-6
– 2 – IEC 62531:2007(E)
IEEE 1850-2005(E)
CONTENTS
FOREWORD . 4
IEEE introduction .7
1. Overview. 8
1.1 Scope. 8
1.2 Purpose. 8
1.2.1 Background. 8
1.2.2 Motivation. 9
1.2.3 Goals . 9
1.3 Usage . 9
1.3.1 Functional specification. 9
1.3.2 Functional verification. 10
2. Normative references .14
3. Definitions, acronyms, and abbreviations.16
3.1 Definitions . 16
3.2 Acronyms and abbreviations .19
3.3 Special terms. 19
4. Organization. 22
4.1 Abstract structure. 22
4.1.1 Layers. 22
4.1.2 Flavors . 22
4.2 Lexical structure . 23
4.2.1 Identifiers . 23
4.2.2 Keywords . 23
4.2.3 Operators. 24
4.2.4 Macros . 29
4.2.5 Comments . 31
4.3 Syntax . 31
4.3.1 Conventions . 31
4.3.2 HDL dependencies. 32
4.4 Semantics . 36
4.4.1 Clocked vs. unclocked evaluation . 36
4.4.2 Safety vs. liveness properties. 37
4.4.3 Linear vs. branching logic . 37
4.4.4 Simple subset . 37
4.4.5 Finite-length vs. infinite-length behavior . 38
4.4.6 The concept of strength. 38
5. Boolean layer . 40
5.1 Expression type classes. 40
5.1.1 Bit expressions. 40
5.1.2 Boolean expressions . 41
5.1.3 BitVector expressions . 42
5.1.4 Numeric expressions. 42
5.1.5 String expressions .43
5.2 Expression forms . 43
5.2.1 HDL expressions. 43
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE 1850-2005(E)
5.2.2 PSL expressions .45
5.2.3 Built-in functions . 45
5.2.4 Union expressions. 51
5.3 Clock expressions . 51
5.4 Default clock declaration . 53
6. Temporal layer .56
6.1 Sequential expressions . 57
6.1.1 Sequential Extended Regular Expressions (SEREs) . 57
6.1.2 Sequences. 64
6.2 Properties . 70
6.2.1 FL properties. 71
6.2.2 Optional Branching Extension (OBE) properties . 91
6.2.3 Replicated properties . 98
6.3 Property and sequence declarations.100
6.3.1 Parameters.101
6.3.2 Declarations .103
6.3.3 Instantiation .104
7. Verification layer . 108
7.1 Verification directives. 108
7.1.1 assert . 108
7.1.2 assume. 109
7.1.3 assume_guarantee . 110
7.1.4 restrict . 110
7.1.5 restrict_guarantee. 111
7.1.6 cover. 112
7.1.7 fairness and strong_fairness. 112
7.2 Verification units . 113
7.2.1 Verification unit binding. 114
7.2.2 Verification unit inheritance . 116
7.2.3 Verification unit scoping rules. 117
8. Modeling layer. 120
8.1 Integer ranges. 120
8.2 Structures . 121
Annex A (normative) Syntax rule summary. 122
Annex B (normative) Formal syntax and semantics of IEEE Std 1850 PSL. 136
Annex C (informative) Bibliography. 146
Annex D (informative) List of participants. 148
Index . 150
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

– 4 – IEC 62531:2007(E)
IEEE 1850-2005(E)
IEEE 1850-2005(E)
INTERNATIONAL ELECTROTECHNICAL COMMISSION
___________
STANDARD FOR
PROPERTY 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 concerning 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)”). Their 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.
IEC collaborates closely with the International Organization for Standardization (ISO) in accordance with
conditions determined by agreement between the two organizations.
2) The formal decisions or agreements 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 National Committees.
3) IEC Publications have the form of recommendations for international use and are accepted by IEC National
Committees in that sense. While all reasonable efforts are made to ensure that the technical content of IEC
Publications is accurate, IEC 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
transparently to the maximum extent possible in their national and regional publications. Any divergence
between any IEC Publication and the corresponding national or regional publication shall be clearly
indicated in the latter.
5) IEC provides no marking procedure to indicate its approval and cannot be rendered responsible for any
equipment declared to be in conformity with an IEC Publication.
6) Attention is drawn to the possibility that some of the elements of this IEC Publication may be the subject of
patent rights. IEC shall not be held responsible for identifying any or all such patent rights.
International Standard IEC/IEEE 62531 has been processed through Technical Committee
93: Design automation.
The text of this standard is based on the following documents:
IEEE Std FDIS Report on voting
1850(2005) 93/253/FDIS 93/264/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 committee has decided that the contents of this publication will remain unchanged until
the maintenance result 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.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE 1850-2005(E)
IEEE 1850-2005(E)
IEC/IEEE Dual Logo International Standards
This Dual Logo International Standard is the result of an agreement between the IEC and the Institute of
Electrical and Electronics Engineers, Inc. (IEEE). The original IEEE Standard was submitted to the IEC for
consideration under the agreement, and the resulting IEC/IEEE Dual Logo International Standard has been
published in accordance with the ISO/IEC Directives.
IEEE Standards documents are developed within the IEEE Societies and the Standards Coordinating
Committees of the IEEE Standards Association (IEEE-SA) Standards Board. The IEEE develops its standards
through a consensus development process, approved by the American National Standards Institute, which
brings together volunteers representing varied viewpoints and interests to achieve the final product. Volunteers
are not necessarily members of the Institute and serve without compensation. While the IEEE administers the
process and establishes rules to promote fairness in the consensus development process, the IEEE does not
independently evaluate, test, or verify the accuracy of any of the information contained in its standards.
Use of an IEC/IEEE Dual Logo International Standard is wholly voluntary. The IEC and IEEE disclaim liability for
any personal injury, property or other damage, of any nature whatsoever, whether special, indirect,
consequential, or compensatory, directly or indirectly resulting from the publication, use of, or reliance upon
this, or any other IEC or IEEE Standard document.
The IEC and IEEE do not warrant or represent the accuracy or content of the material contained herein, and
expressly disclaim any express or implied warranty, including any implied warranty of merchantability or fitness
for a specific purpose, or that the use of the material contained herein is free from patent infringement.
IEC/IEEE Dual Logo International Standards documents are supplied “AS IS”.
The existence of an IEC/IEEE Dual Logo International Standard does not imply that there are no other ways to
produce, test, measure, purchase, market, or provide other goods and services related to the scope of the
IEC/IEEE Dual Logo International Standard. Furthermore, the viewpoint expressed at the time a standard is
approved and issued is subject to change brought about through developments in the state of the art and
comments received from users of the standard.
Every IEEE Standard is subjected to review at least every five years for revision or reaffirmation. When a
document is more than five years old and has not been reaffirmed, it is reasonable to conclude that its contents,
although still of some value, do not wholly reflect the present state of the art. Users are cautioned to check to
determine that they have the latest edition of any IEEE Standard.
In publishing and making this document available, the IEC and IEEE are not suggesting or rendering
professional or other services for, or on behalf of, any person or entity. Neither the IEC nor IEEE is undertaking
to perform any duty owed by any other person or entity to another. Any person utilizing this, and any other
IEC/IEEE Dual Logo International Standards or IEEE Standards document, should rely upon the advice of a
competent professional in determining the exercise of reasonable care in any given circumstances.
Interpretations – Occasionally questions may arise regarding the meaning of portions of standards as they relate
to specific applications. When the need for interpretations is brought to the attention of IEEE, the Institute will
initiate action to prepare appropriate responses. Since IEEE Standards represent a consensus of concerned
interests, it is important to ensure that any interpretation has also received the concurrence of a balance of
interests. For this reason, IEEE and the members of its societies and Standards Coordinating Committees are
not able to provide an instant response to interpretation requests except in those cases where the matter has
previously received formal consideration.
Comments for revision of IEC/IEEE Dual Logo International Standards are welcome from any interested party,
regardless of membership affiliation with the IEC or IEEE. Suggestions for changes in documents should be in
the form of a proposed change of text, together with appropriate supporting comments. Comments on standards
and requests for interpretations should be addressed to:
Secretary, IEEE-SA Standards Board, 445 Hoes Lane, P.O. Box 1331, Piscataway, NJ 08855-1331, USA and/or
General Secretary, IEC, 3, rue de Varembé, PO Box 131, 1211 Geneva 20, Switzerland.
Authorization to photocopy portions of any individual standard for internal or personal use is granted by the
Institute of Electrical and Electronics Engineers, Inc., provided that the appropriate fee is paid to Copyright
Clearance Center. To arrange for payment of licensing fee, please contact Copyright Clearance Center,
Customer Service, 222 Rosewood Drive, Danvers, MA 01923 USA; [phone]. Permission to photocopy
portions of any individual standard for educational classroom use can also be obtained through the Copyright
Clearance Center.
NOTE – 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 respect to the
existence 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 the
legal validity or scope of those patents that are brought to its attention.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

– 6 – IEC 62531:2007(E)
IEEE 1850-2005(E)
IEEE Standard for
Property Specification 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
Grateful acknowledgment is made to Accellera Organization, Inc. for the permission to use 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 specification 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-language 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. 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
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE 1850-2005(E)
IEEE 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 behavior, 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 system 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 interpretations 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 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 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 such 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.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

– 8 – IEC 62531:2007(E)
IEEE 1850-2005(E)
STANDARD FOR
PROPERTY SPECIFICATION VOLTAGE (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 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 Std 1364™ (Verilog ), IEEE P1800™ (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
approaches 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 last
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 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 verification using both simulation and formal
verification, thereby enabling a productivity boost in functional verification.
Numbers 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 information about obtaining drafts, contact the Institute of Electrical and Electronics Engineers, Inc.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE 1850-2005(E)
IEEE
Std 1850-2005 IEEE STANDARD FOR
1.2.2 Motivation
Ensuring that a design’s implementation satisfies its specification is the foundation of hardware verification.
Key to the design and verification process is the act of specification. Yet historically, the process of
specification has consisted of creating a natural language description of a set of design requirements. This
form of specification is both ambiguous and, in many cases, unverifiable due to the lack of a standard
machine-executable representation. Furthermore, ensuring that all functional aspects of the specification
have been adequately verified (that is, covered) is problematic.
The IEEE PSL was developed to address these shortcomings. It gives the design architect a standard means
of specifying design properties using a concise syntax with clearly-defined formal semantics. Similarly, it
enables the RTL implementer to capture design intent in a verifiable form, while enabling the verification
engineer to validate that the implementation satisfies its specification through dynamic (that is, simulation)
and static (that is, formal) verification means. Furthermore, it provides a means to measure the quality of the
verification process through the creation of functional coverage models built on formally specified
properties. In addition, it provides a standard means for hardware designers and verification engineers to
create a rigorous and machine-executable design specification.
1.2.3 Goals
PSL was specifically developed to fulfill the following general hardware functional specification
requirements:
— Easy to learn, write, and read
—Concise syntax
— Rigorously well-defined formal semantics
— Expressive power, permitting specifications of a large class of real-world design properties
— Known efficient underlying algorithms in simulation, as well as formal verification
1.3 Usage
PSL is a language for the formal specification of hardware. It is used to describe properties that are required
to hold in the design under verification. PSL provides a means to write specifications that are both easy to
read and mathematically precise. It is intended to be used for functional specification on the one hand and as
input to functional verification tools on the other. Thus, a PSL specification is an executable specification of
a hardware design.
1.3.1 Functional specification
PSL can be used to capture requirements regarding the overall behavior of a design, as well as assumptions
about the environment in which the design is expected to operate. PSL can also capture internal behavioral
requirements and assumptions that arise during the design process. Both enable more effective functional
verification and reuse of the design.
One important use of PSL is for documentation, either in place of or along with an English specification. A
PSL specification can describe simple invariants (for example, signals read_enable and
write_enable are never asserted simultaneously) as well as multi-cycle behavior (for example, correct
behavior of an interface with respect to a bus protocol or correct behavior of pipelined operations).
A PSL specification consists of assertions regarding properties of a design under a set of assumptions. A
property is built from three kinds of elements: Boolean expressions, which describe behavior over one cycle;
sequential expressions, which can describe multi-cycle behavior; and temporal operators, which describe
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

– 10 – IEC 62531:2007(E)
IEEE 1850-2005(E)
IEEE
PROPERTY SPECIFICATION LANGUAGE (PSL) Std 1850-2005
temporal relationships among Boolean expressions and sequences. For example, consider the following
Verilog Boolean expression:
ena || enb
This expression describes a cycle in which at least one of the signals ena and enb are asserted. The PSL
sequential expression
{req; ack; !cancel}
describes a sequence of cycles, such that req is asserted in the first cycle, ack is asserted in the second
cycle, and cancel is deasserted in the third cycle. The following property, obtained by applying the
temporal 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;!cancel} occurs, then either ena
or 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 this
expectation needs to be verified.
1.3.2 Functional verification
PSL can also be used as input to verification tools, for both verification by simulation, as well as formal
verification using a model checker or a theorem prover. Each of these is discussed in the subclauses that
follow.
1.3.2.1 Simulation
A PSL specification can also be used to automatically generate checks of simulated behavior. This can be
done, for example, by directly integrating the checks in the simulation tool; by interpreting PSL properties in
a testbench automation tool that drives the simulator; by generating HDL monitors that are simulated
alongside the design; or by analyzing the traces produced during simulation.
For instance, the following PSL property:
Property 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 the
functionality of the finite state machine (FSM) shown in Figure 1.
Figure 1—A simple (deterministic) FSM that checks Property 1
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE
Std 1850-2005 IEEE STANDARD FOR
IEEE 1850-2005(E)
For properties more complicated than the property shown in Figure 1, manually writing a corresponding
checker 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 specification can be used as input to
a tool that automatically generates simulatable checkers.
Although in principle, all PSL properties can be checked for finite paths in simulation, the implementation
of the checks is often significantly simpler for a subset called the simple subset of PSL. Informally, in this
subset, composition of temporal properties is restricted to ensure that time moves forward from left to right
through a property, as it does in a timing diagram. (See 4.4.4 for the formal definition of the simple subset.)
For example, the property
Property 2: always (a -> next[3] b)
which states that, if a is asserted, then b is asserted three cycles later, belongs to the simple subset, because
a appears to the left of b in the property and also appears to the left of b in the timing diagram of any
behavior that is not a violation of the property. Figure 2 shows an example of such a timing diagram.
0      1       2       3       4      5      6       7
a
b
Figure 2—A trace that satisfies Property 2
An example of a property that is not in this subset is the property
Property 3: always ((a && next[3] b) -> c)
which states that, if a is asserted and b is asserted three cycles later, then c is asserted (in the same cycle as
a). This property does not belong to the simple subset, because although c appears to the right of a and b in
the property, it appears to the left of b in a timing diagram that is not a violation of the property. Figure 3
shows an example of such a timing diagram.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

– 12 – IEC 62531:2007(E)
IEEE 1850-2005(E)
IEEE
PROPERTY SPECIFICATION LANGUAGE (PSL) Std 1850-2005
0      1       2       3       4      5      6       7
a
b
c
Figure 3—A trace that satisfies Property 3
1.3.2.2 Formal verification
PSL is an extension of the standard temporal logics Linear-Time Temporal Logic (LTL) and Computation
Tree Logic (CTL). A specification in the PSL Foundation Language (respectively, the PSL Optional Branch-
ing Extension) can be compiled down to a formula of pure LTL (respectively, CTL), possibly with some
auxiliary HDL code, known as a satellite.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE 1850-2005(E)
IEEE
Std 1850-2005 IEEE STANDARD FOR
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

– 14 – IEC 62531:2007(E)
IEEE 1850-2005(E)
IEEE
PROPERTY SPECIFICATION LANGUAGE (PSL) Std 1850-2005
2. Normative references
The following referenced documents are indispensable for the application of this document. For dated
references, only the edition cited applies. For undated references, the latest edition of the referenced
document (including any amendments or corrigenda) applies.
“General Description Language,” Accellera, Napa, CA, Mar. 2005.
IEC/IEEE 62142 (IEEE Std 1364.1), Standard for Verilog Register Transfer Level Synthesis.
IEEE Std 1076™, IEEE Standard VHDL Language Reference Manual.
IEEE Std 1076.6™, IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis.
IEEE Std 1364™, IEEE Standard for Verilog Hardware Description Language.
IEEE P1666™, Draft Standard for the SystemC Language.
IEEE P1800™, Draft Standard for the SystemVerilog Language.
This document is available from the IEEE Standards World Wide Web site, at http://standards.ieee.org/downloads/1850/1850-2005/
gdl.pdf.
IEC publications are available from the Sales Department of the International Electrotechnical Commission, Case Postale 131, 3, rue
de Varembé, CH-1211, Genève 20, Switzerland/Suisse (http://www.iec.ch/). IEC publications are also available in the United States
from the Sales Department, American National Standards Institute, 11 West 42nd Street, 13th Floor, New York, NY 10036, USA.
IEEE publications are available from the Institute of Electrical and Electronics Engineers, 445 Hoes Lane, P.O. Box 1331, Piscataway,
NJ 08855-1331, USA (http://standards.ieee.org/).
The IEEE standards or products referred to in this standard are trademarks of the Institute of Electrical and Electronics Engineers, Inc.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE 1850-2005(E)
IEEE
Std 1850-2005 IEEE STANDARD FOR
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

– 16 – IEC 62531:2007(E)
IEEE 1850-2005(E)
IEEE
PROPERTY SPECIFICATION LANGUAGE (PSL) Std 1850-2005
3. Definitions, acronyms, and abbreviations
For the purposes of this standardt, the following terms and definitions apply. The Authoritative Dictionary of
IEEE Standards Terms [B5] should be referenced for terms not defined in this clause.
3.1 Definitions
This subclause defines the terms used in this standard.
3.1.1 assertion: A statement that a given property is required to hold and a directive to functional
verification tools to verify that it does hold.
3.1.2 assumption: A statement that the design is constrained by the given property and a directive to
functional verification tools to consider only paths on which the given property holds.
3.1.3 asynchronous property: A property whose clock context is equivalent to True.
3.1.4 behavior: A path.
3.1.5 Boolean (expression): An expression that yields a logical value.
3.1.6 checker: An auxiliary process (usually constructed as a finite state machine) that monitors simulation
of a design and reports errors when asserted properties do not hold. A checker may be represented in the
same HDL code as the design or in some other form that can be linked with a simulation of the design.
3.1.7 completes: A term used to identify the last cycle of a path that satisfies a sequential expression or
property.
3.1.8 computation path: A succession of states of the design, such that the design can actually transition
from each state on the path to its successor.
3.1.9 constraint: A condition (usually on the input signals) that limits the set of behaviors to be considered.
A constraint may represent real requirements (e.g., clocking requirements) on the environment in which the
design is used, or it may represent artificial limitations (e.g., mode settings) imposed in order to partition the
functional verification task.
3.1.10 count: A number or range.
3.1.11 coverage: A measure of the occurrence of certain behavior during (typically dynamic) functional
verification and, therefore, a measure of the completeness of the (dynamic) functional verification process.
3.1.12 cycle: An evaluation cycle.
3.1.13 describes: A term used to identify the set of behaviors for which Boolean expression, sequential
expression, or property holds.
3.1.14 design: A model of a piece of hardware, described in some hardware description language (HDL). A
design typically involves a collection of inputs, outputs, state elements, and combinational functions that
compute next state and outputs from current state and inputs.
3.1.15 design behavior: A computation path for a given design.
The numbers in brackets correspond to those of the bibliography in Annex C.
Published by IEC under licence from IEEE. © 2005 IEEE. All rights reserved.

IEEE 1850-2005(E)
IEEE
Std 1850-2005 IEEE STANDARD FOR
3.1.16 dynamic verification: A verification process such as simulation, in which a property is checked over
individual, finite design behaviors that are typically obtained by dynamically exercising the design through a
finite number of evaluation cycles. Generally, dynamic verification supports no inference about whether the
property holds for a behavior over which the property has not yet been checked.
3.1.17 evaluation: The process of exercising a design by iteratively applying values to its inputs, computing
i
...