Foreword for "Formal Verification: An Essential Toolkit for Modern VLSI Design" |
|
xiii | |
Acknowledgments |
|
xvii | |
|
Chapter 1 Formal verification: from dreams to reality |
|
|
1 | (22) |
|
|
2 | (1) |
|
|
3 | (1) |
|
|
4 | (2) |
|
FV: The Next Level of Depth |
|
|
6 | (7) |
|
|
6 | (1) |
|
General Usage Models for FV |
|
|
7 | (1) |
|
|
8 | (3) |
|
FV Methods Not Discussed in This Book |
|
|
11 | (2) |
|
The Emergence of Practical FV |
|
|
13 | (3) |
|
Early Automated Reasoning |
|
|
13 | (1) |
|
Applications to Computer Science |
|
|
14 | (1) |
|
Model Checking Becomes Practical |
|
|
14 | (1) |
|
The Standardizing of Assertions |
|
|
15 | (1) |
|
Challenges in Implementing FV |
|
|
16 | (2) |
|
Fundamental Limitations of Mathematics |
|
|
16 | (1) |
|
|
17 | (1) |
|
|
17 | (1) |
|
Amplifying the Power of Formal |
|
|
18 | (1) |
|
Getting the Most Out of This Book |
|
|
19 | (2) |
|
Practical Tips from This Chapter |
|
|
20 | (1) |
|
|
21 | (2) |
|
Chapter 2 Basic formal verification algorithms |
|
|
23 | (26) |
|
Formal Verification (FV) in the Validation Process |
|
|
23 | (3) |
|
A Simple Vending Machine Example |
|
|
24 | (2) |
|
|
26 | (3) |
|
|
28 | (1) |
|
Formalizing Operation Definitions |
|
|
29 | (1) |
|
Building Truth Tables Intelligently |
|
|
29 | (1) |
|
|
30 | (1) |
|
|
30 | (5) |
|
Basic Boolean Algebra Laws |
|
|
32 | (1) |
|
|
32 | (3) |
|
|
35 | (4) |
|
Computing a BDD for a Circuit Design |
|
|
37 | (1) |
|
|
38 | (1) |
|
|
39 | (7) |
|
|
40 | (1) |
|
|
41 | (2) |
|
The Davis---Putnam SAT Algorithm |
|
|
43 | (2) |
|
The Davis Logemann Loveland (DLL) SAT Algorithm |
|
|
45 | (1) |
|
|
46 | (1) |
|
|
47 | (2) |
|
Chapter 3 Introduction to systemverilog assertions |
|
|
49 | (38) |
|
|
50 | (4) |
|
|
50 | (1) |
|
|
51 | (1) |
|
|
51 | (1) |
|
|
52 | (1) |
|
Clarification on Assertion Statements |
|
|
52 | (1) |
|
SVA Assertion Language Basics |
|
|
53 | (1) |
|
|
54 | (12) |
|
Writing Immediate Assertions |
|
|
55 | (1) |
|
Complications of Procedural Code and Motivation for Assert Final |
|
|
56 | (2) |
|
Location in Procedural Blocks |
|
|
58 | (1) |
|
|
58 | (1) |
|
Concurrent Assertion Basics and Clocking |
|
|
59 | (1) |
|
Sampling and Assertion Clocking |
|
|
60 | (1) |
|
|
61 | (1) |
|
Concurrent Assertion Clock Edges |
|
|
62 | (2) |
|
Concurrent Assertion Reset (Disable) Conditions |
|
|
64 | (1) |
|
Setting Default Clock and Reset |
|
|
65 | (1) |
|
Sequences, Properties, and Concurrent Assertions |
|
|
66 | (17) |
|
Sequence Syntax and Examples |
|
|
67 | (4) |
|
Property Syntax and Examples |
|
|
71 | (3) |
|
Named Sequences and Properties |
|
|
74 | (1) |
|
Assertions and Implicit Multithreading |
|
|
75 | (1) |
|
|
76 | (7) |
|
|
83 | (3) |
|
Practical Tips from This Chapter |
|
|
84 | (2) |
|
|
86 | (1) |
|
Chapter 4 Formal property verification |
|
|
87 | (32) |
|
|
87 | (3) |
|
Example for This Chapter: Combination Lock |
|
|
90 | (1) |
|
Bringing Up a Basic FPV Environment |
|
|
91 | (12) |
|
How Is FPV Different from Simulation? |
|
|
103 | (12) |
|
What Types and Sizes of Models Can Be Run? |
|
|
105 | (1) |
|
How Do We Reach Targeted Behaviors? |
|
|
105 | (1) |
|
|
106 | (5) |
|
Deciding Where and How to Run FPV |
|
|
111 | (4) |
|
|
115 | (2) |
|
Practical Tips from This Chapter |
|
|
116 | (1) |
|
|
117 | (2) |
|
Chapter 5 Effective FPV for design exercise |
|
|
119 | (34) |
|
Example for This Chapter: Traffic Light Controller |
|
|
120 | (3) |
|
Creating a Design Exercise Plan |
|
|
123 | (8) |
|
|
124 | (1) |
|
Major Properties for Design Exercise |
|
|
125 | (1) |
|
|
126 | (3) |
|
|
129 | (1) |
|
|
130 | (1) |
|
Setting Up the Design Exercise FPV Environment |
|
|
131 | (2) |
|
|
131 | (1) |
|
|
132 | (1) |
|
|
132 | (1) |
|
|
133 | (1) |
|
|
133 | (1) |
|
|
133 | (7) |
|
|
133 | (2) |
|
Wiggling Stage 1: Our First Short Waveform |
|
|
135 | (2) |
|
Debugging Another Short Waveform |
|
|
137 | (3) |
|
Exploring More Interesting Behaviors |
|
|
140 | (6) |
|
Answering Some New Questions |
|
|
140 | (3) |
|
|
143 | (3) |
|
Removing Simplifications and Exploring More Behaviors |
|
|
146 | (4) |
|
|
149 | (1) |
|
|
150 | (2) |
|
Practical Tips from This Chapter |
|
|
151 | (1) |
|
|
152 | (1) |
|
Chapter 6 Effective FPV for verification |
|
|
153 | (36) |
|
Deciding on Your FPV Goals |
|
|
154 | (2) |
|
|
154 | (1) |
|
|
155 | (1) |
|
|
156 | (1) |
|
Example for This Chapter: Simple ALU |
|
|
157 | (1) |
|
|
158 | (3) |
|
Creating the FPV Verification Plan |
|
|
161 | (22) |
|
|
162 | (1) |
|
|
163 | (4) |
|
|
167 | (3) |
|
Quality Checks and Exit Criteria |
|
|
170 | (6) |
|
|
176 | (1) |
|
|
177 | (5) |
|
Expanding the Cover Points |
|
|
182 | (1) |
|
Removing Simplifications and Exploring More Behaviors |
|
|
183 | (2) |
|
The Road to Full Proof FPV |
|
|
184 | (1) |
|
|
185 | (3) |
|
Practical Tips from This Chapter |
|
|
186 | (2) |
|
|
188 | (1) |
|
Chapter 7 FPV "Apps" for specific SOC problems |
|
|
189 | (36) |
|
Reusable Protocol Verification |
|
|
190 | (8) |
|
Basic Design of the Reusable Property Set |
|
|
191 | (2) |
|
Property Direction Issues |
|
|
193 | (2) |
|
Verifying Property Set Consistency |
|
|
195 | (2) |
|
|
197 | (1) |
|
Unreachable Coverage Elimination |
|
|
198 | (3) |
|
The Role of Assertions in UCE |
|
|
200 | (1) |
|
Covergroups and Other Coverage Types |
|
|
201 | (1) |
|
Connectivity Verification |
|
|
201 | (6) |
|
Model Build for Connectivity |
|
|
202 | (2) |
|
Specifying the Connectivity |
|
|
204 | (1) |
|
Possible Connectivity FPV Complications |
|
|
205 | (2) |
|
Control Register Verification |
|
|
207 | (8) |
|
Specifying Control Register Requirements |
|
|
209 | (1) |
|
SVA Assertions for Control Registers |
|
|
210 | (2) |
|
Major Challenges of Control Register Verification |
|
|
212 | (3) |
|
|
215 | (6) |
|
Building the FPV Environment |
|
|
215 | (3) |
|
The Paradox of Too Much Information |
|
|
218 | (1) |
|
Using Semiformal Design Exploration |
|
|
219 | (1) |
|
Proving Your Bug Fixes Correct |
|
|
220 | (1) |
|
|
221 | (3) |
|
Practical Tips from This Chapter |
|
|
221 | (3) |
|
|
224 | (1) |
|
Chapter 8 Formal equivalence verification |
|
|
225 | (36) |
|
Types of Equivalence to Check |
|
|
226 | (5) |
|
Combinational Equivalence |
|
|
226 | (2) |
|
|
228 | (1) |
|
Transaction-Based Equivalence |
|
|
229 | (2) |
|
|
231 | (7) |
|
|
231 | (2) |
|
|
233 | (5) |
|
|
238 | (10) |
|
|
238 | (2) |
|
Key Point Selection and Mapping |
|
|
240 | (5) |
|
Assumptions and Constraints |
|
|
245 | (2) |
|
|
247 | (1) |
|
Additional FEV Challenges |
|
|
248 | (8) |
|
|
248 | (1) |
|
|
249 | (2) |
|
|
251 | (1) |
|
|
252 | (4) |
|
|
256 | (3) |
|
Practical Tips from This Chapter |
|
|
256 | (3) |
|
|
259 | (2) |
|
Chapter 9 Formal verification's greatest bloopers: the danger of false positives |
|
|
261 | (28) |
|
Misuse of the SVA Language |
|
|
263 | (6) |
|
|
263 | (1) |
|
Assertion at Both Clock Edges |
|
|
264 | (1) |
|
Short-Circuited Function with Assertion |
|
|
265 | (1) |
|
Subtle Effects of Signal Sampling |
|
|
266 | (1) |
|
Liveness Properties That Are Not Alive |
|
|
267 | (1) |
|
Preventing SVA-Related False Positives |
|
|
268 | (1) |
|
|
269 | (8) |
|
Misleading Cover Point with Bad Reset |
|
|
270 | (1) |
|
Proven Memory Controller That Failed Simulation |
|
|
271 | (1) |
|
Contradiction Between Assumption and Constraint |
|
|
272 | (2) |
|
The Queue That Never Fills, Because It Never Starts |
|
|
274 | (1) |
|
Preventing Vacuity: Tool and User Responsibility |
|
|
275 | (2) |
|
Implicit or Unstated Assumptions |
|
|
277 | (5) |
|
Libraries with Schematic Assumptions |
|
|
277 | (2) |
|
Expectations for Multiply-Driven Signals |
|
|
279 | (1) |
|
Unreachable Logic Elements: Needed or Not? |
|
|
279 | (2) |
|
Preventing Misunderstandings |
|
|
281 | (1) |
|
|
282 | (3) |
|
|
282 | (1) |
|
Case-Splitting with Missing Cases |
|
|
283 | (1) |
|
|
284 | (1) |
|
|
284 | (1) |
|
|
285 | (2) |
|
Practical Tips from This Chapter |
|
|
286 | (1) |
|
|
287 | (2) |
|
Chapter 10 Dealing with complexity |
|
|
289 | (36) |
|
Design State and Associated Complexity |
|
|
289 | (2) |
|
Example for This Chapter: Memory Controller |
|
|
291 | (2) |
|
Observing Complexity Issues |
|
|
293 | (1) |
|
Simple Techniques for Convergence |
|
|
294 | (13) |
|
Choosing the Right Battle |
|
|
294 | (1) |
|
|
295 | (2) |
|
|
297 | (1) |
|
Parameters and Size Reduction |
|
|
297 | (1) |
|
|
298 | (2) |
|
|
300 | (2) |
|
|
302 | (3) |
|
|
305 | (1) |
|
|
306 | (1) |
|
Helper Assumptions ... and Not-So-Helpful Assumptions |
|
|
307 | (3) |
|
Writing Custom Helper Assumptions |
|
|
308 | (1) |
|
Leveraging Proven Assertions |
|
|
308 | (1) |
|
Do You Have Too Many Assumptions? |
|
|
309 | (1) |
|
Generalizing Analysis Using Free Variables |
|
|
310 | (3) |
|
Exploiting Symmetry with Rigid Free Variables |
|
|
310 | (1) |
|
Other Uses of Free Variables |
|
|
311 | (1) |
|
Downsides of Free Variables |
|
|
312 | (1) |
|
Abstraction Models for Complexity Reduction |
|
|
313 | (7) |
|
|
313 | (2) |
|
|
315 | (1) |
|
|
316 | (3) |
|
|
319 | (1) |
|
|
320 | (3) |
|
Practical Tips from This Chapter: Summary |
|
|
321 | (2) |
|
|
323 | (2) |
|
Chapter 11 Your new FV-aware lifestyle |
|
|
325 | (18) |
|
|
326 | (3) |
|
|
326 | (1) |
|
|
327 | (1) |
|
|
327 | (1) |
|
Specialized FPV Using Apps |
|
|
328 | (1) |
|
Formal Equivalence Verification |
|
|
328 | (1) |
|
|
329 | (2) |
|
Engineer Preparation to Use FV |
|
|
330 | (1) |
|
|
331 | (1) |
|
Making Your Manager Happy |
|
|
331 | (7) |
|
|
332 | (3) |
|
|
335 | (1) |
|
|
335 | (3) |
|
|
338 | (2) |
|
|
340 | (1) |
|
|
341 | (2) |
Index |
|
343 | |