IEC 62531:2007

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: inmail@iec.ch Email: stds-info@ieee.org
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: csc@iec.ch
Tel.: +41 22 919 02 11
Fax: +41 22 919 03 00
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
...