|
|
1 | (8) |
|
1.1 How Will This Book Help You? |
|
|
4 | (1) |
|
1.2 System Verilog Assertions and Functional Coverage Under IEEE 1800 System Verilog Umbrella |
|
|
5 | (2) |
|
1.3 System Verilog Assertions Evolution |
|
|
7 | (2) |
|
2 System Verilog Assertions |
|
|
9 | (22) |
|
2.1 What Is an Assertion? |
|
|
9 | (1) |
|
2.2 Why Assertions? What Are the Advantages? |
|
|
9 | (7) |
|
2.2.1 Assertions Shorten Time to Develop |
|
|
10 | (1) |
|
2.2.2 Assertions Improve Observability |
|
|
11 | (1) |
|
2.2.3 Assertions Provide Temporal Domain Functional Coverage |
|
|
11 | (3) |
|
2.2.4 Assertion Based Methodology Allows for Full Random Verification |
|
|
14 | (1) |
|
2.2.5 Assertions Help Detect Bugs not Easily Observed at Primary Outputs |
|
|
15 | (1) |
|
2.2.6 Other Major Benefits |
|
|
15 | (1) |
|
2.3 How Do Assertions Work with an Emulator? |
|
|
16 | (1) |
|
2.4 Assertions in Static Formal |
|
|
17 | (2) |
|
2.5 One-Time Effort, Many Benefits |
|
|
19 | (1) |
|
|
20 | (2) |
|
2.6.1 Who Will Add Assertions? War Within! |
|
|
21 | (1) |
|
2.7 A Simple PCI Read Example---Creating an Assertions Test Plan |
|
|
22 | (2) |
|
2.8 What Type of Assertions Should I Add? |
|
|
24 | (1) |
|
2.9 Protocol for Adding Assertions |
|
|
25 | (1) |
|
2.10 How Do I Know I Have Enough Assertions? |
|
|
26 | (1) |
|
2.11 Use Assertions for Specification and Review |
|
|
26 | (1) |
|
|
27 | (1) |
|
2.13 Conventions Used in the Book |
|
|
28 | (3) |
|
|
31 | (4) |
|
4 Concurrent Assertions---Basics (Sequence, Property, Assert) |
|
|
35 | (32) |
|
4.1 Implication Operator, Antecedent and Consequent |
|
|
40 | (2) |
|
|
42 | (2) |
|
4.3 Sampling Edge (Clock Edge) Value: How Are Assertions Evaluated in a Simulation Time Tick? |
|
|
44 | (9) |
|
4.3.1 Default Clocking Block |
|
|
48 | (4) |
|
|
52 | (1) |
|
4.4 Concurrent Assertions Are Multi-threaded |
|
|
53 | (2) |
|
|
55 | (3) |
|
4.6 Disable (Property) Operator---'Disable Iff' |
|
|
58 | (2) |
|
4.7 Severity Levels (for Both Concurrent and Immediate Assertions) |
|
|
60 | (1) |
|
|
61 | (4) |
|
4.8.1 Binding Properties (Scope Visibility) |
|
|
62 | (2) |
|
4.8.2 Assertion Adoption in Existing Design |
|
|
64 | (1) |
|
4.9 Difference Between `Sequence' and `Property' |
|
|
65 | (2) |
|
5 Sampled Value Functions $rose, $fell, $stable, $past |
|
|
67 | (14) |
|
5.1 $rose---Edge Detection in Property/Sequence |
|
|
68 | (4) |
|
5.1.1 Edge Detection Is Useful Because |
|
|
68 | (3) |
|
5.1.2 $fell---Edge Detection in Property/Sequence |
|
|
71 | (1) |
|
5.1.3 $rose, $fell---in Procedural |
|
|
71 | (1) |
|
|
72 | (1) |
|
5.2.1 $stable in Procedural Block |
|
|
73 | (1) |
|
|
73 | (8) |
|
5.3.1 Application: $past () |
|
|
78 | (1) |
|
5.3.2 $past Rescues $fell! |
|
|
78 | (3) |
|
|
81 | (66) |
|
|
81 | (3) |
|
6.1.1 Clock Delay Operator: ##m Where m=0 |
|
|
82 | (2) |
|
6.2 ##[ m:nL-Clock Delay Range |
|
|
84 | (10) |
|
6.2.1 Clock Delay Range Operator: ##[ m:n]: Multiple Threads |
|
|
85 | (9) |
|
6.2.2 Clock Delay Range Operator:: ##[ m:n] (m=0; n=$) |
|
|
94 | (1) |
|
6.3 [ *m]---Consecutive Repetition Operator |
|
|
94 | (4) |
|
6.4 [ *m:n]---Consecutive Repetition Range |
|
|
98 | (9) |
|
6.4.1 Application: Consecutive Repetition Range Operator |
|
|
101 | (6) |
|
6.5 [ =m]---Repetition Non-consecutive |
|
|
107 | (4) |
|
6.6 [ =m:n]---Repetition Non-consecutive Range |
|
|
111 | (3) |
|
6.6.1 Application: Repetition Non-consecutive Operator |
|
|
112 | (2) |
|
6.7 [ ->m] Non-consecutive GoTo Repetition Operator |
|
|
114 | (1) |
|
6.8 Difference Between [ =m:n] and [ ->m:n] |
|
|
115 | (2) |
|
6.8.1 Application: GoTo Repetition---Non-consecutive Operator |
|
|
116 | (1) |
|
|
117 | (4) |
|
6.9.1 Application: Sig1 throughout Seq1 |
|
|
118 | (3) |
|
|
121 | (3) |
|
6.10.1 Application: Seq1 within Seq2 |
|
|
122 | (1) |
|
6.10.2 `within' Operator PASS CASES |
|
|
123 | (1) |
|
6.10.3 `within' Operator: FAIL CASES |
|
|
124 | (1) |
|
|
124 | (3) |
|
6.11.1 Application: `and' Operator |
|
|
127 | (1) |
|
|
127 | (4) |
|
6.12.1 Application: or Operator |
|
|
128 | (3) |
|
6.13 Seq1 `intersect' Seq2 |
|
|
131 | (1) |
|
6.14 Application: `intersect' Operator |
|
|
132 | (5) |
|
6.14.1 Application: intersect Operator (Interesting Application) |
|
|
133 | (4) |
|
6.14.2 `intersect' and `and' :: What's the Difference? |
|
|
137 | (1) |
|
|
137 | (4) |
|
6.15.1 Application: first_match |
|
|
138 | (3) |
|
|
141 | (2) |
|
6.16.1 Application: not Operator |
|
|
141 | (2) |
|
6.17 if (expression) property_expr1 else property_expr2 |
|
|
143 | (2) |
|
6.17.1 Application: if then else |
|
|
145 | (1) |
|
|
145 | (2) |
|
7 System Functions and Tasks |
|
|
147 | (8) |
|
|
147 | (2) |
|
|
149 | (1) |
|
|
150 | (1) |
|
7.3.1 $countones (as Boolean) |
|
|
151 | (1) |
|
7.4 $assertoff, $asserton, $assertkill |
|
|
151 | (4) |
|
|
155 | (12) |
|
8.1 Multiply-Clocked Sequences and Properties |
|
|
155 | (12) |
|
8.1.1 Multiply Clocked Sequences |
|
|
156 | (1) |
|
8.1.2 Multiply Clocked Sequences--Legal and Illegal Sequences |
|
|
157 | (1) |
|
8.1.3 Multiply Clocked Properties---`and' Operator |
|
|
158 | (1) |
|
8.1.4 Multiply Clocked Properties---`or' Operator |
|
|
159 | (2) |
|
8.1.5 Multiply Clocked Properties---`not'---Operator |
|
|
161 | (1) |
|
8.1.6 Multiply Clocked Properties---Clock Resolution |
|
|
161 | (3) |
|
8.1.7 Multiply Clocked Properties---Legal and Illegal Conditions |
|
|
164 | (3) |
|
|
167 | (14) |
|
9.1 Application: Local Variables |
|
|
179 | (2) |
|
|
181 | (6) |
|
10.1 Application: Recursive Property |
|
|
182 | (1) |
|
10.2 Application: Recursive Property |
|
|
183 | (4) |
|
11 Detecting and Using Endpoint of a Sequence |
|
|
187 | (14) |
|
11.1 .triggered (Replaced for .ended) |
|
|
187 | (8) |
|
|
195 | (6) |
|
11.2.1 Application: matched |
|
|
198 | (3) |
|
|
201 | (4) |
|
13 `assume' and Formal (Static Functional) Verification |
|
|
205 | (2) |
|
14 Very Important Topics and Applications |
|
|
207 | (40) |
|
14.1 Asynchronous FIFO Assertions |
|
|
207 | (10) |
|
14.1.1 Asynchronous FIFO Design |
|
|
208 | (2) |
|
14.1.2 Asynchronous FIFO Testbench and Assertions |
|
|
210 | (4) |
|
14.1.3 Test the Testbench |
|
|
214 | (3) |
|
14.2 Embedding Concurrent Assertions in Procedural Code |
|
|
217 | (5) |
|
|
222 | (3) |
|
14.4 Sequence as a Formal Argument |
|
|
225 | (1) |
|
14.5 Sequence as an Antecedent |
|
|
226 | (1) |
|
14.6 Sequence in Sensitivity List |
|
|
227 | (1) |
|
|
228 | (1) |
|
14.8 Clock Delay: What if You Want Variable Clock Delay? |
|
|
229 | (2) |
|
14.9 What if the `Action Block' Is Blocking? |
|
|
231 | (3) |
|
14.10 Interesting Observation with Multiple (Nested) Implications in a Property. Be Careful |
|
|
234 | (1) |
|
14.11 Subsequence in a Sequence |
|
|
235 | (1) |
|
|
236 | (1) |
|
14.13 Refinement on a Theme |
|
|
237 | (1) |
|
14.14 Simulation Performance Efficiency |
|
|
237 | (2) |
|
14.15 It's a Vacuous World! Huh? |
|
|
239 | (4) |
|
14.15.1 Concurrent Assertion---Without---An Implication |
|
|
239 | (1) |
|
14.15.2 Concurrent Assertion---With---An Implication |
|
|
240 | (1) |
|
14.15.3 Vacuous Pass. What? |
|
|
241 | (1) |
|
14.15.4 Concurrent Assertion---with `Cover' |
|
|
241 | (2) |
|
|
243 | (4) |
|
15 Asynchronous Assertions!!! |
|
|
247 | (4) |
|
16 IEEE-1800-2009/2012 Features |
|
|
251 | (54) |
|
16.1 Strong and Weak Sequences |
|
|
251 | (1) |
|
16.2 Deferred Immediate Assertions |
|
|
252 | (4) |
|
|
256 | (1) |
|
|
257 | (1) |
|
16.5 $past_gclk, $rose_gclk, $fell_gclk, $stable_gclk, $changed_ gclk, $future_gclk. $rising_gclk, $falling_gclk, $steady_gclk, $changing_gclk |
|
|
258 | (3) |
|
16.6 `followed by' Properties #-# and #=# |
|
|
261 | (1) |
|
16.7 `always' and `s_always' Property |
|
|
262 | (2) |
|
16.8 `eventually', `s_eventually' |
|
|
264 | (1) |
|
16.9 `until', `s_until' `until_with' and `s_until_with' |
|
|
265 | (2) |
|
16.10 `nexttime' and `s_nexttime' |
|
|
267 | (3) |
|
|
270 | (1) |
|
16.12 $inferred_clock and $inferred_disable |
|
|
271 | (2) |
|
|
273 | (7) |
|
|
274 | (1) |
|
16.13.2 let: With Parameters |
|
|
275 | (2) |
|
16.13.3 let: In Immediate and Concurrent Assertions |
|
|
277 | (3) |
|
16.14 `restrict' for Formal Verification |
|
|
280 | (1) |
|
16.15 Abort Properties: reject_on, accept_on, sync_reject_on, sync_accept_on |
|
|
280 | (4) |
|
16.16 $assertpassoff, $assertpasson, $assertfailoff, $assertfailon, $assertnonvacuouson, $assertvacuousoff |
|
|
284 | (1) |
|
|
285 | (5) |
|
|
290 | (15) |
|
|
295 | (1) |
|
16.18.2 Checkers: Illegal Conditions |
|
|
296 | (2) |
|
16.18.3 Checkers: Important Points |
|
|
298 | (3) |
|
16.18.4 Checker: Instantiation Rules |
|
|
301 | (4) |
|
17 System Verilog Assertions LABs |
|
|
305 | (38) |
|
17.1 LAB1: Assertions with/Without Implication and `bind' |
|
|
305 | (5) |
|
17.1.1 LAB1: `bind' DUT Model and Testbench |
|
|
306 | (2) |
|
|
308 | (2) |
|
17.2 LAB2: Overlap and Non-overlap Operators |
|
|
310 | (3) |
|
17.2.1 LAB2 DUT Model and Testbench |
|
|
310 | (1) |
|
|
311 | (2) |
|
17.3 LAB3: Synchronous FIFO Assertions |
|
|
313 | (8) |
|
17.3.1 LAB3: DUT Model and Testbench |
|
|
313 | (4) |
|
|
317 | (4) |
|
|
321 | (6) |
|
|
324 | (3) |
|
17.5 LAB5: Data Transfer Protocol |
|
|
327 | (9) |
|
|
335 | (1) |
|
17.6 LAB6: PCI Read Protocol |
|
|
336 | (7) |
|
|
340 | (3) |
|
18 System Verilog Assertions---LAB Answers |
|
|
343 | (18) |
|
18.1 LAB1: Answers: `bind' and Implication Operators |
|
|
344 | (5) |
|
18.2 LAB2: Answers: Overlap and Non-overlap Operators |
|
|
349 | (4) |
|
18.3 LAB3: Answers: Synchronous FIFO |
|
|
353 | (2) |
|
18.4 LAB4: Answers: Counter |
|
|
355 | (1) |
|
18.5 LAB5: Answers: Data Transfer Protocol |
|
|
356 | (3) |
|
18.6 LAB6: Answers: PCI Read Protocol |
|
|
359 | (2) |
|
|
361 | (6) |
|
19.1 Difference Between Code Coverage and Functional Coverage |
|
|
361 | (1) |
|
19.2 Assertion Based Verification (ABV) and Functional Coverage (FC) Based Methodology |
|
|
362 | (5) |
|
|
366 | (1) |
|
20 Functional Coverage---Language Features |
|
|
367 | (24) |
|
20.1 Covergroup/Coverpoint |
|
|
367 | (1) |
|
20.2 System Verilog `Covergroup'---Basics |
|
|
368 | (1) |
|
20.3 System Verilog Coverpoint Basics |
|
|
368 | (4) |
|
20.3.1 Covergroup/Coverpoint Example |
|
|
371 | (1) |
|
20.4 System Verilog `Bins'---Basics |
|
|
372 | (6) |
|
20.4.1 Covergroup/Coverpoint with Bins---Example |
|
|
374 | (1) |
|
20.4.2 System Verilog `covergroup'----Formal and Actual Arguments |
|
|
375 | (1) |
|
20.4.3 `covergroup' in a `class' |
|
|
376 | (2) |
|
|
378 | (4) |
|
|
382 | (9) |
|
20.6.1 `Bins' for Transition Coverage |
|
|
382 | (4) |
|
|
386 | (1) |
|
|
386 | (1) |
|
|
387 | (1) |
|
20.6.5 `binsof and `intersect' |
|
|
388 | (3) |
|
21 Performance Implications of Coverage Methodology |
|
|
391 | (4) |
|
21.1 Know What You Should Cover |
|
|
391 | (1) |
|
21.2 Know When You Should Cover |
|
|
392 | (1) |
|
21.3 When to `Cover' (Performance Implication) |
|
|
392 | (1) |
|
21.4 Application: Have You Transmitted All Different Lengths of a Frame? |
|
|
393 | (2) |
|
|
395 | (8) |
|
22.1 Coverage Options---Instance Specific---Example |
|
|
397 | (1) |
|
22.2 Coverage Options---Instance Specific Per-Syntactic Level |
|
|
397 | (3) |
|
22.3 Coverage Options for `Covergroup' Type---Example |
|
|
400 | (3) |
Index |
|
403 | |