Muutke küpsiste eelistusi

E-raamat: Formal Verification: An Essential Toolkit for Modern VLSI Design

(Intel Corporation, Bengaluru, Karnataka, India), (Adjunct Professor, Department of Electrical and Computer Engineering, Portland State University, Portland, OR, USA), (Senior Product Engineering Architect, Cadence Design Systems)
  • Formaat: EPUB+DRM
  • Ilmumisaeg: 24-Jul-2015
  • Kirjastus: Morgan Kaufmann Publishers In
  • Keel: eng
  • ISBN-13: 9780128008157
  • Formaat - EPUB+DRM
  • Hind: 83,25 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
  • Formaat: EPUB+DRM
  • Ilmumisaeg: 24-Jul-2015
  • Kirjastus: Morgan Kaufmann Publishers In
  • Keel: eng
  • ISBN-13: 9780128008157

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

Formal Verification: An Essential Toolkit for Modern VLSI Design presents practical approaches for design and validation, with hands-on advice for working engineers integrating these techniques into their work.

Building on a basic knowledge of System Verilog, this book demystifies FV and presents the practical applications that are bringing it into mainstream design and validation processes at Intel and other companies. The text prepares readers to effectively introduce FV in their organization and deploy FV techniques to increase design and validation productivity.

  • Presents formal verification algorithms allowing users to gain full coverage without exhaustive simulation
  • Provides discussion of formal verification tools and how they differ from simulation tools
  • Teaches users how to glean insights into how models work to find initial bugs
  • Presents valuable information from an Intel insider who shares his hard-won knowledge and solutions to complex design problems

Arvustused

"...the authors thoroughly expressed their practical knowledge of this complex, and misunderstood topic, in an easy to read presentation...I strongly recommend this book to design and verification engineers who are contemplating, or are currently using formal verification..." --VerificationAcademy.com

Muu info

Intel insiders demystify formal verification to improve circuit design and increase productivity
Foreword for "Formal Verification: An Essential Toolkit for Modern VLSI Design" xiii
Acknowledgments xvii
Chapter 1 Formal verification: from dreams to reality
1(22)
What Is FV?
2(1)
Why This Book?
3(1)
A Motivating Anecdote
4(2)
FV: The Next Level of Depth
6(7)
Overall Advantages of FV
6(1)
General Usage Models for FV
7(1)
FV for Complete Coverage
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)
Complexity Theory
17(1)
The Good News
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)
Further Reading
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)
Comparing Specifications
26(3)
Cones of Influence
28(1)
Formalizing Operation Definitions
29(1)
Building Truth Tables Intelligently
29(1)
Adding Sequential Logic
30(1)
Boolean Algebra Notation
30(5)
Basic Boolean Algebra Laws
32(1)
Comparing Specifications
32(3)
BDDs
35(4)
Computing a BDD for a Circuit Design
37(1)
Model Checking
38(1)
Boolean Satisfiability
39(7)
Bounded Model Checking
40(1)
Solving the SAT Problem
41(2)
The Davis---Putnam SAT Algorithm
43(2)
The Davis Logemann Loveland (DLL) SAT Algorithm
45(1)
Chapter Summary
46(1)
Further Reading
47(2)
Chapter 3 Introduction to systemverilog assertions
49(38)
Basic Assertion Concepts
50(4)
A Simple Arbiter Example
50(1)
What Are Assertions?
51(1)
What Are Assumptions?
51(1)
What Are Cover Points?
52(1)
Clarification on Assertion Statements
52(1)
SVA Assertion Language Basics
53(1)
Immediate Assertions
54(12)
Writing Immediate Assertions
55(1)
Complications of Procedural Code and Motivation for Assert Final
56(2)
Location in Procedural Blocks
58(1)
Boolean Building Blocks
58(1)
Concurrent Assertion Basics and Clocking
59(1)
Sampling and Assertion Clocking
60(1)
Sampled Value Functions
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)
Writing the Properties
76(7)
Summary
83(3)
Practical Tips from This
Chapter
84(2)
Further Reading
86(1)
Chapter 4 Formal property verification
87(32)
What Is FPV?
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)
What Values Are Checked?
106(5)
Deciding Where and How to Run FPV
111(4)
Summary
115(2)
Practical Tips from This
Chapter
116(1)
Further Reading
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)
Design Exercise Goals
124(1)
Major Properties for Design Exercise
125(1)
Complexity Staging Plan
126(3)
Exit Criteria
129(1)
Putting It All Together
130(1)
Setting Up the Design Exercise FPV Environment
131(2)
Cover Points
131(1)
Assumptions
132(1)
Assertions
132(1)
Clocks and Resets
133(1)
Sanity-Checks
133(1)
Wiggling the Design
133(7)
The Wiggling Process
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)
Proving the Assertions
143(3)
Removing Simplifications and Exploring More Behaviors
146(4)
Facing Complexity Issues
149(1)
Summary
150(2)
Practical Tips from This
Chapter
151(1)
Further Reading
152(1)
Chapter 6 Effective FPV for verification
153(36)
Deciding on Your FPV Goals
154(2)
Bug Hunting FPV
154(1)
Full Proof FPV
155(1)
Staging Your FPV Efforts
156(1)
Example for This
Chapter: Simple ALU
157(1)
Understanding the Design
158(3)
Creating the FPV Verification Plan
161(22)
FPV Goals
162(1)
Major Properties for FPV
163(4)
Addressing Complexity
167(3)
Quality Checks and Exit Criteria
170(6)
Initial Cover Points
176(1)
Extended Wiggling
177(5)
Expanding the Cover Points
182(1)
Removing Simplifications and Exploring More Behaviors
183(2)
The Road to Full Proof FPV
184(1)
Summary
185(3)
Practical Tips from This
Chapter
186(2)
Further Reading
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)
Checking Completeness
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)
Post-Silicon Debug
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)
Summary
221(3)
Practical Tips from This
Chapter
221(3)
Further Reading
224(1)
Chapter 8 Formal equivalence verification
225(36)
Types of Equivalence to Check
226(5)
Combinational Equivalence
226(2)
Sequential Equivalence
228(1)
Transaction-Based Equivalence
229(2)
FEV Use Cases
231(7)
RTL to Netlist FEV
231(2)
RTL to RTL FEV
233(5)
Running FEV
238(10)
Choosing the Models
238(2)
Key Point Selection and Mapping
240(5)
Assumptions and Constraints
245(2)
Debugging Mismatches
247(1)
Additional FEV Challenges
248(8)
Latch/Flop Optimizations
248(1)
Conditional Equivalence
249(2)
Don't Care Space
251(1)
Complexity
252(4)
Summary
256(3)
Practical Tips from This
Chapter
256(3)
Further Reading
259(2)
Chapter 9 Formal verification's greatest bloopers: the danger of false positives
261(28)
Misuse of the SVA Language
263(6)
The Missing Semicolon
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)
Vacuity Issues
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)
Division of Labor
282(3)
Loss of Glue Logic
282(1)
Case-Splitting with Missing Cases
283(1)
Undoing Temporary Hacks
284(1)
Safe Division of Labor
284(1)
Summary
285(2)
Practical Tips from This
Chapter
286(1)
Further Reading
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)
Engine Tuning
295(2)
Blackboxing
297(1)
Parameters and Size Reduction
297(1)
Case-Splitting
298(2)
Property Simplification
300(2)
Cut Points
302(3)
Semiformal Verification
305(1)
Incremental FEV
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)
Counter Abstraction
313(2)
Sequence Abstraction
315(1)
Memory Abstraction
316(3)
Shadow Models
319(1)
Summary
320(3)
Practical Tips from This
Chapter: Summary
321(2)
Further Reading
323(2)
Chapter 11 Your new FV-aware lifestyle
325(18)
Uses of FV
326(3)
Design Exercise
326(1)
Bug Hunting FPV
327(1)
Full Proof FPV
327(1)
Specialized FPV Using Apps
328(1)
Formal Equivalence Verification
328(1)
Getting Started
329(2)
Engineer Preparation to Use FV
330(1)
Tool Preparation
331(1)
Making Your Manager Happy
331(7)
ROI Calculation
332(3)
Bug Complexity Ranking
335(1)
Progress Tracking
335(3)
What Do FVers Really Do?
338(2)
Summary
340(1)
Further Reading
341(2)
Index 343
Erik Seligman is currently a Senior Product Engineering Architect at Cadence Design Systems, where he helps to plan and support the Jasper Formal Verification tool suite. Previously he worked at Intel Corporation in Hillsboro, Oregon for over two decades, in a variety of positions involving software, design, simulation, and formal verification. In his spare time he hosts the Math Mutation” podcast, and has served as an elected director on the Hillsboro school board. Tom Schubert is on the Electrical and Computer Engineering faculty at Portland State University and directs a graduate track in Design Verification and Validation. Previously, he was at Intel Corporation for 17 years in Hillsboro, Oregon, where he managed Intel's largest pre-silicon validation formal verification team develop and apply FPV techniques on multiple generations of microprocessor designs. Tom received a PhD in Computer Science from the University of California, Davis. M V Achutha Kiran Kumar is an Intel Fellow in the Design Engineering group at intel and leads the companys Formal Verification Central Technology Office, one of the largest industrial Formal Verification teams in the world. He has over 19 years experience where he worked in various areas of the chip design cycle which includes RTL design, structural design, circuit design, simulation and various levels of validation including formal verification. He is the co-author of 'Formal Verification - An Essential toolkit for the Hardware Design'.