IEEE IEC 62531 2012
$140.83
IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL)
| Published By | Publication Date | Number of Pages |
| IEEE | 2012 | 188 |
– Active. The IEEE Property Specification Language (PSL) is defined. 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 1354 (Verilog), IEEE Std 1666 (SystemC), and IEEE Std 1800 (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
PDF Catalog
| PDF Pages | PDF Title |
|---|---|
| 1 | IEC 62531 (IEEE Std 1850) Front Cover |
| 4 | CONTENTS IEEE Contents |
| 6 | IEC FOREWORD |
| 8 | Title page |
| 10 | IEEE Introduction Notice to users Laws and regulations Copyrights Updating of IEEE documents Errata |
| 11 | Interpretations Patents Participants |
| 12 | Important Notice 1. Overview 1.1 Scope 1.2 Purpose |
| 13 | 1.2.1 Background 1.2.2 Motivation 1.2.3 Goals 1.3 Usage |
| 14 | 1.3.1 Functional specification 1.3.2 Functional verification |
| 18 | 2. Normative references |
| 20 | 3. Definitions, acronyms, and abbreviations 3.1 Definitions |
| 23 | 3.2 Acronyms and abbreviations 3.3 Special terms |
| 26 | 4. Organization 4.1 Abstract structure 4.1.1 Layers 4.1.2 Flavors |
| 27 | 4.2 Lexical structure 4.2.1 Identifiers 4.2.2 Keywords |
| 28 | 4.2.3 Operators |
| 33 | 4.2.4 Macros |
| 35 | 4.2.5 Comments 4.3 Syntax 4.3.1 Conventions |
| 36 | 4.3.2 HDL dependencies |
| 40 | 4.4 Semantics 4.4.1 Clocked vs. unclocked evaluation |
| 41 | 4.4.2 Safety vs. liveness properties 4.4.3 Linear vs. branching logic 4.4.4 Simple subset |
| 42 | 4.4.5 Finite-length vs. infinite-length behavior 4.4.6 The concept of strength |
| 44 | 5. Boolean layer 5.1 Expression type classes 5.1.1 Bit expressions |
| 45 | 5.1.2 Boolean expressions |
| 46 | 5.1.3 BitVector expressions 5.1.4 Numeric expressions |
| 47 | 5.1.5 String expressions 5.2 Expression forms 5.2.1 HDL expressions |
| 50 | 5.2.2 PSL expressions 5.2.3 Built-in functions |
| 56 | 5.2.4 Union expressions 5.3 Clock expressions |
| 58 | 5.4 Default clock declaration |
| 60 | 6. Temporal layer |
| 61 | 6.1 Sequential expressions 6.1.1 Sequential Extended Regular Expressions (SEREs) |
| 68 | 6.1.2 Sequences |
| 74 | 6.2 Properties 6.2.1 FL properties |
| 95 | 6.2.2 Optional Branching Extension (OBE) properties |
| 101 | 6.2.3 Replicated properties |
| 104 | 6.3 Local variables |
| 108 | 6.4 Procedural blocks |
| 114 | 6.5 Property and sequence declarations |
| 115 | 6.5.1 Parameters |
| 117 | 6.5.2 Declarations |
| 118 | 6.5.3 Instantiation |
| 122 | 7. Verification layer 7.1 Verification directives 7.1.1 assert |
| 123 | 7.1.2 assume |
| 124 | 7.1.3 restrict 7.1.4 restrict! |
| 126 | 7.1.5 cover |
| 127 | 7.1.6 fairness and strong_fairness |
| 128 | 7.2 Verification units |
| 132 | 7.2.1 Verification unit binding 7.2.2 Verification unit instantiation |
| 133 | 7.2.3 Verification unit inheritance |
| 135 | 7.2.4 Overriding assignments |
| 140 | 8. Modeling layer 8.1 Integer ranges |
| 141 | 8.2 Structures |
| 142 | 9. Scope and visibility rules 9.1 Immediate scope 9.2 Extended scope |
| 143 | 9.3 Direct and indirect name references |
| 146 | Annex A (normative) Syntax rule summary A.1 Conventions |
| 147 | A.2 Tokens A.3 HDL dependencies |
| 148 | A.3.1 Verilog extensions |
| 149 | A.3.2 Flavor macros |
| 151 | A.4 Syntax productions A.4.1 Verification units |
| 152 | A.4.2 PSL declarations |
| 153 | A.4.3 PSL directives A.4.4 PSL properties |
| 155 | A.4.5 Sequential Extended Regular Expressions (SEREs) |
| 156 | A.4.6 Parameterized Properties and SEREs A.4.7 Sequences |
| 157 | A.4.8 Forms of expression |
| 158 | A.4.9 Optional Branching Extension |
| 160 | Annex B (normative) Formal Syntax and Semantics of IEEE Std 1850 Property Specification Language (PSL) |
| 178 | Annex C (informative) Bibliography |
| 183 | Index |
Related products
-
BS IEC 62531:2012
IEEE standard for property specification language (PSL) Published By Publication Date Number of Pages BSI…
-
BS IEC 62531:2012
IEEE standard for property specification language (PSL) Published By Publication Date Number of Pages BSI…
