000			05723cam a2200541Ia 4500
001			ocn915311665
003			OCoLC
005			20190328114812.0
006			m o d
007			cr cnu---unuuu
008			150801s2015 ne a o 001 0 eng d
040			_aEBLCP _beng _epn _cEBLCP _dN$T _dOCLCO _dOPELS _dIDEBK _dYDXCP _dCDX _dOCLCF _dOCLCO _dDEBSZ _dOCLCO _dOCLCQ _dOCLCO _dOCLCQ _dUAB _dOCLCQ _dK6U _dMERUC _dU3W _dD6H _dAU@ _dCOO _dOCLCQ
020			_a9780128008157 _q(electronic bk.)
020			_a0128008156 _q(electronic bk.)
020			_z9780128007273
035			_a(OCoLC)915311665
050		4	_aTK7867
072		7	_aTEC _x009070 _2bisacsh
082	0	4	_a621.3815/48
100	1		_aSeligman, Erik.
245	1	0	_aFormal verification : an essential toolkit for modern VLSI design / _h[electronic resource] _cErik Seligman, Tom Schubert, M.V. Achutha Kiran Kumar.
260			_aAmsterdam : _bElsevier Science, _c2015.
300			_a1 online resource (372 pages) : _billustrations
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
500			_aIncludes index.
588	0		_aPrint version record.
505	0		_aFront 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		_aModel 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		_aBasic 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		_aWriting 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		_aWriting 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			_aHow Do We Reach Targeted Behaviors?
520			_aFormal 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	_aElectronic circuits _xTesting.
650		0	_aIntegrated circuits _xVery large scale integration _xDesign and construction.
650		0	_aVerilog (Computer hardware description language)
650		7	_aTECHNOLOGY & ENGINEERING _xMechanical. _2bisacsh
650		7	_aElectronic circuits _xTesting. _2fast _0(OCoLC)fst00906898
650		7	_aIntegrated circuits _xVery large scale integration _xDesign and construction. _2fast _0(OCoLC)fst00975610
650		7	_aVerilog (Computer hardware description language) _2fast _0(OCoLC)fst01165388
655		4	_aElectronic books.
700	1		_aSchubert, Tom.
700	1		_aKumar, M. V. Achutha Kiran.
776	0	8	_iPrint version: _aSeligman, Erik. _tFormal Verification : An Essential Toolkit for Modern VLSI Design. _dBurlington : Elsevier Science, �2015 _z9780128007273
856	4	0	_3ScienceDirect _uhttp://www.sciencedirect.com/science/book/9780128007273
999			_c247124 _d247124