Verification Techniques for System-Level Design.Material type: TextSeries: eBooks on DemandSystems on Silicon: Publisher: Burlington : Elsevier Science, 2014Description: 1 online resource (251 p.)ISBN: 9780080553139Subject(s): Formal methods (Computer science) | Integrated circuits | Integrated circuits - Verification | Systems on a chip - Testing | Systems on a chip | Testing | VerificationGenre/Form: Electronic books.Additional physical formats: Print version:: Verification Techniques for System-Level DesignDDC classification: 621.3815 LOC classification: TK7895.E42F95 2008Online resources: Click here to view this ebook.
|Item type||Current location||Call number||URL||Status||Date due||Barcode|
|Electronic Book||UT Tyler Online Online||TK7895.E42F95 2008 (Browse shelf)||http://uttyler.eblib.com/patron/FullRecord.aspx?p=318151||Available||EBL318151|
Front Cover; Verification Techniques For System-Level Design; Copyright Page; Contents; Acknowledgments; Chapter 1 Introduction; Chapter 2 Higher-Level Design Methodology and Associated Verification Problems; 2.1 Introduction; 2.2 Issues in High-Level Design; 2.3 C/C++-Based Design and Specification Languages; 2.3.1 SpecC Language; 2.3.2 The Semantics of par Statements; 2.3.3 Relationship with Simulation Time; 2.4 System-Level Design Methodology Based on C/C++-Based Design and Specification Languages; 2.5 Verification Problems in High-Level Designs
Chapter 3 Basic Technology for Formal Verification3.1 The Boolean Satisfiability Problem; 3.2 The DPLL Algorithm; 3.3 Enhancements to Modern SAT Solvers; 3.4 Capabilities of Modern SAT Solvers; 3.5 Binary Decision Diagrams; 3.5.1 Manipulation of BDDs; 3.5.2 Variants of BDDs; 3.6 Automatic Test Pattern Generation Engines; 3.6.1 Single Stuck-at Testing for Combinational Circuits; 3.6.2 Stuck-at Testing in Sequential Circuits; 3.7 SAT, BDD, and ATPG Engines for Validation; 3.8 Theorem-Proving and Decision Procedures; References; Chapter 4 Verification Algorithms for FSM Models
4.1 Combinational Equivalence Checking4.1.1 Sequential Equivalence Checking as Combinational Equivalence Checking; 4.1.2 Latch Mapping Problem; 4.1.3 EC Based on Internal Equivalences; 4.1.4 Anatomy and Capabilities of Modern CEC Tools; 4.2 Model Checking; 4.2.1 Modeling Concurrent Systems; 4.2.2 Temporal Logics; 4.2.3 Types of Properties; 4.2.4 Basic Model-Checking Algorithms; 4.2.5 Symbolic Model Checking; 4.3 Semi-Formal Verification Techniques; 4.3.1 SAT-Based Bounded Model Checking; 4.3.2 Symbolic Simulation; 4.3.3 Enhancing Simulation Using Formal Methods; 4.4 Conclusion; References
Chapter 5 Static Checking of Higher-Level Design Descriptions5.1 Program Slicing; 5.1.1 System Dependence Graph; 5.1.2 Nodes and Edges; 5.1.3 Concurrency; 5.1.4 Synchronization on Concurrent Processes; 5.2 Checking Method and Its Implying Design Flow; 5.2.1 Basic Static Description Checking; 5.2.2 Improvement of Accuracy Using Conditions of Control Nodes; 5.3 Application of the Checking Methods to HW/SW Partitioning and Optimization; 5.4 Case Study; 5.4.1 MPEG2; 5.4.2 JPEG2000; 5.4.3 Experimental Results on Static Checking; References
Chapter 6 Equivalence Checking on Higher-Level Design Descriptions6.1 Introduction; 6.2 High-Level Design Flow from the Viewpoint of Equivalence Checking; 6.3 Symbolic Simulation for Equivalence Checking; 6.4 Equivalence-Checking Methods Based on the Identification of Differences between two Descriptions; 6.4.1 Identification of Differences between Two Descriptions; 6.4.2 Symbolic Simulation Based on Textual Differences; 6.4.3 Example; 6.4.4 Experimental Results; 6.5 Further Improvement on the Use of Differences between Two Descriptions; 6.5.1 Extension of the Verification Area
6.5.2 Symbolic Simulation on SDGs
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.<br><br>For higher design productivity, it is essential to debug desig
Description based upon print version of record.