Verification Techniques for System-Level Design

Verification Techniques for System-Level Design

by Masahiro Fujita, Indradeep Ghosh, Mukul Prasad
Released July 2010
Publisher(s): Morgan Kaufmann
ISBN: 9780080553139

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

This book will explain how to verify SoC (Systems on Chip) logic designs using “formal” and “semiformal” verification techniques. The critical issue to be addressed is whether the functionality of the design is the one that the designers intended. Simulation has been used for checking the correctness of SoC designs (as in “functional” verification), but many subtle design errors cannot be caught by simulation. Recently, formal verification, giving mathematical proof of the correctness of designs, has been gaining popularity.For higher design productivity, it is essential to debug designs as early as possible, which this book facilitates. This book covers all aspects of high-level formal and semiformal verification techniques for system level designs.

• First book that covers all aspects of formal and semiformal, high-level (higher than RTL) design verification targeting SoC designs.• Formal verification of high-level designs (RTL or higher).• Verification techniques are discussed with associated system-level design methodology.

Table of contents

  1. Copyright
  2. The Morgan Kaufmann Series in Systems on Silicon
  3. Acknowledgments
  4. 1. Introduction
  5. 2. Higher-Level Design Methodology and Associated Verification Problems
    1. 2.1. Introduction
    2. 2.2. Issues in High-Level Design
    3. 2.3. C/C++-Based Design and Specification Languages
      1. 2.3.1. SpecC Language
      2. 2.3.2. The Semantics of par Statements
      3. 2.3.3. Relationship with Simulation Time
    4. 2.4. System-Level Design Methodology Based on C/C++-Based Design and Specification Languages
    5. 2.5. Verification Problems in High-Level Designs
  6. 3. Basic Technology for Formal Verification
    1. 3.1. The Boolean Satisfiability Problem
    2. 3.2. The DPLL Algorithm
    3. 3.3. Enhancements to Modern SAT Solvers
    4. 3.4. Capabilities of Modern SAT Solvers
    5. 3.5. Binary Decision Diagrams
      1. 3.5.1. Manipulation of BDDs
      2. 3.5.2. Variants of BDDs
    6. 3.6. Automatic Test Pattern Generation Engines
      1. 3.6.1. Single Stuck-at Testing for Combinational Circuits
        1. The D-Algorithm [25]
        2. Podem [26]
        3. Fan [27]
      2. 3.6.2. Stuck-at Testing in Sequential Circuits
    7. 3.7. SAT, BDD, and ATPG Engines for Validation
    8. 3.8. Theorem-Proving and Decision Procedures
    9. References
  7. 4. Verification Algorithms for FSM Models
    1. 4.1. Combinational Equivalence Checking
      1. 4.1.1. Sequential Equivalence Checking as Combinational Equivalence Checking
      2. 4.1.2. Latch Mapping Problem
      3. 4.1.3. EC Based on Internal Equivalences
      4. 4.1.4. Anatomy and Capabilities of Modern CEC Tools
    2. 4.2. Model Checking
      1. 4.2.1. Modeling Concurrent Systems
        1. Kripke Structures
      2. 4.2.2. Temporal Logics
        1. Computation Tree Logic CTL*
        2. CTL and LTL
      3. 4.2.3. Types of Properties
      4. 4.2.4. Basic Model-Checking Algorithms
      5. 4.2.5. Symbolic Model Checking
        1. Symbolic Model Checking Using BDDs
        2. Symbolic Model Checking Using SAT
          1. SAT-Based State Space Search
          2. SAT-Based Inductive Reasoning
    3. 4.3. Semi-Formal Verification Techniques
      1. 4.3.1. SAT-based Bounded Model Checking
        1. Structural Pruning during CNF Generation
        2. Decision Variable Ordering of the SAT Solver
        3. Addition of Constraints to the SAT Problem
        4. Methodology Improvements to BMC
        5. Industrial Application of BMC
      2. 4.3.2. Symbolic Simulation
      3. 4.3.3. Enhancing Simulation Using Formal Methods
    4. 4.4. Conclusion
    5. References
  8. 5. Static Checking of Higher-Level Design Descriptions
    1. 5.1. Program Slicing
      1. 5.1.1. System Dependence Graph
      2. 5.1.2. Nodes and Edges
      3. 5.1.3. Concurrency
      4. 5.1.4. Synchronization on Concurrent Processes
    2. 5.2. Checking Method and Its Implying Design Flow
      1. 5.2.1. Basic Static Description Checking
        1. Detection of Unused Variables/Unused Statements
        2. Detection of Uninitialized Variables
      2. 5.2.2. Improvement of Accuracy Using Conditions of Control Nodes
        1. Detection of Out-of-Bounds Array Index
        2. Detection of Deadlock
        3. Detection of Race Condition
    3. 5.3. Application of the Checking Methods to HW/SW Partitioning and Optimization
    4. 5.4. Case Study
      1. 5.4.1. MPEG2
      2. 5.4.2. JPEG2000
      3. 5.4.3. Experimental Results on Static Checking
    5. References
  9. 6. Equivalence Checking on Higher-Level Design Descriptions
    1. 6.1. Introduction
    2. 6.2. High-Level Design Flow from the Viewpoint of Equivalence Checking
    3. 6.3. Symbolic Simulation for Equivalence Checking
    4. 6.4. Equivalence-Checking Methods Based on the Identification of Differences between two Descriptions
      1. 6.4.1. Identification of Differences between Two Descriptions
      2. 6.4.2. Symbolic Simulation Based on Textual Differences
      3. 6.4.3. Example
      4. 6.4.4. Experimental Results
    5. 6.5. Further Improvement on the Use of Differences between Two Descriptions
      1. 6.5.1. Extension of the Verification Area
      2. 6.5.2. Symbolic Simulation on SDGs
      3. 6.5.3. Verification Example
      4. 6.5.4. Discussion of the Strategy of Extension
      5. 6.5.5. Experimental Results on the Extension-Based Method
    6. References
  10. 7. Model Checking on Higher-Level Design Descriptions
    1. 7.1. Introduction
    2. 7.2. Goal of Synchronization Verification in High-Level Designs
    3. 7.3. Model Checking and High-Level Design Descriptions
    4. 7.4. Brief Review of SpecC and Its Semantics for Synchronization Verification
    5. 7.5. Synchronization Verification Framework
      1. 7.5.1. From SpecC to Boolean SpecC
      2. 7.5.2. From Boolean SpecC to Mathematical Representations of Equalities/Inequalities
      3. 7.5.3. Verification Method
      4. 7.5.4. Validating the Abstract Counterexample
      5. 7.5.5. Checking for Race Conditions
      6. 7.5.6. Renaming Variables
      7. 7.5.7. Predicate Discovery and Boolean SpecC Refinement
    6. 7.6. Experimental Results
    7. References
  11. 8. Simulation-Based Verification Techniques for System-Level Designs
    1. 8.1. Introduction
    2. 8.2. Simulation Types
      1. 8.2.1. Event-Driven Simulation
      2. 8.2.2. Cycle-Based Simulation
      3. 8.2.3. Specification/Behavior-Level Simulation
      4. 8.2.4. Mixed-Mode Simulation
    3. 8.3. High-Level Simulation Tools
      1. 8.3.1. Static Checking (Linting)
      2. 8.3.2. Simulators, Waveform Viewers, and Debuggers
    4. 8.4. Simulation Drawbacks
    5. 8.5. Coverage Metrics
      1. 8.5.1. Drawbacks of Coverage Metrics
    6. 8.6. Test-Bench Automation
      1. 8.6.1. Transaction Level Modeling
      2. 8.6.2. Property Specification Languages
      3. 8.6.3. Test-Bench Automation Frameworks
      4. 8.6.4. Model-Driven Automatic Test-Bench Generation
      5. 8.6.5. Automatic Test-Bench Generation from Implementation Design
    7. 8.7. Tackling Performance Issues
      1. 8.7.1. Emulation and Hardware Acceleration
      2. 8.7.2. Using Preverified IPs/Cores and Higher Abstraction Levels
      3. 8.7.3. Correct by Construction Design
    8. 8.8. Stopping Criteria
    9. 8.9. An Example Case Study
    10. 8.10. Conclusion
    11. 8.11. Future Directions
    12. References
  12. 9. Conclusion

Product information

  • Title: Verification Techniques for System-Level Design
  • Author(s): Masahiro Fujita, Indradeep Ghosh, Mukul Prasad
  • Release date: July 2010
  • Publisher(s): Morgan Kaufmann
  • ISBN: 9780080553139