book

Hardware Design Verification: Simulation and Formal Method-Based Approaches

Name: Hardware Design Verification: Simulation and Formal Method-Based Approaches
Author: William K. Lam
ISBN: 9780131433472

by William K. Lam

March 2005

Intermediate to advanced

624 pages

14h 34m

English

Pearson

Read now

Unlock full access

Copyright
Dedication
Prentice Hall Modern Semiconductor Design Series
Preface
To the AudienceTo the InstructorOrganization of the BookErrata
Acknowledgments
About the Author
1. An Invitation to Design Verification
1.1. What Is Design Verification?1.2. The Basic Verification Principle1.3. Verification Methodology1.3.1. Simulation-Based Verification1.3.2. Formal Method-Based Verification1.4. Simulation-Based Verification versus Formal Verification1.5. Limitations of Formal Verification1.6. A Quick Overview of Verilog Scheduling and Execution Semantics1.6.1. Concurrent Processes1.6.2. Nondeterminism1.6.3. Scheduling Semantics1.7. Summary
2. Coding for Verification
2.1. Functional Correctness2.1.1. Syntactical ChecksOperands of unequal widthImplicitly embedded sequential stateOverlapping conditional casesConnection rulesPreferred design constructs2.1.2. Structural ChecksLoop structureBus operationFF and latch configurationSequential element reset2.2. Timing Correctness2.2.1. Race Problem2.2.2. Clock Gating2.2.3. Time Zero and Zero Time Glitches2.2.4. Domain-Crossing Glitches2.3. Simulation Performance2.3.1. Higher Level of Abstraction2.3.2. Simulator Recognizable Components2.3.3. Vector versus Scalar2.3.4. Minimization of the Interface to Other Simulation Systems2.3.5. Low-Level/Component-Level Optimization2.3.6. Code Profiling2.4. Portability and Maintainability2.4.1. Project Code Layout2.4.2. Centralized Resource2.4.3. RTL Design File Format2.5. “Synthesizability,” “Debugability,” and General Tool Compatibility2.5.1. Synthesizability2.5.2. Debugability2.6. Cycle-Based Simulation2.7. Hardware Simulation/Emulation2.8. Two-State and Four-State Simulation2.9. Design and Use of a Linter2.10. Summary2.11. Problems
3. Simulator Architectures and Operations
3.1. The Compilers3.2. The Simulators3.2.1. Event-Driven SimulatorsTiming wheel/event managerScheduling semanticsUpdate and evaluation eventsEvent propagationTime advancement and oscillation detectionEvent-driven scheduling algorithm3.2.2. Cycle-Based SimulatorsLevelingCombinational loop detectionClock domain analysisClock tree processingExecution orderCode generation and simulation control3.2.3. Hybrid SimulatorsCompiled event-driven simulatorLeveled event processing for zero-delay simulationCompiling combinational loops for cycle-based simulationDistributed event management3.2.4. Hardware Simulators and Emulators3.3. Simulator Taxonomy and Comparison3.3.1. Two-State and Four-State Simulators3.3.2. Zero- versus Unit-Delay Simulators3.3.3. Event-Driven versus Cycle-Based Simulators3.3.4. Interpreted versus Compiled Simulators3.3.5. Hardware Simulators3.4. Simulator Operations and Applications3.4.1. The Basic Simulation File Structure3.4.2. Performance and Debugging3.4.3. Timing Verification3.4.4. Design Profiling3.4.5. Two-State and Four-State3.4.6. Cosimulation with Encapsulated Models3.5. Incremental Compilation3.6. Simulator Console3.7. Summary3.8. Problems
4. Test Bench Organization and Design
4.1. Anatomy of a Test Bench and a Test Environment4.2. Initialization Mechanism4.2.1. RTL Initialization4.2.2. PLI Initialization4.2.3. Initialization at Time Zero4.3. Clock Generation and Synchronization4.3.1. Explicit and Toggle Methods4.3.2. Absolute Transition Delay4.3.3. Time Zero Clock Transition4.3.4. Time Unit and Resolution4.3.5. Clock Multiplier and Divider4.3.6. Clock Independence and Jitter4.3.7. Clock Synchronization and Delta Delay4.3.8. Clock Generator Organization4.4. Stimulus Generation4.4.1. Asynchronous Stimuli Application4.4.2. Instruction Code or Programmed Stimuli4.5. Response Assessment4.5.1. Design State Dumping4.5.2. Golden ResponseSelf-checking codesCosimulation with reference model4.5.3. Checking Temporal Specifications4.6. Verification Utility4.6.1. Error Injector4.6.2. Error and Warning Alert Mechanism4.6.3. Memory Loading and Dumping Mechanism4.6.4. Sparse Memory and Content Addressable Memory (CAM)4.6.5. Assertion Routines4.7. Test Bench-to-Design Interface4.8. Common Practical Techniques and Methodologies4.8.1. Verification Environment Configuration4.8.2. Bus Functional Model4.9. Summary4.10. Problems
5. Test Scenarios, Assertions, and Coverage
5.1. Hierarchical Verification5.1.1. System Level5.1.2. Unit Level5.1.3. Module Level5.2. Test Plan5.2.1. Extract Functionality from Architectural Specifications5.2.2. Prioritize Functionality5.2.3. Create Test Cases5.2.4. Track Progress5.3. Pseudorandom Test Generator5.3.1. User Interface5.3.2. Register and Memory Allocation5.3.3. Program Construction5.3.4. Self-checking Mechanism5.4. Assertions5.4.1. Defining What to Assert5.4.2. Assertion Components5.4.3. Writing AssertionsSignal rangeUnknown valueParitySignal membershipOne-hot/cold signalsSequential assertionsSignal change patternTime windowInterval constraintUnclocked timing assertionsContainer assertions5.4.4. Built-in Commercial Assertions5.5. SystemVerilog Assertions5.5.1. Immediate Assertions5.5.2. Concurrent AssertionsSequence constructorsSequence connectivesOperator ANDOperator intersectOperator OROperator first_matchOperator implicationOperator throughoutOperator withinOperator containerOperator endedSystem functionsMultiple clocks5.6. Verification Coverage5.6.1. Code CoverageStatement coverageBlock coveragePath coverageExpression coverageState coverageTransition coverageSequence coverageToggle coverageCode instrumentationPerformance and methodology5.6.2. Parameter Coverage5.6.3. Functional CoverageFunctional verification object5.6.4. Item Coverage and Cross-Coverage5.7. Summary5.8. Problems

6. Debugging Process and Verification Cycle
6.1. Failure Capture, Scope Reduction, and Bug Tracking6.1.1. Failure Capture6.1.2. Scope ReductionCircuit reductionTest case reductionCheck pointing6.1.3. Error Tracking System6.2. Simulation Data Dumping6.2.1. Spatial Neighborhood6.2.2. Temporal Window6.3. Isolation of Underlying Causes6.3.1. Reference Value, Propagation, and Bifurcation6.3.2. Forward and Backward Debugging6.3.3. Tracing Diagram6.3.4. Time Framing6.3.5. Load, Driver, and Cone Tracing6.3.6. Memory and Array Tracing6.3.7. Zero Time Loop Constructs6.3.8. The Four Basic Views of Design6.3.9. Typical Debugger Functionality6.4. Design Update and Maintenance: Revision Control6.5. Regression, Release Mechanism, and Tape-out Criteria6.6. Summary6.7. Problems
7. Formal Verification Preliminaries
7.1. Sets and Operations7.2. Relation, Partition, Partially Ordered Set, and Lattice7.3. Boolean Functions and Representations7.3.1. Symmetric Boolean Functions7.3.2. Incompletely Specified Boolean Functions7.3.3. Characteristic Functions7.4. Boolean Functional Operators7.5. Finite-State Automata and Languages7.5.1. Product Automata and Machines7.5.2. State Equivalence and Machine Minimization7.5.3. Finite-State Machine Equivalence7.5.4. Graph Algorithms7.5.5. Depth-First Search7.5.6. Breadth-First Search7.6. Summary7.7. Problems
8. Decision Diagrams, Equivalence Checking, and Symbolic Simulation
8.1. Binary Decision Diagrams8.1.1. Operations on BDDsConstructionReductionRestrictionBoolean operations8.1.2. Variable OrderingDynamic Variable OrderingFunctions and BDD Sizes8.2. Decision Diagram Variants8.2.1. Shared BDDs (SBDDs)8.2.2. Edge-Attributed BDDs8.2.3. Zero-Suppressed BDDs (ZBDDs)8.2.4. Ordered Functional Decision Diagrams (OFDDs)8.2.5. Pseudo Boolean Functions and Decision Diagrams8.2.6. Binary Moment Diagram (BMD)8.3. Decision Diagram-Based Equivalence Checking8.3.1. Node Mapping and Constraining8.4. Boolean Satisfiability8.4.1. Resolvent Algorithm8.4.2. Search-Based Algorithm8.4.3. Implication Graph and Learning8.5. Symbolic Simulation8.5.1. Symbolic Verification8.5.2. Input Constraining8.5.3. Symbolic Simulation Using Characteristic Functions8.5.4. Parameterization8.6. Summary8.7. Problems
9. Model Checking and Symbolic Computation
9.1. Properties, Specifications, and Logic9.1.1. Sequential Specification Using Automata9.1.2. Temporal Structure and Computation Tree9.1.3. Propositional Temporal Logic: LTL, CTL*, and CTL9.1.4. Fairness Constraint9.1.5. Relative Expressiveness of CTL*, CTL, and LTL9.1.6. SystemVerilog Assertion Language9.2. Property Checking9.2.1. Property Specification Using an Automaton9.2.2. Language Containment9.2.3. Checking CTL Formulas9.2.4. Checking with Fairness Constraints9.3. Symbolic Computation and Model Checking9.3.1. Symbolic Finite-State Machine Representation and State Traversal9.3.2. Counterexample Generation9.3.3. Equivalence Checking9.3.4. Language Containment and Fairness Constraints9.4. Symbolic CTL Model Checking9.4.1. Fix-point Computation9.4.2. CTL Checking with Fairness Constraints9.5. Computational Improvements9.5.1. Early Quantification9.5.2. Generalized Cofactor9.6. Using Model-Checking Tools9.7. Summary9.8. Problems
Bibliography

Content preview from Hardware Design Verification: Simulation and Formal Method-Based Approaches

Bibliography

[biblio01_001] 1. M., Abramovici, M. A. Breuer, and A. D. Friedman. Digital Systems Testing and Testable Design. New York: IEEE Computer Society Press, <year>1994</year>.

[biblio01_002] 2. D. Abts, “Integrating Code Coverage Analysis into a Large Scale ASIC Design Verification Flow.” In Proceedings of the International HDL Conference, 1999.

[biblio01_003] 3. S. B. Akers, “Binary Decision Diagrams.” IEEE Transactions on Computers 37, no. 6 (June 1978): 40–45.

[biblio01_004] 4. F. Aloul and K. Sakallah, “Satometer: How Much Have We Searched?” In Proceedings of the 39th Design Automation Conference, 2002.

[biblio01_005] 5. F., Aloul, A. Ramani, I. Markov, and K. Sakallah. “PBS: A Backtrack Search Pseudo-Boolean Solver.” In International ...

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.

Read now

Unlock full access

More than 5,000 organizations count on O’Reilly

O’Reilly covers everything we've got, with content to help us build a world-class technology community, upgrade the capabilities and competencies of our teams, and improve overall team performance as well as their engagement.

Julian F.

Head of Cybersecurity

I wanted to learn C and C++, but it didn't click for me until I picked up an O'Reilly book. When I went on the O’Reilly platform, I was astonished to find all the books there, plus live events and sandboxes so you could play around with the technology.

Addison B.

Field Engineer

I’ve been on the O’Reilly platform for more than eight years. I use a couple of learning platforms, but I'm on O'Reilly more than anybody else. When you're there, you start learning. I'm never disappointed.

Amir M.

Data Platform Tech Lead

I'm always learning. So when I got on to O'Reilly, I was like a kid in a candy store. There are playlists. There are answers. There's on-demand training. It's worth its weight in gold, in terms of what it allows me to do.

Mark W.

Embedded Software Engineer

Process Control: Modeling, Design, and Simulation

Publisher Resources

ISBN: 0131433474Purchase book

Cloud Computing

Data Engineering

Data Science

AI & ML

Programming Languages

Software Architecture

IT/Ops

Security

Design

Business

Soft Skills

Hardware Design Verification: Simulation and Formal Method-Based Approaches

by William K. Lam

Bibliography

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.