IEEE 1850 2005

$153.29

IEEE Standard for Property Specification Language (PSL)

Published By	Publication Date	Number of Pages
IEEE	2005	153

Guaranteed Safe Checkout

Category: IEEE

If you have any questions, feel free to reach out to our online customer service team by clicking on the bottom right corner. We’re here to assist you 24/7.
Email:[email protected]

Description

New IEEE Standard – Inactive – Superseded. Replaced by 62531(E):2007. 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 St

PDF Catalog

PDF Pages	PDF Title
1	IEEE Std 1850™-2005, IEEE Standard for Property Specification Language (PSL)
6	Introduction Notice to users Errata Interpretations Patents
7	Participants
9	CONTENTS
11	1. Overview 1.1 Scope 1.2 Purpose 1.2.1 Background
12	1.2.2 Motivation 1.2.3 Goals 1.3 Usage 1.3.1 Functional specification
13	1.3.2 Functional verification
17	2. Normative references
19	3. Definitions, acronyms, and abbreviations 3.1 Definitions
22	3.2 Acronyms and abbreviations 3.3 Special terms
25	4. Organization 4.1 Abstract structure 4.1.1 Layers 4.1.2 Flavors
26	4.2 Lexical structure 4.2.1 Identifiers 4.2.2 Keywords
27	4.2.3 Operators
32	4.2.4 Macros
34	4.2.5 Comments 4.3 Syntax 4.3.1 Conventions
35	4.3.2 HDL dependencies
39	4.4 Semantics 4.4.1 Clocked vs. unclocked evaluation
40	4.4.2 Safety vs. liveness properties 4.4.3 Linear vs. branching logic 4.4.4 Simple subset
41	4.4.5 Finite-length vs. infinite-length behavior 4.4.6 The concept of strength
43	5. Boolean layer 5.1 Expression type classes 5.1.1 Bit expressions
44	5.1.2 Boolean expressions
45	5.1.3 BitVector expressions 5.1.4 Numeric expressions
46	5.1.5 String expressions 5.2 Expression forms 5.2.1 HDL expressions
48	5.2.2 PSL expressions 5.2.3 Built-in functions
54	5.2.4 Union expressions 5.3 Clock expressions
56	5.4 Default clock declaration
59	6. Temporal layer
60	6.1 Sequential expressions 6.1.1 Sequential Extended Regular Expressions (SEREs)
67	6.1.2 Sequences
73	6.2 Properties
74	6.2.1 FL properties
94	6.2.2 Optional Branching Extension (OBE) properties
101	6.2.3 Replicated properties
103	6.3 Property and sequence declarations
104	6.3.1 Parameters
106	6.3.2 Declarations
107	6.3.3 Instantiation
111	7. Verification layer 7.1 Verification directives 7.1.1 assert
112	7.1.2 assume
113	7.1.3 assume_guarantee 7.1.4 restrict
114	7.1.5 restrict_guarantee
115	7.1.6 cover 7.1.7 fairness and strong_fairness
116	7.2 Verification units
117	7.2.1 Verification unit binding
119	7.2.2 Verification unit inheritance
120	7.2.3 Verification unit scoping rules
123	8. Modeling layer 8.1 Integer ranges
124	8.2 Structures
125	Annex A (normative) Syntax rule summary A.1 Conventions
126	A.2 Tokens A.3 HDL dependencies
127	A.3.1 Verilog Extensions
128	A.3.2 Flavor macros
130	A.4 Syntax productions A.4.1 Verification units A.4.2 PSL declarations
131	A.4.3 PSL directives
132	A.4.4 PSL properties
134	A.4.5 Sequential Extended Regular Expressions (SEREs)
135	A.4.6 Parameterized Properties and SEREs A.4.7 Sequences
136	A.4.8 Forms of expression
137	A.4.9 Optional Branching Extension
139	Annex B (normative) Formal syntax and semantics of IEEE Std 1850 PSL B.1 Typed-text representation of symbols B.2 Syntax
140	B.3 Semantics B.3.1 Semantics of FL formulas
143	B.3.2 Semantics of OBE formulas
144	B.4 Syntactic Sugaring B.4.1 Additional SERE operators
145	B.4.2 Additional FL operators
147	B.4.3 Parameterized SEREs and formulas
148	B.5 Rewriting rules for clocks
149	Annex C (informative) Bibliography
151	Index A-F
152	G-S
153	S-Z