Formal verification : an essential toolkit for modern VLSI design / (Record no. 247124)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 05723cam a2200541Ia 4500 |
| 001 - CONTROL NUMBER | |
| control field | ocn915311665 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20190328114812.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS | |
| fixed length control field | m o d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr cnu---unuuu |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 150801s2015 ne a o 001 0 eng d |
| 040 ## - CATALOGING SOURCE | |
| Original cataloging agency | EBLCP |
| Language of cataloging | eng |
| Description conventions | pn |
| Transcribing agency | EBLCP |
| Modifying agency | N$T |
| -- | OCLCO |
| -- | OPELS |
| -- | IDEBK |
| -- | YDXCP |
| -- | CDX |
| -- | OCLCF |
| -- | OCLCO |
| -- | DEBSZ |
| -- | OCLCO |
| -- | OCLCQ |
| -- | OCLCO |
| -- | OCLCQ |
| -- | UAB |
| -- | OCLCQ |
| -- | K6U |
| -- | MERUC |
| -- | U3W |
| -- | D6H |
| -- | AU@ |
| -- | COO |
| -- | OCLCQ |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9780128008157 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 0128008156 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 9780128007273 |
| 035 ## - SYSTEM CONTROL NUMBER | |
| System control number | (OCoLC)915311665 |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | TK7867 |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | TEC |
| Subject category code subdivision | 009070 |
| Source | bisacsh |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 621.3815/48 |
| 100 1# - MAIN ENTRY--PERSONAL NAME | |
| Personal name | Seligman, Erik. |
| 245 10 - TITLE STATEMENT | |
| Title | Formal verification : an essential toolkit for modern VLSI design / |
| Medium | [electronic resource] |
| Statement of responsibility, etc. | Erik Seligman, Tom Schubert, M.V. Achutha Kiran Kumar. |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) | |
| Place of publication, distribution, etc. | Amsterdam : |
| Name of publisher, distributor, etc. | Elsevier Science, |
| Date of publication, distribution, etc. | 2015. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | 1 online resource (372 pages) : |
| Other physical details | illustrations |
| 336 ## - CONTENT TYPE | |
| Content type term | text |
| Content type code | txt |
| Source | rdacontent |
| 337 ## - MEDIA TYPE | |
| Media type term | computer |
| Media type code | c |
| Source | rdamedia |
| 338 ## - CARRIER TYPE | |
| Carrier type term | online resource |
| Carrier type code | cr |
| Source | rdacarrier |
| 500 ## - GENERAL NOTE | |
| General note | Includes index. |
| 588 0# - SOURCE OF DESCRIPTION NOTE | |
| Source of description note | Print version record. |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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? |
| 500 ## - GENERAL NOTE | |
| General note | How Do We Reach Targeted Behaviors? |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | 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. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Electronic circuits |
| General subdivision | Testing. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Integrated circuits |
| General subdivision | Very large scale integration |
| -- | Design and construction. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Verilog (Computer hardware description language) |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | TECHNOLOGY & ENGINEERING |
| General subdivision | Mechanical. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Electronic circuits |
| General subdivision | Testing. |
| Source of heading or term | fast |
| Authority record control number | (OCoLC)fst00906898 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Integrated circuits |
| General subdivision | Very large scale integration |
| -- | Design and construction. |
| Source of heading or term | fast |
| Authority record control number | (OCoLC)fst00975610 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Verilog (Computer hardware description language) |
| Source of heading or term | fast |
| Authority record control number | (OCoLC)fst01165388 |
| 655 #4 - INDEX TERM--GENRE/FORM | |
| Genre/form data or focus term | Electronic books. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Schubert, Tom. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Kumar, M. V. Achutha Kiran. |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Print version: |
| Main entry heading | Seligman, Erik. |
| Title | Formal Verification : An Essential Toolkit for Modern VLSI Design. |
| Place, publisher, and date of publication | Burlington : Elsevier Science, �2015 |
| International Standard Book Number | 9780128007273 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Materials specified | ScienceDirect |
| Uniform Resource Identifier | http://www.sciencedirect.com/science/book/9780128007273 |
No items available.