Assertion-Based Design (eBook)

Harry D. Foster, Adam C. Krolnik, David J. Lacey (Autoren)

eBook Download: PDF

2005 | 2nd ed. 2004
XXIII, 390 Seiten
Springer US (Verlag)
978-1-4020-8028-9 (ISBN)

Infos

Chapter 3 Specifying RTL Properties 61 3. 1 Definitions and concepts 62 62 3. 1. 1 Property 3. 1. 2 Events 65 3. 2 Property classification 65 Safety versus liveness 66 3. 2. 1 3. 2. 2 Constraint versus assertion 67 3. 2. 3 Declarative versus procedural 67 3. 3 RTL assertion specification techniques 68 RTL invariant assertions 69 3. 3. 1 3. 3. 2 Declaring properties with PSL 72 RTL cycle related assertions 73 3. 3. 3 3. 3. 4 PSL and default clock declaration 74 3. 3. 5 Specifying sequences 75 3. 3. 6 Specifying eventualities 80 3. 3. 7 PSL built-in functions 82 3. 4Pragma-based assertions 82 3. 5 SystemVerilog assertions 84 3. 5. 1 Immediate assertions 84 3. 5. 2Concurrent assertions 86 3. 5. 3 System functions 95 3. 6 PCI property specification example 96 3. 6. 1 PCI overview 96 3. 7 Summary 102 Chapter 4 PLI-Based Assertions 103 4. 1 Procedural assertions 104 4. 1. 1 A simple PLI assertion 105 4. 1. 2 Assertions within a simulation time slot 108 4. 1. 3 Assertions across simulation time slots 111 4. 1. 4 False firing across multiple time slots 116 4. 2 PLI-based assertion library 118 4. 2. 1 Assert quiescent state 119 4. 3 Summary 123 Chapter 5 Functional Coverage 125 5. 1 Verification approaches 126 5. 2 Understanding coverage 127 5. 2. 1 Controllability versus observability 128 5. 2.

Inhalt

TABLE OF CONTENTS 6
PREFACE 15
Book organization 17
New in Second Edition 20
Acknowledgements 20
1 INTRODUCTION 22
1.1 Property checking 22
1.2 Verification techniques 23
1.3 What is an assertion? 24
1.3.1 A historical perspective 25
1.3.2 Do assertions really work? 27
1.3.3 What are the benefits of assertions? 28
1.3.4 Why are assertions not used? 32
1.4 Phases of the design process 35
1.4.1 Ensuring requirements are satisfied 37
1.4.2 Techniques for ensuring consistency 39
1.4.3 Roles and ownership 40
1.5 Summary 41
2 ASSERTION METHODOLOGY 42
2.1 Design methodology 42
2.1.1 Project planning 43
2.1.2 Design requirements 48
2.1.3 Design documents 49
2.1.4 Design reviews 50
2.1.5 Design validation 51
2.2 Assertion methodology for new designs 51
2.2.1 Key learnings 52
2.2.2 Best practices 54
2.2.3 Assertion density 58
2.2.4 Process for adding assertions 60
2.2.5 When not to add assertions 60
2.3 Assertion methodology for existing designs 61
2.4 Assertions and simulation 63
2.5 Assertions and formal verification 65
2.5.1 Formal verification framework 65
2.5.2 Formal methodology 69
2.5.3 ECC example 74
2.5.4 Gradual exhaustive formal verification 77
2.6 Summary 80
3 SPECIFYING RTL PROPERTIES 81
3.1 Definitions and concepts 82
3.1.1 Property 82
3.1.2 Events 85
3.2 Property classification 85
3.2.1 Safety versus liveness 86
3.2.2 Constraint versus assertion 87
3.2.3 Declarative versus procedural 87
3.3 RTL assertion specification techniques 88
3.3.1 RTL invariant assertions 89
3.3.2 Declaring properties with PSL 92
3.3.3 RTL cycle related assertions 93
3.3.4 PSL and default clock declaration 94
3.3.5 Specifying sequences 95
3.3.6 Specifying eventualities 100
3.3.7 PSL built- in functions 102
3.4 Pragma- based assertions 102
3.5 SystemVerilog assertions 104
3.5.1 Immediate assertions 104
3.5.2 Concurrent assertions 106
3.5.3 System functions 115
3.6 PCI property specification example 116
3.6.1 PCI overview 116
3.7 Summary 122
4 PLI-BASED ASSERTIONS 123
4.1 Procedural assertions 124
4.1.1 A simple PLI assertion 125
4.1.2 Assertions within a simulation time slot 128
4.1.3 Assertions across simulation time slots 131
4.1.4 False firing across multiple time slots 136
4.2 PLI-based assertion library 138
4.2.1 Assert quiescent state 139
4.3 Summary 143
5 FUNCTIONAL COVERAGE 144
5.1 Verification approaches 145
5.2 Understanding coverage 146
5.2.1 Controllability versus observability 147
5.2.2 Types of traditional coverage metrics 147
5.2.3 What is functional coverage? 149
5.2.4 Building functional coverage models 151
5.2.5 Sources of functional coverage 152
5.3 Does functional coverage really work? 153
5.3.1 Benefits of functional coverage 154
5.3.2 Success stories 154
5.3.3 Why is functional coverage not used 155
5.4 Functional coverage methodology 156
5.4.1 Steps to functional coverage 157
5.4.2 Correct coverage density 158
5.4.3 Incorrect coverage density 160
5.4.4 Coverage analysis 161
5.4.5 Coverage best practices 164
5.4.6 Coverage-driven test generation 168
5.5 Specifying functional coverage 169
5.5.1 Embedded in the RTL 169
5.5.2 Functional coverage libraries 170
5.5.3 Assertion- based methods 171
5.5.4 Post processing 173
5.5.5 PLI logging and reporting 173
5.5.6 Simulation control 174
5.6 Functional coverage examples 175
5.7 AHB example 177
5.8 Summary 179
6 ASSERTION PATTERNS 180
6.1 Introduction to patterns 180
6.1.1 What are assertion patterns? 181
6.1.2 Elements of an assertion pattern 182
6.2 Signal patterns 183
6.2.1 X detection pattern 183
6.2.2 Valid range pattern 186
6.2.3 One- hot pattern 188
6.2.4 Gray-code pattern 191
6.3 Set patterns 192
6.3.1 Valid opcode pattern 192
6.3.2 Valid signal combination pattern 194
6.3.3 Invalid signal combination pattern 196
6.4 Conditional patterns 198
6.4.1 Conditional expression pattern 198
6.4.2 Sequence implication pattern 200
6.5 Past and future event patterns 204
6.5.1 Past event pattern 204
6.5.2 Future event pattern 206
6.6 Window patterns 208
6.6.1 Time-bounded window patterns 208
6.6.2 Event-bounded window patterns 211
6.7 Sequence patterns 213
6.7.1 Forbidden sequence patterns 213
6.7.2 Buffered data validity pattern 214
6.7.3 Tagged transaction pattern 215
6.7.4 Pipelined protocol pattern 218
6.8 Applying patterns to a real example 221
6.8.1 Intra-interface assertions 223
6.8.2 Inter-interface assertions 227
6.9 Summary 229
7 ASSERTION COOKBOOK 230
7.1 Queue-FIFO 232
7.1.1 Assertions 233
7.1.2 FIFO functional coverage 237
7.2 Fixed depth pipeline register 238
7.2.1 Assertions 239
7.2.2 Functional coverage 241
7.3 Stack-LIFO 241
7.3.1 Assertion 242
7.3.2 Functional coverage 243
7.4 Caches - direct mapped 244
7.4.1 Assertions 246
7.4.2 Functional coverage 248
7.5 Cache - set associative 250
7.5.1 Assertion 252
7.5.2 Functional coverage 253
7.6 FSM 255
7.6.1 Assertions 256
7.6.2 Functional coverage 258
7.7 Counters 259
7.7.1 Assertions 260
7.7.2 Functional coverage 261
7.8 Multiplexers 263
7.8.1 Encoded multiplexer 263
7.8.2 Decoded one-hot multiplexer 264
7.8.3 Priority multiplexer 265
7.8.4 Complex multiplexer 267
7.9 Encoder 268
7.10 Priority encoder 270
7.10.1 Functional coverage 270
7.11 Simple single request protocol 271
7.11.1 Assertions 271
7.11.2 Functional Coverage 272
7.12 In-order multiple request protocol 273
7.12.1 Functional Coverage 273
7.13 Out-of-order request protocol 276
7.13.1 Functional coverage 277
7.14 Memories 278
7.14.1 Assertions 279
7.15 Arbiter 281
7.15.1 Assertions 282
7.15.2 Functional coverage 284
7.16 Summary 285
8 SPECIFYING CORRECT BEHAVIOR 286
8.1 Natural language interpretation 286
8.1.1 Temporal ambiguity 287
8.1.2 Active ambiguity 290
8.1.3 Boundary ambiguity 292
8.1.5 Implicit assumption 295
8.1.6 Partial specification 296
8.2 Property specification guidelines 297
8.2.1 Sequence ambiguity 299
8.2.2 Syntax ambiguity 299
8.3 Clarity in higher- level specification 300
8.3.1 Implementation assertions 302
8.3.2 Higher-level requirements 304
8.3.3 Modeling high-level requirements 306
8.4 Summary 307
A OPENVERIFICATION LIBRARY 309
A. 1 OVL methodology advantages 309
A. 2 OVL standard definition 310
A. 2.1 OVL runtime macro controls 311
A. 2.2 Customizing OVL messages 312
A. 3 Firing OVL monitors 314
A. 4 Using OVL assertion monitors 315
A. 5 Checking invariant properties 316
A. 5.1 assert_always 316
A. 5.2 assert_never 318
A. 5.3 assert_ zero_ one_ hot 320
A.5.4 assert_range 321
A.6 Checking cycle relationships 323
A.6.1 assert_next 323
A.6.2 assert frame 325
A.6.3 assert_cycle_sequence 327
A.7 Checking event bounded windows 329
A.7.1 assert_win_change 329
A.7.2 assert_win_unchange 331
A.8 Checking time bounded 332
A.8.1 assert_change 333
A.8.2 assert_unchange 334
A.9 Checking state transitions 336
A.9.1 assert_no_transition 336
A.9.2 assert_transition 337
B PSL PROPERTY SPECIFICATIONLANGUAGE 339
B.1 Introduction to PSL 339
B.2 Operators and keywords 340
B. 3 PSL Boolean layer 341
B. 4 PSL Temporal Layer 342
B.4.1 SERE 342
B.4.2 Sequence 343
B.4.3 Braced SERE 343
B.4.4 SERE concatenation ( ) operator
B.4.5 Consecutive repetition ([* ]) operator 343
B.4.6 Nonconsecutive repetition ([= ]) operator 345
B.4.9 Sequence non-length-matching (& ) operator
B.4.10 Sequence length-matching (& &
B.4.11 Sequence or (|) operator 347
B.4.12 until* sequence operators 348
B.4.13 within sequence operators 348
B.4.14 next operator 348
B.4.15 eventually! operator 349
B.4.16 before* operators 349
B.5 PSL properties 352
B.5.1 Property declaration 352
B.5.2 Named properties 352
B.5.3 Property clocking 352
B.5.4 forall property replication 353
B.6 The verification layer 354
B.6.1 assert directive 354
B.6.2 assume directive 354
B.6.3 cover directive 354
B.7 The modeling layer 355
B.7.1 prev() 355
B.7.2 next() 355
B.7.3 stable() 356
B.7.4 rose() 356
B.7.5 fell() 357
B.7.6 isunknown() 357
B.7.7 countones() 357
B.7.8 onehot(), onehot0() 358
B. 8 BNF 358
C SYSTEMVERILOG ASSERTIONS 370
C.1 . Introduction to SystemVerilog 370
C.2 Operator and keywords 370
C.3 Sequence and property operations 372
C.3.1 Temporal delay 373
C.3.2 Consecutive repetition 374
C.3.3 Goto repetition 374
C.3.4 Nonconsecutive repetition 375
C.3.5 Sequence and Property AND 376
C.3.6 Sequence intersection 377
C.3.7 Sequence and Property OR 377
C.3.8 Boolean until (throughout) 378
C.3.9 Within sequence 379
C.3.10 Ended 379
C.3.11 Matched 380
C.3.12 First match 380
C.3.13 Property Implication 381
C.3.14 Conditional property selection 382
C.4 Property declarations 383
C.4.1 Sequence composition 385
C.5 Assert, Assume and Cover statements. 386
C.6 Dynamic data within sequences 387
C.7 System Functions 388
C.7.1 New operators 389
C.8 SystemTasks 390
C.9 BNF 391
C.9.1 Use of Assertions BNF: 392
C.9.2 Assertion statements 392
C.9.3 Property and sequence declarations 393
C.9.4 Property construction 394
C.9.5 Sequence construction 395
BIBLIOGRAPHY 396
Index 401

Produkt-Details

• Erscheint lt. Verlag: 28.12.2005
• Zusatzinfo: XXIII, 390 p.
• Verlagsort: New York
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Themenwelt: Informatik ► Weitere Themen ► CAD-Programme
• Themenwelt: Technik ► Elektrotechnik / Energietechnik
• Schlagworte: Material • Modeling • Patterns • RTL • Standard • verification • Verilog
• ISBN-10: 1-4020-8028-X / 140208028X
• ISBN-13: 978-1-4020-8028-9 / 9781402080289