相關主題
商品描述
Description
Functional verification has become an important aspect of the chip design process. Significant resources, both in industry and academia, are devoted to the design complexity and verification endeavors.
SAT-Based Scalable Formal Verification Solutions discusses in detail several of the latest and interesting scalable SAT-based techniques including: Hybrid SAT Solver, Customized Bounded/Unbounded Model Checking, Distributed Model Checking, Proofs and Proof-based Abstraction Methods, Verification of Embedded Memory System & Multi-clock Systems, and Synthesis for Verification Paradigm. These techniques have been designed and implemented in a verification platform Verisol (formally called DiVer) and have been used successfully in industry. This book provides algorithmic details and engineering insights into devising scalable approaches for an effective realization. It also includes the authors’ practical experiences and recommendations in verifying the large industry designs using VeriSol.
The book is primarily written for researchers, scientists, and verification engineers who would like to gain an in-depth understanding of scalable SAT-based verification techniques. The book will also be of interest for CAD tool developers who would like to incorporate various SAT-based advanced techniques in their products.
商品描述(中文翻譯)
**描述**
功能驗證已成為晶片設計過程中的一個重要方面。業界和學術界都投入了大量資源於設計複雜性和驗證工作。
《基於SAT的可擴展形式驗證解決方案》詳細討論了幾種最新且有趣的可擴展基於SAT的技術，包括：混合SAT求解器、定制的有界/無界模型檢查、分佈式模型檢查、證明及基於證明的抽象方法、嵌入式記憶體系統及多時鐘系統的驗證，以及驗證範式的綜合。這些技術已在驗證平台Verisol（正式名稱為DiVer）中設計和實現，並已在業界成功應用。本書提供了算法細節和工程見解，以制定可擴展的方法以有效實現。它還包括作者在使用VeriSol驗證大型行業設計方面的實踐經驗和建議。
本書主要針對希望深入了解可擴展基於SAT的驗證技術的研究人員、科學家和驗證工程師。對於希望在其產品中整合各種基於SAT的先進技術的CAD工具開發者，本書也將引起他們的興趣。
