Hardware Design Verification: Simulation and Formal Method-Based Approaches

Hardware Design Verification: Simulation and Formal Method-Based Approaches

by William K. Lam
Released March 2005
Publisher(s): Pearson
ISBN: 9780131433472

Read it now on the O’Reilly learning platform with a 10-day free trial.

O’Reilly members get unlimited access to books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial

Book description

The Practical, Start-to-Finish Guide to Modern Digital Design Verification

As digital logic designs grow larger and more complex, functional verification has become the number one bottleneck in the design process. Reducing verification time is crucial to project success, yet many practicing engineers have had little formal training in verification, and little exposure to the newest solutions. Hardware Design Verification systematically presents today's most valuable simulation-based and formal verification techniques, helping test and design engineers choose the best approach for each project, quickly gain confidence in their designs, and move into fabrication far more rapidly. College students will find that coverage of verification principles and common industry practices will help them prepare for jobs as future verification engineers.

Author William K. Lam, one of the world's leading experts in design verification, is a recent winner of the Chairman's Award for Innovation, Sun Microsystems' most prestigious technical achievement award. Drawing on his wide-ranging experience, he introduces the foundational principles of verification, presents traditional techniques that have survived the test of time, and introduces emerging techniques for today's most challenging designs. Throughout, Lam emphasizes practical examples rather than mathematical proofs; wherever advanced math is essential, he explains it clearly and accessibly.

Coverage includes

  • Simulation-based versus formal verification: advantages, disadvantages, and tradeoffs

  • Coding for verification: functional and timing correctness, syntactical and structure checks, simulation performance, and more

  • Simulator architectures and operations, including event-driven, cycle-based, hybrid, and hardware-based simulators

  • Testbench organization, design, and tools: creating a fast, efficient test environment

  • Test scenarios and assertion: planning, test cases, test generators, commercial and Verilog assertions, and more

  • Ensuring complete coverage, including code, parameters, functions, items, and cross-coverage

  • The verification cycle: failure capture, scope reduction, bug tracking, simulation data dumping, isolation of underlying causes, revision control, regression, release mechanisms, and tape-out criteria

  • An accessible introduction to the mathematics and algorithms of formal verification, from Boolean functions to state-machine equivalence and graph algorithms

  • Decision diagrams, equivalence checking, and symbolic simulation

  • Model checking and symbolic computation

    • Simply put, Hardware Design Verification will help you improve and accelerate your entire verification process--from planning through tape-out--so you can get to market faster with higher quality designs.

    Table of contents

    1. Copyright
      1. Dedication
    2. Prentice Hall Modern Semiconductor Design Series
    3. Preface
      1. To the Audience
      2. To the Instructor
      3. Organization of the Book
      4. Errata
    4. Acknowledgments
    5. About the Author
    6. 1. An Invitation to Design Verification
      1. 1.1. What Is Design Verification?
      2. 1.2. The Basic Verification Principle
      3. 1.3. Verification Methodology
        1. 1.3.1. Simulation-Based Verification
        2. 1.3.2. Formal Method-Based Verification
      4. 1.4. Simulation-Based Verification versus Formal Verification
      5. 1.5. Limitations of Formal Verification
      6. 1.6. A Quick Overview of Verilog Scheduling and Execution Semantics
        1. 1.6.1. Concurrent Processes
        2. 1.6.2. Nondeterminism
        3. 1.6.3. Scheduling Semantics
      7. 1.7. Summary
    7. 2. Coding for Verification
      1. 2.1. Functional Correctness
        1. 2.1.1. Syntactical Checks
          1. Operands of unequal width
          2. Implicitly embedded sequential state
          3. Overlapping conditional cases
          4. Connection rules
          5. Preferred design constructs
        2. 2.1.2. Structural Checks
          1. Loop structure
          2. Bus operation
          3. FF and latch configuration
          4. Sequential element reset
      2. 2.2. Timing Correctness
        1. 2.2.1. Race Problem
        2. 2.2.2. Clock Gating
        3. 2.2.3. Time Zero and Zero Time Glitches
        4. 2.2.4. Domain-Crossing Glitches
      3. 2.3. Simulation Performance
        1. 2.3.1. Higher Level of Abstraction
        2. 2.3.2. Simulator Recognizable Components
        3. 2.3.3. Vector versus Scalar
        4. 2.3.4. Minimization of the Interface to Other Simulation Systems
        5. 2.3.5. Low-Level/Component-Level Optimization
        6. 2.3.6. Code Profiling
      4. 2.4. Portability and Maintainability
        1. 2.4.1. Project Code Layout
        2. 2.4.2. Centralized Resource
        3. 2.4.3. RTL Design File Format
      5. 2.5. “Synthesizability,” “Debugability,” and General Tool Compatibility
        1. 2.5.1. Synthesizability
        2. 2.5.2. Debugability
      6. 2.6. Cycle-Based Simulation
      7. 2.7. Hardware Simulation/Emulation
      8. 2.8. Two-State and Four-State Simulation
      9. 2.9. Design and Use of a Linter
      10. 2.10. Summary
      11. 2.11. Problems
    8. 3. Simulator Architectures and Operations
      1. 3.1. The Compilers
      2. 3.2. The Simulators
        1. 3.2.1. Event-Driven Simulators
          1. Timing wheel/event manager
          2. Scheduling semantics
          3. Update and evaluation events
          4. Event propagation
          5. Time advancement and oscillation detection
          6. Event-driven scheduling algorithm
        2. 3.2.2. Cycle-Based Simulators
          1. Leveling
          2. Combinational loop detection
          3. Clock domain analysis
          4. Clock tree processing
          5. Execution order
          6. Code generation and simulation control
        3. 3.2.3. Hybrid Simulators
          1. Compiled event-driven simulator
          2. Leveled event processing for zero-delay simulation
          3. Compiling combinational loops for cycle-based simulation
          4. Distributed event management
        4. 3.2.4. Hardware Simulators and Emulators
      3. 3.3. Simulator Taxonomy and Comparison
        1. 3.3.1. Two-State and Four-State Simulators
        2. 3.3.2. Zero- versus Unit-Delay Simulators
        3. 3.3.3. Event-Driven versus Cycle-Based Simulators
        4. 3.3.4. Interpreted versus Compiled Simulators
        5. 3.3.5. Hardware Simulators
      4. 3.4. Simulator Operations and Applications
        1. 3.4.1. The Basic Simulation File Structure
        2. 3.4.2. Performance and Debugging
        3. 3.4.3. Timing Verification
        4. 3.4.4. Design Profiling
        5. 3.4.5. Two-State and Four-State
        6. 3.4.6. Cosimulation with Encapsulated Models
      5. 3.5. Incremental Compilation
      6. 3.6. Simulator Console
      7. 3.7. Summary
      8. 3.8. Problems
    9. 4. Test Bench Organization and Design
      1. 4.1. Anatomy of a Test Bench and a Test Environment
      2. 4.2. Initialization Mechanism
        1. 4.2.1. RTL Initialization
        2. 4.2.2. PLI Initialization
        3. 4.2.3. Initialization at Time Zero
      3. 4.3. Clock Generation and Synchronization
        1. 4.3.1. Explicit and Toggle Methods
        2. 4.3.2. Absolute Transition Delay
        3. 4.3.3. Time Zero Clock Transition
        4. 4.3.4. Time Unit and Resolution
        5. 4.3.5. Clock Multiplier and Divider
        6. 4.3.6. Clock Independence and Jitter
        7. 4.3.7. Clock Synchronization and Delta Delay
        8. 4.3.8. Clock Generator Organization
      4. 4.4. Stimulus Generation
        1. 4.4.1. Asynchronous Stimuli Application
        2. 4.4.2. Instruction Code or Programmed Stimuli
      5. 4.5. Response Assessment
        1. 4.5.1. Design State Dumping
        2. 4.5.2. Golden Response
          1. Self-checking codes
          2. Cosimulation with reference model
        3. 4.5.3. Checking Temporal Specifications
      6. 4.6. Verification Utility
        1. 4.6.1. Error Injector
        2. 4.6.2. Error and Warning Alert Mechanism
        3. 4.6.3. Memory Loading and Dumping Mechanism
        4. 4.6.4. Sparse Memory and Content Addressable Memory (CAM)
        5. 4.6.5. Assertion Routines
      7. 4.7. Test Bench-to-Design Interface
      8. 4.8. Common Practical Techniques and Methodologies
        1. 4.8.1. Verification Environment Configuration
        2. 4.8.2. Bus Functional Model
      9. 4.9. Summary
      10. 4.10. Problems
    10. 5. Test Scenarios, Assertions, and Coverage
      1. 5.1. Hierarchical Verification
        1. 5.1.1. System Level
        2. 5.1.2. Unit Level
        3. 5.1.3. Module Level
      2. 5.2. Test Plan
        1. 5.2.1. Extract Functionality from Architectural Specifications
        2. 5.2.2. Prioritize Functionality
        3. 5.2.3. Create Test Cases
        4. 5.2.4. Track Progress
      3. 5.3. Pseudorandom Test Generator
        1. 5.3.1. User Interface
        2. 5.3.2. Register and Memory Allocation
        3. 5.3.3. Program Construction
        4. 5.3.4. Self-checking Mechanism
      4. 5.4. Assertions
        1. 5.4.1. Defining What to Assert
        2. 5.4.2. Assertion Components
        3. 5.4.3. Writing Assertions
          1. Signal range
          2. Unknown value
          3. Parity
          4. Signal membership
          5. One-hot/cold signals
          6. Sequential assertions
          7. Signal change pattern
          8. Time window
          9. Interval constraint
          10. Unclocked timing assertions
          11. Container assertions
        4. 5.4.4. Built-in Commercial Assertions
      5. 5.5. SystemVerilog Assertions
        1. 5.5.1. Immediate Assertions
        2. 5.5.2. Concurrent Assertions
          1. Sequence constructors
          2. Sequence connectives
          3. Operator AND
          4. Operator intersect
          5. Operator OR
          6. Operator first_match
          7. Operator implication
          8. Operator throughout
          9. Operator within
          10. Operator container
          11. Operator ended
          12. System functions
          13. Multiple clocks
      6. 5.6. Verification Coverage
        1. 5.6.1. Code Coverage
          1. Statement coverage
          2. Block coverage
          3. Path coverage
          4. Expression coverage
          5. State coverage
          6. Transition coverage
          7. Sequence coverage
          8. Toggle coverage
          9. Code instrumentation
          10. Performance and methodology
        2. 5.6.2. Parameter Coverage
        3. 5.6.3. Functional Coverage
          1. Functional verification object
        4. 5.6.4. Item Coverage and Cross-Coverage
      7. 5.7. Summary
      8. 5.8. Problems
    11. 6. Debugging Process and Verification Cycle
      1. 6.1. Failure Capture, Scope Reduction, and Bug Tracking
        1. 6.1.1. Failure Capture
        2. 6.1.2. Scope Reduction
          1. Circuit reduction
          2. Test case reduction
          3. Check pointing
        3. 6.1.3. Error Tracking System
      2. 6.2. Simulation Data Dumping
        1. 6.2.1. Spatial Neighborhood
        2. 6.2.2. Temporal Window
      3. 6.3. Isolation of Underlying Causes
        1. 6.3.1. Reference Value, Propagation, and Bifurcation
        2. 6.3.2. Forward and Backward Debugging
        3. 6.3.3. Tracing Diagram
        4. 6.3.4. Time Framing
        5. 6.3.5. Load, Driver, and Cone Tracing
        6. 6.3.6. Memory and Array Tracing
        7. 6.3.7. Zero Time Loop Constructs
        8. 6.3.8. The Four Basic Views of Design
        9. 6.3.9. Typical Debugger Functionality
      4. 6.4. Design Update and Maintenance: Revision Control
      5. 6.5. Regression, Release Mechanism, and Tape-out Criteria
      6. 6.6. Summary
      7. 6.7. Problems
    12. 7. Formal Verification Preliminaries
      1. 7.1. Sets and Operations
      2. 7.2. Relation, Partition, Partially Ordered Set, and Lattice
      3. 7.3. Boolean Functions and Representations
        1. 7.3.1. Symmetric Boolean Functions
        2. 7.3.2. Incompletely Specified Boolean Functions
        3. 7.3.3. Characteristic Functions
      4. 7.4. Boolean Functional Operators
      5. 7.5. Finite-State Automata and Languages
        1. 7.5.1. Product Automata and Machines
        2. 7.5.2. State Equivalence and Machine Minimization
        3. 7.5.3. Finite-State Machine Equivalence
        4. 7.5.4. Graph Algorithms
        5. 7.5.5. Depth-First Search
        6. 7.5.6. Breadth-First Search
      6. 7.6. Summary
      7. 7.7. Problems
    13. 8. Decision Diagrams, Equivalence Checking, and Symbolic Simulation
      1. 8.1. Binary Decision Diagrams
        1. 8.1.1. Operations on BDDs
          1. Construction
          2. Reduction
          3. Restriction
          4. Boolean operations
        2. 8.1.2. Variable Ordering
          1. Dynamic Variable Ordering
          2. Functions and BDD Sizes
      2. 8.2. Decision Diagram Variants
        1. 8.2.1. Shared BDDs (SBDDs)
        2. 8.2.2. Edge-Attributed BDDs
        3. 8.2.3. Zero-Suppressed BDDs (ZBDDs)
        4. 8.2.4. Ordered Functional Decision Diagrams (OFDDs)
        5. 8.2.5. Pseudo Boolean Functions and Decision Diagrams
        6. 8.2.6. Binary Moment Diagram (BMD)
      3. 8.3. Decision Diagram-Based Equivalence Checking
        1. 8.3.1. Node Mapping and Constraining
      4. 8.4. Boolean Satisfiability
        1. 8.4.1. Resolvent Algorithm
        2. 8.4.2. Search-Based Algorithm
        3. 8.4.3. Implication Graph and Learning
      5. 8.5. Symbolic Simulation
        1. 8.5.1. Symbolic Verification
        2. 8.5.2. Input Constraining
        3. 8.5.3. Symbolic Simulation Using Characteristic Functions
        4. 8.5.4. Parameterization
      6. 8.6. Summary
      7. 8.7. Problems
    14. 9. Model Checking and Symbolic Computation
      1. 9.1. Properties, Specifications, and Logic
        1. 9.1.1. Sequential Specification Using Automata
        2. 9.1.2. Temporal Structure and Computation Tree
        3. 9.1.3. Propositional Temporal Logic: LTL, CTL*, and CTL
        4. 9.1.4. Fairness Constraint
        5. 9.1.5. Relative Expressiveness of CTL*, CTL, and LTL
        6. 9.1.6. SystemVerilog Assertion Language
      2. 9.2. Property Checking
        1. 9.2.1. Property Specification Using an Automaton
        2. 9.2.2. Language Containment
        3. 9.2.3. Checking CTL Formulas
        4. 9.2.4. Checking with Fairness Constraints
      3. 9.3. Symbolic Computation and Model Checking
        1. 9.3.1. Symbolic Finite-State Machine Representation and State Traversal
        2. 9.3.2. Counterexample Generation
        3. 9.3.3. Equivalence Checking
        4. 9.3.4. Language Containment and Fairness Constraints
      4. 9.4. Symbolic CTL Model Checking
        1. 9.4.1. Fix-point Computation
        2. 9.4.2. CTL Checking with Fairness Constraints
      5. 9.5. Computational Improvements
        1. 9.5.1. Early Quantification
        2. 9.5.2. Generalized Cofactor
      6. 9.6. Using Model-Checking Tools
      7. 9.7. Summary
      8. 9.8. Problems
    15. Bibliography

    Product information

    • Title: Hardware Design Verification: Simulation and Formal Method-Based Approaches
    • Author(s): William K. Lam
    • Release date: March 2005
    • Publisher(s): Pearson
    • ISBN: 9780131433472