Название: Formal Verification: An Essential Toolkit for Modern VLSI Design, 2nd EditionАвтор: Erik Seligman, Tom Schubert, M.V. Achutha Kiran Kumar
Издательство: Morgan Kaufmann/Elsevier
Год: 2023
Страниц: 428
Язык: английский
Формат: pdf (true)
Размер: 10.2 MB
Formal Verification: An Essential Toolkit for Modern VLSI Design, Second Edition presents practical approaches for design and validation, with hands-on advice to help working engineers integrate these techniques into their work. Formal Verification (FV) enables a designer to directly analyze and mathematically explore the quality or other aspects of a Register Transfer Level (RTL) design without using simulations. This can reduce time spent validating designs and more quickly reach a final design for manufacturing. Building on a basic knowledge of SystemVerilog, this book demystifies FV and presents the practical applications that are bringing it into mainstream design and validation processes.
New sections cover advanced techniques, and a new chapter, The Road To Formal Signoff, emphasizes techniques used when replacing simulation work with Formal Verification. After reading this book, readers will be prepared to introduce FV in their organization to effectively deploy FV techniques that increase design and validation productivity.
The authors of this book start by describing their goal: helping VLSI designers and validators who focus on RTL to do their jobs more effectively and efficiently by leveraging FV techniques. This approach is sometimes referred to at Intel as the democratization of FV, or “FV for All,” since the intent is to expand the use of FV beyond the realm of FV experts and enable much wider use of FV tools and techniques. They briefly describe the history of FV: how early artificial intelligence concepts led to FV; theoretical objections to FVand why they are not true blocking issues; and general techniques for abstracting problems to make them more tractable for FV.
Chapter 2 describes basic FV algorithms in enough detail to convince the reader that FV isn’t some form of black magicdthese techniques really do gain full coverage without requiring exhaustive (and computationally infeasible) simulation cycles. In particular, the Boolean satisfiability (SAT) problem is explained, along with a description of the model-checking algorithms and tools that allow it to be solved for many classes of problem.
Chapter 3 provides an introduction to System Verilog Assertions (SVAs): what they are (and the different types of SVAs such as simple Boolean conditions, temporal assertions, etc.) and how they can be combined into sequences and properties.
Chapter 4 builds on this by introducing the concept of Formal Property Verification (FPV): what it is; how it compares with dynamic simulation; and usage models such as design exploration, bug hunting, and bounded- and full-proofs. The heart of the book lies in Chapters 5 and 6, which explain how to make effective use of FPV for Design Exercise and Verification, respectively. The authors’ extensive experience with the application of FPV to real-world problems illuminates almost every page of these two chapters with examples gleaned from current and past Intel development projects, along with many helpful hints that will enable the novice user to make effective use of FPV tools.
Chapter 7 switches gears to describe how FPV can be used to create “Apps” for different design domains such as post-silicon bug reproduction, SoC connectivity checking, standard (nonproject-specific) protocol verification, unreachable coverage elimination, and control register access policies. These apps enable design and validation engineers who do not have an FV background to quickly apply FV methods to the targeted domains, rather than relying on expensive and time-consuming dynamic simulation.
Chapter 11 wraps things up by describing how the reader can introduce the techniques described in this book into his or her organization, and effectively deploy them to increase design and validation productivity. Once again, the emphasis is on the practical: solving real-life problems, using small experiments to demonstrate the power of FPV techniques, getting measurable results, and data that help to convince skeptics.
Скачать Formal Verification: An Essential Toolkit for Modern VLSI Design, 2nd Edition