[Ebook] Assertion based design 2nd Edition

opqrst

TABLE OF CONTENTS
Chapter 1 Introduction 1
1.1
1.2
1.3
Property checking
Verification techniques
What is an assertion?
1.3.1
1.3.2
1.3.3
1.3.4
A historical perspective
Do assertions really work?
What are the benefits of assertions?
Why are assertions not used?
1.4 Phases of the design process
1.4.1
1.4.2
1.4.3
Ensuring requirements are satisfied
Techniques for ensuring consistency
Roles and ownership
1.5 Summary
1
2
3
4
6
7
11
14
16
18
19
20
Chapter 2 Assertion Methodology 21
2.1 Design methodology
2.1.1
2.1.2
2.1.3
2.1.4
2.1.5
Project planning
Design requirements
Design documents
Design reviews
Design validation
21
22
27
28
29
30
2.2 Assertion methodology for new designs
2.2.1
2.2.2
2.2.3
2.2.4
2.2.5
Key learnings
Best practices
Assertion density
Process for adding assertions
When not to add assertions
30
31
33
37
39
39
2.3
2.4
2.5
Assertion methodology for existing designs
Assertions and simulation
Assertions and formal verification
2.5.1
2.5.2
2.5.3
2.5.4
Formal verification framework
Formal methodology
ECC example
Gradual exhaustive formal verification
40
42
44
44
48
53
56
T a b l e of C o n t e n t s vii
2.6 Summary 59
Chapter 3 Specifying RTL Properties 61
3.1 Definitions and concepts
3.1.1
3.1.2
Property
Events
3.2 Property classification
3.2.1
3.2.2
3.2.3
Safety versus liveness
Constraint versus assertion
Declarative versus procedural
3.3 RTL assertion specification techniques
3.3.1
3.3.2
3.3.3
3.3.4
3.3.5
3.3.6
3.3.7
RTL invariant assertions
Declaring properties with PSL
RTL cycle related assertions
PSL and default clock declaration
Specifying sequences
Specifying eventualities
PSL built-in functions
3.4
3.5
Pragma-based assertions
Systemverilog assertions
3.5.1
3.5.2
3.5.3
Immediate assertions
Concurrent assertions
System functions
3.6 PCI property specification example
3.6.1 PCI overview
3.7 Summary
Chapter 4 PLI-Based Assertions
4.1 Procedural assertions
4.1.1
4.1.2
4.1.3
4.1.4
A simple PLI assertion
Assertions within a simulation time slot
Assertions across simulation time slots
False firing across multiple time slots
4.2 PLI-based assertion library
4.2.1 Assert quiescent state
4.3 Summary
Chapter 5 Functional Coverage
5.1
5.2
Verification approaches
Understanding coverage
5.2.1
5.2.2
5.2.3
5.2.4
5.2.5
Controllability versus observability
Types of traditional coverage metrics
What is functional coverage?
Building functional coverage models
Sources of functional coverage
62
62
65
65
66
67
67
68
69
72
73
74
75
80
82
82
84
84
86
95
96
96
102
103
104
105
108
111
116
118
119
123
125
126
127
128
128
130
132
133
v i i i A s s e r t i o n - B a s e d D e s i g n
5.3 Does functional coverage really work?
5.3.1
5.3.2
5.3.3
Benefits of functional coverage
Success stories
Why is functional coverage not used
5.4 Functional coverage methodology
5.4.1
5.4.2
5.4.3
5.4.4
5.4.5
5.4.6
Steps to functional coverage
Correct coverage density
Incorrect coverage density
Coverage analysis
Coverage best practices
Coverage-driven test generation
5.5 Specifying functional coverage
5.5.1
5.5.2
5.5.3
5.5.4
5.5.5
5.5.6
Embedded in the RTL
Functional coverage libraries
Assertion-based methods
Post processing
PLI logging and reporting
Simulation control
5.6
5.7
5.8
Functional coverage examples
AHB example
Summary
Chapter 6 Assertion Patterns
6.1 Introduction to patterns
6.1.1
6.1.2
What are assertion patterns?
Elements of an assertion pattern
6.2 Signal patterns
6.2.1
6.2.2
6.2.3
6.2.4
X detection pattern
Valid range pattern
One-hot pattern
Gray-code pattern
6.3 Set patterns
6.3.1
6.3.2
6.3.3
Valid opcode pattern
Valid signal combination pattern
Invalid signal combination pattern
6.4 Conditional patterns
6.4.1
6.4.2
Conditional expression pattern
Sequence implication pattern
6.5 Past and future event patterns
6.5.1
6.5.2
Past event pattern
Future event pattern
6.6 Window patterns
6.6.1
6.6.2
Time-bounded window patterns
Event-bounded window patterns
6.7 Sequence patterns
6.7.1
6.7.2
Forbidden sequence patterns
Buffered data validity pattern
134
135
135
136
137
138
139
141
142
145
149
150
150
151
152
154
154
155
156
158
160
161
161
162
163
164
164
167
169
172
173
173
175
177
179
179
181
185
185
187
189
189
192
194
194
195
T a b l e of C o n t e n t s ix
6.7.3 Tagged transaction pattern
6.7.4 Pipelined protocol pattern
6.8 Applying patterns to a real example
6.8.1
6.8.2
Intra-interface assertions
Inter-interface assertions
6.9 Summary
196
199
202
204
208
210
Chapter 7 Assertion Cookbook
7.1
7.2
7.3
7.4
7.5
7.6
7.7
7.8
Queue—fifo
Fixed depth pipeline register
Stack—LIFO
Caches—direct mapped
Cache—set associative
FSM
Counters
Multiplexers
7.8.1
7.8.2
7.8.3
7.8.4
Encoded multiplexer
Decoded one-hot multiplexer
Priority multiplexer
Complex multiplexer
7.9 Encoder
7.10
7.11
7.12
7.13
7.14
7.15
7.16
Priority encoder
Simple single request protocol
In-order multiple request protocol
Out-of-order request protocol
Memories
Arbiter
Summary
211
213
219
222
225
231
236
240
244
244
245
246
248
249
251
252
254
257
259
262
266
Chapter 8 Specifying Correct Behavior 267
8.1 Natural language interpretation
8.1.1
8.1.2
8.1.3
8.1.4
8.1.5
8.1.6
Temporal ambiguity
Active ambiguity
Boundary ambiguity
Too strong interpretation
Implicit assumption
Partial specification
8.2 Property specification guidelines
8.2.2 Syntax ambiguity
8.3 Clarity in higher-level specification
8.3.1
8.3.2
8.3.3
Implementation assertions
Higher-level requirements
Modeling high-level requirements
8.4 Summary
267
268
271
273
274
276
277
278
280
281
283
285
287
288
x A s s e r t i o n - B a s e d D e s i g n
Appendix A Open Verification Library 291
A.1
A.2
OVL methodology advantages
OVL standard definition
A.2.1 OVL runtime macro controls
A.2.2 Customizing OVL messages
A.3
A.4
A.5
Firing OVL monitors
Using OVL assertion monitors
Checking invariant properties
A.5.1
A.5.2
A.5.3
A.5.4
assert_always
assert_never
assert_zero_one_hot
assert_range
A.6 Checking cycle relationships
A.6.1
A.6.2
A.6.3
assert_next
assert_frame
assert_cycle_sequence
A.7 Checking event bounded windows
A.7.1 assert_win_change
A.7.2 assert_win_unchange
A.8 Checking time bounded windows
A.8.1
A.8.2
assert_change
assert_unchange
A.9 Checking state transitions
A.9.1
A.9.2
assert_no_transition
assert_transition
291
292
293
294
296
297
298
298
300
302
303
305
305
307
309
311
311
313
314
315
316
318
318
319
Appendix B PSL Property Specification Language 321
B.1
B.2
B.3
B.4
Introduction to PSL
Operators and keywords
PSL Boolean layer
PSL Temporal Layer
B.4.1
B.4.2
B.4.3
B.4.4
B.4.5
B.4.6
B.4.7
B.4.8
B.4.9
SERE
Sequence
Braced SERE
SERE concatenation ( ; ) operator
Consecutive repetition ([* ]) operator
Nonconsecutive repetition ([= ]) operator
Goto repetition ([-> ]) operator
Sequence fusion (: ) operator
Sequence non-length-matching (& ) operator
B.4.10
B.4.11
B.4.12
B.4.13
B.4.14
B.4.15
B.4.16
Sequence length-matching (&&) operator
Sequence or ( | ) operator
until* sequence operators
within sequence operators
next operator
eventually! operator
before* operators
321
322
323
324
324
325
325
325
325
327
328
329
329
329
329
330
330
330
331
331
T a b l e of C o n t e n t s xi

opqrst

part 2

opqrst

part 3

opqrst

finished.

yangyuf

谢谢搂住共享
很有用

yangyuf

楼主是好人啊

frank123

楼主是好人啊

armhy

谢谢. 下载了.

weix

多谢了！一直在找这本书

lonelyman

多谢楼主无私共享!