Comprehensive functional verification the complete industry cycle /
Bruce Wile, John C. Goss, Wolfgang Roesner.
- Amsterdam ; Boston : Elsevier/Morgan Kaufmann, c2005.
- xiii, 676 p. : ill. ; 24 cm.
Includes bibliographical references (p. 657-662) and index.
Introduction to Verification -- Verification in the Chip Design Process Introduction to Functional Verification The Verification Challenge The Challenge of State Space Explosion The Challenge of Detecting Incorrect Behavior Mission and Goals of Verification Verification Engineer "Musts" Cost of Verification Engineering Costs and the Need for an Independent Verification Team Design Automation Tools Time Areas of Verification Beyond the Scope of this Book The Verification Cycle: A Structured Process Functional Specification Create Verification Plan Develop Environment Debug HDL and Environment Regression Fabricate Hardware Debug Fabricated Hardware (Systems Test) Escape Analysis Common Verification Cycle Breakdowns Verification Flow Verification Hierarchy Levels of Verification What Level to Choose? Strategy of Verification Driving Principles Checking Strategies Checking the Black Box The General Simulation Environment Verification Methodology Evolution Fundamentals of Simulation Based Verification Basic Verification Environment: A Test Bench Stimulus Component Monitor Checker Scoreboard Design Under Verification Observation Points: Black-Box, White-Box and Grey-Box Verification Black Box White Box Grey Box Assertion Based Verification-An Overview The Importance of Assertions Assertions Express Design Intent Classification of Assertions Test Benches and Testing Strategies Deterministic Test Benches Self-Checking Test Benches The Verification Plan The Functional Specification The Evolution of the Verification Plan Contents of the Verification Plan Description of Verification Levels Required Tools Risks and Dependencies Functions to be Verified Specific Tests and Methods: Environment Coverage Requirements Test Case Scenarios: Matrix Resource Requirements Schedule Details Verification Example: Calc1 Design Description Creating the Verification Plan for Calc1 Deterministic Verification of Calc1 Simulation Based Verification -- HDLs and Simulation Engines Hardware Description Languages HDL Modeling Levels Verification Aspects of HDLs Simulation Engines: Introduction Speed versus Accuracy Making the Right Methodology Choices Event-Driven Simulation Hierarchical Model Network Model Evaluation Over Time Event-Driven Control of Model Evaluation Implementation Sketch of an Event-Driven Simulation Engine Improving Simulation Throughput Cycle-Based Simulation Synchronous Design The Cycle-Based Simulation Algorithm Extensions to Basic Cycle-Based Simulation Engines Waveform Viewers Creating Environments Test Bench Writing Tools HDL Languages as Test Bench Tool C/C++ Libraries High-Level Verification Languages Other Test Bench Tools Verification Coverage Functional Verification Test Coverage versus Manufacturing Test Coverage Structural Coverage Functional Coverage Coverage Bulk Data Collection and Management The Right Coverage Analysis Strategy Strategies for Simulation-Based Stimulus Generation Calc2 Overview Calc2 Verification Plan Calc2 and the Strategies for Stimulus Generation Strategies for Stimulus Generation Types of Stimulus Generation General Algorithms for Stimulus Components Applying the Four Types of Stimulus Generation to Calc2 Seeding Random Test Cases Constraint Solving in Random Environments Coverage Techniques in Random Environments Making Rare Events Occur Stimulus Generation of Deadlocks and Livelocks Strategies for Results Checking in Simulation-Based Verification Types of Result Checking On-the-Fly Checking versus End-of-Test Case Checking Pregenerated Test Cases versus On-the-Fly Generated Test Cases Applying the Checking Strategies to Calc2 Debug Debug Process How Different Types of Test Benches Affect Debug Pervasive Function Verification System Reset and Bring-Up Reset Line Initialization Scan Initialization Testability and Built-In Self-Test Error and Degraded Mode Handling Verifying Error Detection Verifying Self-Healing Hardware Verifying Hardware Debug Assists Verifying Scan Ring Dumps Low Power Mode Verification Power Savings Through Disabling Functional Units Power Savings Through Cycle Time Degradation Re-Use Strategies and System Simulation Re-Use Strategies Guidelines for Re-Use Horizontal Re-Use Vertical Re-Use Applying Re-Use to Calc2 Assertion Re-Use System Simulation System Test Bench Connectivity and Interaction of Units Verification Challenges in a Re-Usable IP World Beyond General-Purpose Logic Simulation Acceleration Emulation Hardware/Software Co-verification Co-simulation Formal Verification -- Introduction to Formal Verification Design Correctness and Specifications Computational Complexity The Myth of Linear Scaling of Simulation Mathematical Proof Methods in Formal Verification Formal Boolean Equivalence Checking The Role of Equivalence Checking in the VLSI Design Flow Main Elements of an Equivalence Checker Tool Sequential and Combinational Boolean Equivalence Checking Core Algorithms for Combinational Equivalence Checking Blueprint of a Modern Equivalence Checking Tool Functional Formal Verification-Property Checking Property Checking vs. Part I 1 5 -- 1.1 5 -- 1.2 8 -- 1.2.1 9 -- 1.2.2 12 -- 1.3 14 -- 1.3.1 18 -- 1.4 20 -- 1.4.1 20 -- 1.4.2 21 -- 1.4.3 22 -- 1.5 23 -- 1.6 24 -- 1.6.1 25 -- 1.6.2 26 -- 1.6.3 27 -- 1.6.4 27 -- 1.6.5 28 -- 1.6.6 28 -- 1.6.7 29 -- 1.6.8 29 -- 1.6.9 30 -- 2 35 -- 2.1 35 -- 2.1.1 36 -- 2.1.2 41 -- 2.2 45 -- 2.2.1 45 -- 2.2.2 50 -- 2.2.3 55 -- 2.2.5 61 -- 2.2.6 62 -- 3 73 -- 3.1 73 -- 3.1.1 74 -- 3.1.2 80 -- 3.1.3 82 -- 3.1.4 83 -- 3.1.5 85 -- 3.2 86 -- 3.2.1 86 -- 3.2.2 87 -- 3.2.3 88 -- 3.3 89 -- 3.3.1 90 -- 3.3.2 92 -- 3.3.3 94 -- 3.4 95 -- 3.4.1 95 -- 3.4.2 97 -- 4 103 -- 4.1 103 -- 4.2 104 -- 4.3 106 -- 4.3.1 106 -- 4.3.2 107 -- 4.3.3 108 -- 4.3.4 109 -- 4.3.5 111 -- 4.3.6 115 -- 4.3.7 116 -- 4.3.8 117 -- 4.3.9 118 -- 4.4 121 -- 4.4.1 121 -- 4.4.2 125 -- 4.4.3 131 -- Part II 5 141 -- 5.1 143 -- 5.1.1 143 -- 5.1.2 153 -- 5.2 159 -- 5.2.1 160 -- 5.2.2 162 -- 5.3 162 -- 5.3.1 163 -- 5.3.2 165 -- 5.3.3 167 -- 5.3.4 172 -- 5.4 178 -- 5.5 182 -- 5.5.1 183 -- 5.5.2 184 -- 5.5.3 188 -- 5.6 191 -- 6 199 -- 6.1 200 -- 6.1.1 201 -- 6.1.2 207 -- 6.1.3 230 -- 6.1.4 241 -- 6.2 243 -- 6.2.2 246 -- 6.2.3 247 -- 6.2.4 251 -- 6.2.5 254 -- 6.2.6 255 -- 7 259 -- 7.1 260 -- 7.1.1 263 -- 7.1.2 269 -- 7.2 270 -- 7.2.1 270 -- 7.2.2 275 -- 7.2.3 277 -- 7.2.4 294 -- 7.2.5 297 -- 7.2.6 301 -- 7.2.7 303 -- 7.2.8 306 -- 8 313 -- 8.1 313 -- 8.1.1 314 -- 8.1.2 321 -- 8.1.3 322 -- 8.2 334 -- 8.2.1 336 -- 8.2.2 349 -- 9 355 -- 9.1 356 -- 9.1.1 357 -- 9.1.2 361 -- 9.1.3 363 -- 9.2 368 -- 9.2.1 368 -- 9.2.2 372 -- 9.3 380 -- 9.3.1 381 -- 384 -- 9.4.1 385 -- 9.4.2 387 -- 10 391 -- 10.1 392 -- 10.1.1 395 -- 10.1.2 403 -- 10.1.3 404 -- 10.1.4 405 -- 10.1.5 410 -- 10.2 412 -- 10.2.1 412 -- 10.2.2 414 -- 10.2.3 418 -- 10.3 420 -- 10.3.1 421 -- 10.3.2 427 -- 10.3.3 428 -- 10.3.4 430 -- Part III 11 439 -- 11.1.1 441 -- 11.1.2 443 -- 11.1.3 445 -- 11.1.4 446 -- 11.2 448 -- 11.2.1 449 -- 11.2.2 450 -- 11.2.3 451 -- 11.2.4 454 -- 11.2.5 465 -- 11.3 467 -- 11.3.1 Sequential Equivalence Checking The Myth of Complete Verification with FV Properties for an Example Design DUV Drivers for Formal Verification State Space Traversal and Temporal Logic Functional Formal Verification Tool Flow Using Formal Verification Property Specification Using an HDL Library The Open Verification Library (OVL) Using OVL to Specify Properties The Property Specification Language PSL The Boolean Layer of PSL The Temporal Layer of PSL The Verification Layer of PSL The Modeling Layer of PSL Using PSL to Specify Properties Advanced PSL Topics and Caveats Property Checking Using Formal Verification Property Re-Use between Simulation and FV Model Compliation Formal Functional Verification Algorithms Solutions to Address the Problem of State Space Explosion Semi-Formal Verification EDA Vendors Supplying Formal and Semi-Formal Verification Tools Comprehensive Verification -- Completing the Verification Cycle Regression Regression in the Verification Flow Regression Quality Regression Efficiency Problem Tracking Tape-Out Readiness Metrics Completion Criteria Escape Analysis Individual Bug Analysis Escape Examples Escape Analysis Trends Advanced Verification Techniques Save Verification Cycles-Bootstrapping the Verification Process Separating POR and Mainline Verification Bootstrapping the DUV into High-Potential States Manipulating the DUV Specification Provoking States of Resource Conflict High-Level Modeling-Concepts Applications of the High-Level Model High-Level Modeling Styles Coverage-Directed Generation The Line Delete Escape The Background The Verification Environments The Escape Branch History Table 468 -- 11.3.2 470 -- 11.3.3 471 -- 11.3.4 476 -- 11.3.5 479 -- 11.3.6 483 -- 12 487 -- 12.1 488 -- 12.1.1 489 -- 12.1.2 495 -- 12.2 499 -- 12.2.2 501 -- 12.2.3 504 -- 12.2.4 508 -- 12.2.5 511 -- 12.2.6 512 -- 12.2.7 514 -- 12.3 521 -- 12.3.1 521 -- 12.3.2 522 -- 12.3.3 523 -- 12.3.4 527 -- 12.3.5 530 -- 12.3.6 532 -- Part IV 13 539 -- 13.1 540 -- 13.1.1 540 -- 13.1.2 542 -- 13.1.3 543 -- 13.2 548 -- 13.3 552 -- 13.3.1 552 -- 13.3.2 557 -- 13.4 559 -- 13.4.1 561 -- 13.4.2 569 -- 13.4.3 572 -- 14 579 -- 14.1 580 -- 14.1.1 580 -- 14.1.2 583 -- 14.1.3 585 -- 14.2 586 -- 14.2.1 587 -- 14.2.2 590 -- 14.3 595 -- 15.1 603 -- 15.1.1 603 -- 15.1.2 605 -- 15.1.3 607 -- 15.2 608
A key strength of this book is that it describes the entire verification cycle and details each stage. The organization of the book follows the cycle, demonstrating how functional verification engages all aspects of the overall design effort and how individual cycle stages relate to the larger design process. Throughout the text, the authors leverage their 35 plus years experience in functional verification, providing examples and case studies, and focusing on the skills, methods, and tools needed to complete each verification task. Additionally, the major vendors (Mentor Graphics, Cadence Design Systems, Verisity, and Synopsys) have implemented key examples from the text and made these available on line, so that the reader can test out the methods described in the text.