IEC_62531-2012_IEEE_Std_1850.pdf

IEC 62531 Edition 2.0 2012-06 INTERNATIONAL STANDARD Property Specification Language(PSL)IEC 62531:2012(E)IEEE Std 1850-2010 IEEE Std 1850 Copyrighted material licensed to BR Demo by Thomson Reuters(Scientific),Inc.,,downloaded on Nov-28-2014 by James Madison.No further reproduction or distribution is permitted.Uncontrolled when printed.THIS PUBLICATION IS COPYRIGHT PROTECTED Copyright 2010 IEEE 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.infoieee.org Fax:+41 22 919 03 00 www.ieee.org infoiec.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 The advanced search enables you to find IEC publications by a variety of criteria(reference number,text,technical committee,).It also gives information on projects,replaced and withdrawn publications.IEC Just Published-webstore.iec.ch/justpublished Stay up to date on all new IEC publications.Just Published details all new publications released.Available on-line and also once a month by email.Electropedia-www.electropedia.org The worlds leading online dictionary of electronic and electrical terms containing more than 30 000 terms and definitions in English and French,with equivalent terms in additional languages.Also known as the International Electrotechnical Vocabulary(IEV)on-line.Customer Service Centre-webstore.iec.ch/csc If you wish to give us your feedback on this publication or need further assistance,please contact the Customer Service Centre:csciec.ch.Copyrighted material licensed to BR Demo by Thomson Reuters(Scientific),Inc.,,downloaded on Nov-28-2014 by James Madison.No further reproduction or distribution is permitted.Uncontrolled when printed.IEC 62531Edition 2.0 2012-06INTERNATIONAL STANDARD Property Specification Language(PSL)INTERNATIONAL ELECTROTECHNICAL COMMISSION XHICS 25.040;35.060 PRICE CODEISBN 978-2-83220-106-0 Warning!Make sure that you obtained this publication from an authorized distributor.IEEE Std 1850Copyrighted material licensed to BR Demo by Thomson Reuters(Scientific),Inc.,,downloaded on Nov-28-2014 by James Madison.No further reproduction or distribution is permitted.Uncontrolled when printed.Copyright 2010 IEEE.All rights reserved.ixContents1.Overview.11.1 Scope.11.2 Purpose.11.2.1Background.21.2.2Motivation.21.2.3Goals.21.3 Usage.21.3.1Functional specification.31.3.2Functional 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.1Layers.154.1.2Flavors.154.2 Lexical structure.164.2.1Identifiers.164.2.2Keywords.164.2.3Operators.174.2.4Macros.224.2.5Comments.244.3 Syntax.244.3.1Conventions.244.3.2HDL dependencies.254.4 Semantics.294.4.1Clocked vs.unclocked evaluation.294.4.2Safety vs.liveness properties.304.4.3Linear vs.branching logic.304.4.4Simple subset.304.4.5Finite-length vs.infinite-length behavior.314.4.6The concept of strength.315.Boolean layer.335.1 Expression type classes.335.1.1Bit expressions.335.1.2Boolean expressions.345.1.3BitVector expressions.355.1.4Numeric expressions.355.1.5String expressions.365.2 Expression forms.365.2.1HDL expressions.36 ii IEC 62531:2012 IEEE Std 1850-2010 Copyrighted material licensed to BR Demo by Thomson Reuters(Scientific),Inc.,,downloaded on Nov-28-2014 by James Madison.No further reproduction or distribution is permitted.Uncontrolled when printed.5.2.2PSL expressions.395.2.3Built-in functions.395.2.4Union expressions.455.3 Clock expressions.455.4 Default clock declaration.476.Temporal layer.496.1 Sequential expressions.506.1.1Sequential Extended Regular Expressions(SEREs).506.1.2Sequences.576.2 Properties.636.2.1FL properties.636.2.2Optional Branching Extension(OBE)properties.846.2.3Replicated properties.906.3 Local variables.936.4 Procedural blocks.