IEC 62531:2012

IEC 62531
Edition 2.0 2012-06
™
IEEE Std 1850
INTERNATIONAL
STANDARD
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 Institute of Electrical and Electronics Engineers, Inc.
3, rue de Varembé 3 Park Avenue
CH-1211 Geneva 20 New York, NY 10016-5997
Switzerland United States of America
Tel.: +41 22 919 02 11 stds.info@ieee.org
Fax: +41 22 919 03 00 www.ieee.org
info@iec.ch
www.iec.ch
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.

Useful links:
IEC publications search - www.iec.ch/searchpub Electropedia - www.electropedia.org
The advanced search enables you to find IEC publications The world's leading online dictionary of electronic and
by a variety of criteria (reference number, text, technical electrical terms containing more than 30 000 terms and
committee,…). definitions in English and French, with equivalent terms in
It also gives information on projects, replaced and additional languages. Also known as the International
withdrawn publications. Electrotechnical Vocabulary (IEV) on-line.

IEC Just Published - webstore.iec.ch/justpublished Customer Service Centre - webstore.iec.ch/csc
Stay up to date on all new IEC publications. Just Published If you wish to give us your feedback on this publication
details all new publications released. Available on-line and or need further assistance, please contact the
also once a month by email. Customer Service Centre: csc@iec.ch.

IEC 62531
Edition 2.0 2012-06
IEEE Std 1850™
INTERNATIONAL
STANDARD
Property Specification Language (PSL)

INTERNATIONAL
ELECTROTECHNICAL
COMMISSION
PRICE CODE
XH
ICS 25.040; 35.060 ISBN 978-2-83220-106-0

,(&
±LL± ,(((6WG
Contents
1. Overview. 1
1.1 Scope. 1
1.2 Purpose. 1
1.2.1 Background. 2
1.2.2 Motivation. 2
1.2.3 Goals . 2
1.3 Usage . 2
1.3.1 Functional specification.3
1.3.2 Functional 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.1 Layers. 15
4.1.2 Flavors . 15
4.2 Lexical structure . 16
4.2.1 Identifiers . 16
4.2.2 Keywords . 16
4.2.3 Operators. 17
4.2.4 Macros . 22
4.2.5 Comments . 24
4.3 Syntax . 24
4.3.1 Conventions . 24
4.3.2 HDL dependencies. 25
4.4 Semantics . 29
4.4.1 Clocked vs. unclocked evaluation . 29
4.4.2 Safety vs. liveness properties. 30
4.4.3 Linear vs. branching logic . 30
4.4.4 Simple subset . 30
4.4.5 Finite-length vs. infinite-length behavior . 31
4.4.6 The concept of strength. 31
5. Boolean layer . 33
5.1 Expression type classes. 33
5.1.1 Bit expressions. 33
5.1.2 Boolean expressions . 34
5.1.3 BitVector expressions . 35
5.1.4 Numeric expressions. 35
5.1.5 String expressions . 36
5.2 Expression forms . 36
5.2.1 HDL expressions.36

Copyright ©2010 IEEE. All rights reserved. ix

,(&
,(((6WG ±LLL±
5.2.2 PSL expressions. 39
5.2.3 Built-in functions . 39
5.2.4 Union expressions.45
5.3 Clock expressions . 45
5.4 Default clock declaration . 47
6. Temporal layer. 49
6.1 Sequential expressions. 50
6.1.1 Sequential Extended Regular Expressions (SEREs) . 50
6.1.2 Sequences. 57
6.2 Properties . 63
6.2.1 FL properties. 63
6.2.2 Optional Branching Extension (OBE) properties . 84
6.2.3 Replicated properties . 90
6.3 Local variables. 93
6.4 Procedural blocks. 97
6.5 Property and sequence declarations. 103
6.5.1 Parameters. 104
6.5.2 Declarations . 106
6.5.3 Instantiation . 107
7. Verification layer . 111
7.1 Verification directives. 111
7.1.1 assert . 111
7.1.2 assume. 112
7.1.3 restrict . 113
7.1.4 restrict! . 113
7.1.5 cover. 115
7.1.6 fairness and strong_fairness. 116
7.2 Verification units . 117
7.2.1 Verification unit binding. 121
7.2.2 Verification unit instantiation . 121
7.2.3 Verification unit inheritance . 122
7.2.4 Overriding assignments . 124
8. Modeling layer. 129
8.1 Integer ranges. 129
8.2 Structures . 130
9. Scope and visibility rules. 131
9.1 Immediate scope . 131
9.2 Extended scope . 131
9.3 Direct and indirect name references . 132
Annex A (normative) Syntax rule summary. 135
Annex B (normative) Formal Syntax and Semantics of
...