Formal verification an essential toolkit for modern VLSI design
Formal Verification: An Essential Toolkit for Modern VLSI Design presents practical approaches for design and validation, with hands-on advice for working engineers integrating these techniques into their work. Building on a basic knowledge of System Verilog, this book demystifies FV and present...
| Otros Autores: | , , , |
|---|---|
| Formato: | Libro electrónico |
| Idioma: | Inglés |
| Publicado: |
Amsterdam, [Netherlands] :
Morgan Kaufmann
2015.
|
| Edición: | 1st edition |
| Materias: | |
| Ver en Biblioteca Universitat Ramon Llull: | https://discovery.url.edu/permalink/34CSUC_URL/1im36ta/alma991009629570406719 |
Tabla de Contenidos:
- Front Cover; Formal Verification; Copyright Page; Contents; Foreword for "Formal Verification: An Essential Toolkit for Modern VLSI Design"; Acknowledgments; 1 Formal verification: from dreams to reality; What Is FV?; Why This Book?; A Motivating Anecdote; FV: The Next Level of Depth; Overall Advantages of FV; General Usage Models for FV; FV for Complete Coverage; FV for Bug Hunting; FV for Exploring Designs; FV in Real Design Flows; FV Methods Not Discussed In This Book; The Emergence of Practical FV; Early Automated Reasoning; Applications to Computer Science
- Model Checking Becomes PracticalThe Standardizing of Assertions; Challenges in Implementing FV; Fundamental Limitations of Mathematics; Complexity Theory; The Good News; Amplifying the Power of Formal; Getting the Most Out of This Book; Practical Tips from This Chapter; Further Reading; 2 Basic formal verification algorithms; Formal Verification (FV) in the Validation Process; A Simple Vending Machine Example; Comparing Specifications; Cones of Influence; Formalizing Operation Definitions; Building Truth Tables Intelligently; Adding Sequential Logic; Boolean Algebra Notation
- Basic Boolean Algebra LawsComparing Specifications; BDDs; Computing a BDD for a Circuit Design; Model Checking; Boolean Satisfiability; Bounded Model Checking; Solving the SAT Problem; The Davis-Putnam SAT Algorithm; The Davis Logemann Loveland (DLL) SAT Algorithm; Additional SAT Algorithm Improvements; Chapter Summary; Further Reading; 3 Introduction to systemverilog assertions; Basic Assertion Concepts; A Simple Arbiter Example; What are Assertions?; What are Assumptions?; What are Cover Points?; Clarification on Assertion Statements; SVA Assertion Language Basics; Immediate Assertions
- Writing Immediate AssertionsComplications of Procedural Code and Motivation for Assert Final; Location in Procedural Blocks; Boolean Building Blocks; Concurrent Assertion Basics and Clocking; Sampling and Assertion Clocking; Sampled Value Functions; Concurrent Assertion Clock Edges; Concurrent Assertion Reset (Disable) Conditions; Setting Default Clock and Reset; Sequences, Properties, and Concurrent Assertions; Sequence Syntax and Examples; Using sequences instead of rose/fell; Property Syntax and Examples; Named Sequences and Properties; Assertions and Implicit Multithreading
- Writing the PropertiesPlanning properties at the specification phase; Embedded properties during RTL development; Validation-focused properties; Connecting the properties to your design; Summary; Practical Tips from this Chapter; Further Reading; 4 Formal property verification; What is FPV?; Example for this Chapter: Combination Lock; Bringing Up a Basic FPV Environment; Compiling your RTL; Creating cover points; Creating assumptions; Creating assertions; Clocks and resets; Running the verification; How is FPV Different from Simulation?; What Types and Sizes of Models can be Run?
- How Do We Reach Targeted Behaviors?
