rdf-syntax-grammar
mods:
  schema location: http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
  title info:
    title: Formal verification
    sub title: an essential toolkit for modern VLSI design
  name:
    name part: Seligman, Erik.
    role:
      role term: creator
  name:
    name part: Schubert, Tom.
  name:
    name part: Kumar, M. V. Achutha Kiran.
  name:
    name part: ScienceDirect (Online service)
  type of resource: text
  genre: Electronic books.
  origin info:
    place:
      place term: ne
    place:
      place term: Amsterdam
    publisher: Elsevier Science
    date issued: 2015
    issuance: monographic
  language:
    language term: eng
  physical description:
    form: remote
    extent: 1 online resource (372 pages) : illustrations
  abstract: 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 presents the practical applications that are bringing it into mainstream design and validation processes at Intel and other companies. The text prepares readers to effectively introduce FV in their organization and deploy FV techniques to increase design and validation productivity.
  table of contents: 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.
  table of contents: 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.
  table of contents: 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.
  table of contents: 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.
  table of contents: 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?
  note: Erik Seligman, Tom Schubert, M.V. Achutha Kiran Kumar.
  note: Includes index.
  note: How Do We Reach Targeted Behaviors?
  subject:
    topic: Electronic circuits
    topic: Testing
  subject:
    topic: Integrated circuits
    topic: Very large scale integration
    topic: Design and construction
  subject:
    topic: Verilog (Computer hardware description language)
  subject:
    topic: Verilog (Langage de description de matériel informatique)
  subject:
    topic: TECHNOLOGY & ENGINEERING
    topic: Mechanical
  subject:
    topic: Electronic circuits
    topic: Testing
  subject:
    topic: Integrated circuits
    topic: Very large scale integration
    topic: Design and construction
  subject:
    topic: Verilog (Computer hardware description language)
  classification: TK7867
  classification: 621.3815/48
  related item:
    title info:
      title: Formal Verification : An Essential Toolkit for Modern VLSI Design
    name:
      name part: Seligman, Erik.
    origin info:
      publisher: Burlington : Elsevier Science, ©2015
  identifier: 9780128008157
  identifier: 0128008156
  identifier: 9780128007273
  identifier: http://proxy.library.tamu.edu/login
  record info:
    record content source: EBLCP
    record creation date: 150801
    record change date: 20260326213723.5
    record identifier: in00005759413
    language of cataloging:
      language term: eng