Foster / Krolnik / Lacey Assertion-Based Design

2. Auflage 2004
ISBN: 978-1-4020-8028-9
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 406 Seiten

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.

Autoren/Hrsg.

Foster, Harry D.

Krolnik, Adam C.

Lacey, David J.

Inhaltsverzeichnis

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