形式化驗證(現代VLSI設計的必備工具包原書第2版)/集成電路科學與工程叢書

作者：(美)埃里克·塞利格曼//湯姆·舒伯特//(印)M.V.阿楚塔·基蘭·庫馬爾|責編:劉星寧|譯者:李建文//蒲戈光
出版社：機械工業
ISBN：9787111796565

出版日期：2026/01/01
裝幀：平裝
頁數：315

人民幣：RMB 129 元售價：元

內容大鋼

《形式化驗證：現代VLSI設計的必備工具包（原書第2版）》提供了實用的設計與驗證方法，並包含豐富的實踐建議，幫助工程師將這些技術融入實際工作中。形式化驗證（Formal Verification，FV）使設計人員能夠直接分析和數學化地探索寄存器傳輸級（RTL）設計的質量或其他方面，而無需依賴模擬。這不僅可以減少設計驗證所需的時間，還能更快地實現最終的可製造設計。在具備SystemVerilog基礎知識的前提下，本書將幫助讀者深入理解FV，並掌握其在主流設計和驗證流程中的實際應用。
第2版的每一章都經過更新，以反映不斷發展的FV實踐和高級技術。此外，新加入的第11章提供了實施高質量FV簽核的指南，完全用高效的FV方法替代部分模擬任務。閱讀本書後，讀者將具備在組織中引入FV技術的能力，從而提升設計和驗證效率。

作者介紹

(美)埃里克·塞利格曼//湯姆·舒伯特//(印)M.V.阿楚塔·基蘭·庫馬爾|責編:劉星寧|譯者:李建文//蒲戈光

譯者序
第2版序
第1版序
致謝
第1章  形式化驗證（FV）：從夢想到現實
  1.1  FV是什麼
  1.2  為什麼是這本書
  1.3  一個鼓舞人心的軼事
  1.4  FV：更深層次
    1.4.1  FV的整體優勢
    1.4.2  FV的一般使用模型
    1.4.3  完整覆蓋的FV
    1.4.4  本書未討論的FV方法
  1.5  實用FV的出現
    1.5.1  早期自動推理
    1.5.2  電腦科學應用
    1.5.3  模型檢查變得切實可用
    1.5.4  斷言的標準化
  1.6  實施FV的挑戰
    1.6.1  數學的基本局限性
    1.6.2  複雜性理論
    1.6.3  好消息
  1.7  增強形式化的力量
  1.8  充分利用這本書
  1.9  本章實用建議
  進一步閱讀
第2章  基礎形式化驗證（FV）演算法
  2.1  驗證過程中的FV
  2.2  一個簡單的自動售貨機示例
  2.3  模型比較
  2.4  影響錐
  2.5  規範操作定義
    2.5.1  智能構建真值表
    2.5.2  添加順序邏輯
  2.6  布爾代數符號
    2.6.1  布爾代數基本定律
    2.6.2  規範比較
  2.7  二元決策圖（BDD）
    2.7.1  計算電路設計的 BDD
    2.7.2  使用BDD進行模型檢查
  2.8  布爾可滿足性（SAT）
    2.8.1  有界模型檢查
    2.8.2  解決SAT問題
    2.8.3  Davis-Putnam SAT 演算法
    2.8.4  Davis-Logemann-Loveland SAT 演算法
  2.9  總結
  進一步閱讀
第3章  SystemVerilog斷言簡介
  3.1  基本斷言概念
    3.1.1  一個簡易仲裁器實例

    3.1.2  斷言是什麼
    3.1.3  假設是什麼
    3.1.4  覆蓋屬性是什麼
    3.1.5  斷言語句的說明
    3.1.6  SVA語言基礎
    3.1.7  即時斷言
    3.1.8  編寫即時斷言
    3.1.9  過程代碼的複雜性及採用assert final的動機
    3.1.10  過程塊中的位置
    3.1.11  布爾構建塊
    3.1.12  併發斷言基礎和時鐘控制
    3.1.13  採樣和斷言時鐘
    3.1.14  採樣值函數
    3.1.15  併發斷言的時鐘邊沿
    3.1.16  併發斷言的重置（禁用）條件
    3.1.17  設置默認時鐘和重置
  3.2  序列、屬性和併發斷言
    3.2.1  序列語法和示例
    3.2.2  屬性語法和示例
    3.2.3  命名序列和屬性
    3.2.4  斷言和隱式多線程
    3.2.5  常量的挑戰
    3.2.6  編寫屬性
  3.3  總結
  3.4  本章實用建議
  進一步閱讀
第4章  形式化屬性驗證（FPV）
  4.1  什麼是FPV
  4.2  本章示例：組合鎖
  4.3  搭建基礎的FPV環境
    4.3.1  編譯RTL
    4.3.2  創建覆蓋屬性
    4.3.3  創建假設
    4.3.4  創建斷言
    4.3.5  時鐘和複位
    4.3.6  運行驗證
  4.4  FPV與模擬有何不同
    4.4.1  可以運行哪些類型和規模的模型
    4.4.2  如何達到目標行為
    4.4.3  檢查哪些值
    4.4.4  我們如何約束模型
    4.4.5  如何處理內部節點的約束
    4.4.6  我們用什麼進行調試
    4.4.7  典型軌跡有多長
  4.5  決定在哪裡以及如何運行FPV
    4.5.1  運行FPV的動機
    4.5.2  使用設計探索FPV
    4.5.3  使用錯誤搜索FPV
    4.5.4  使用簽核級FPV
    4.5.5  使用特定應用FPV

  4.6  總結
  4.7  本章實用建議
  進一步閱讀
第5章  用於設計探索的有效形式化屬性驗證（FPV）
  5.1  本章示例：交通燈控制器
  5.2  創建設計探索計劃
    5.2.1  設計探索目標
    5.2.2  設計探索的主要屬性
    5.2.3  複雜性分級計劃
    5.2.4  退出標準
    5.2.5  整合計劃
  5.3  設置設計探索FPV環境
    5.3.1  覆蓋屬性
    5.3.2  假設
    5.3.3  斷言
    5.3.4  時鐘和複位
    5.3.5  健全性（sanity）檢查
  5.4  波形調試迭代（wiggling）設計
    5.4.1  wiggling過程
    5.4.2  wiggling階段1：我們的第一個短波形
    5.4.3  調試另一個短波形
  5.5  探索更關鍵的行為
    5.5.1  回答一些新問題
    5.5.2  證明斷言
  5.6  移除簡化並探索更多行為
    5.6.1  面對複雜性問題
  5.7  總結
  5.8  本章實用建議
  進一步閱讀
第6章  有效形式化屬性驗證（FPV）
  6.1  確定FPV目標
    6.1.1  錯誤搜索FPV
    6.1.2  簽核級FPV
  6.2  FPV工作的分階段進行
  6.3  本章示例：簡單的ALU
  6.4  理解設計
  6.5  FPV驗證計劃的制定
    6.5.1  FPV目標
    6.5.2  FPV主要屬性
    6.5.3  處理複雜性
    6.5.4  質量檢查與退出標準
    6.5.5  初始覆蓋屬性
    6.5.6  擴展wiggling
    6.5.7  擴展覆蓋屬性
  6.6  去除簡化和探索更多行為
    6.6.1  演進到簽核級FPV
  6.7  總結
  6.8  本章實用建議
  進一步閱讀
第7章  針對特定問題的形式化屬性驗證（FPV）APP

  7.1  可重用協議驗證
    7.1.1  可重用屬性集的基本設計
    7.1.2  屬性方向問題
    7.1.3  驗證屬性集一致性
    7.1.4  完整性檢查
    7.1.5  動態驗證兼容性
  7.2  不可達覆蓋消除
    7.2.1  在UCE中使用斷言的作用
    7.2.2  覆蓋組和其他覆蓋類型
  7.3  連通性驗證
    7.3.1  連通性模型構建
    7.3.2  指定連通性
    7.3.3  可能的連通性FPV複雜性
    7.3.4  連通性FPV的覆蓋率
  7.4  控制寄存器驗證
    7.4.1  指定控制寄存器要求
    7.4.2  控制寄存器的SVA
    7.4.3  控制寄存器驗證的主要挑戰
  7.5  硅后調試和反應性FPV
    7.5.1  硅后FPV的挑戰
    7.5.2  UNEARTH：一種實用的硅后FPV方法
  7.6  總結
  7.7  本章實用建議
  進一步閱讀
第8章  形式化等價性驗證（FEV）
  8.1  等價性檢查的類型
    8.1.1  組合等價性
    8.1.2  順序等價性
    8.1.3  事務級等價性
  8.2  FEV用例
    8.2.1  RTL到網表FEV
    8.2.2  網表到網表FEV
    8.2.3  RTL到RTL FEV
  8.3  運行FEV
    8.3.1  選擇模型
    8.3.2  關鍵點選擇和映射
    8.3.3  假設和約束
    8.3.4  調試不匹配
  8.4  額外的FEV挑戰
    8.4.1  狀態元素優化
    8.4.2  條件等價性
    8.4.3  不關心空間
    8.4.4  複雜性
  8.5  總結
  8.6  本章實用建議
  進一步閱讀
第9章  形式化驗證最大的失誤：誤報的危險
  9.1  濫用 SVA 語言
    9.1.1  缺少分號
    9.1.2  兩個時鐘邊沿均置位

    9.1.3  帶斷言的短路函數
    9.1.4  信號採樣的微妙影響
    9.1.5  非生命狀態的活性屬性
    9.1.6  錯誤地假設一個序列
    9.1.7  預防與 SVA 相關的誤報
  9.2  空洞問題
    9.2.1  誤導性的覆蓋屬性與糟糕的重置
    9.2.2  經過驗證但模擬失敗的內存控制器
    9.2.3  假設與約束的矛盾
    9.2.4  隊列永遠不會滿，因為它永遠不會開始
    9.2.5  防止空洞工具和用戶的責任
  9.3  隱含或未說明的假設
    9.3.1  具有實施假設的庫
    9.3.2  對多重驅動信號的期望
    9.3.3  無法到達的邏輯元素：需要嗎
    9.3.4  防止誤解
  9.4  分工
    9.4.1  膠合邏輯缺失
    9.4.2  缺失案例的拆分
    9.4.3  撤銷臨時黑客攻擊
    9.4.4  安全分工
  9.5  總結
  9.6  本章實用建議
  進一步閱讀
第10章  應對複雜性
  10.1  設計狀態和相關複雜性
  10.2  本章示例：內存控制器
  10.3  觀察複雜性問題
  10.4  簡單的收斂技術
    10.4.1  選擇正確的戰鬥
    10.4.2  時鐘和複位
    10.4.3  引擎調校
    10.4.4  黑盒化
    10.4.5  參數和尺寸減小
    10.4.6  案例拆分
    10.4.7  硬案例與軟案例拆分
    10.4.8  屬性簡化
    10.4.9  切點
    10.4.10  增量FEV
  10.5  輔助假設與非輔助假設
    10.5.1  編寫自定義輔助假設
    10.5.2  利用已證實的斷言
    10.5.3  您是否有太多的假設
  10.6  使用自由變數進行概括分析
    10.6.1  利用剛性自由變數的對稱性
    10.6.2  自由變數的其他用途
    10.6.3  自由變數的缺點
  10.7  降低複雜性的抽象模型
    10.7.1  反抽象
    10.7.2  序列抽象

    10.7.3  內存抽象
    10.7.4  影子模型
  10.8  半形式化驗證
  10.9  規避複雜性問題：設計和驗證協同工作
  10.10  總結
  10.11  本章的實用建議
  進一步閱讀
第11章  實際項目中的形式化簽核
  11.1  整體簽核方法論
  11.2  規劃和架構
    11.2.1  分治法識別DUT
    11.2.2  審查設計流程
    11.2.3  選擇應用程序
    11.2.4  定義FPV細節
    11.2.5  填補空白
    11.2.6  制定應急計劃
    11.2.7  FV融入設計節點中
  11.3  應用和實施
    11.3.1  確保定期進展
    11.3.2  做好應對反應性FV的準備
  11.4  覆蓋和回歸
    11.4.1  代碼覆蓋
    11.4.2  覆蓋屬性
    11.4.3  FV回歸
    11.4.4  機器學習和回歸
    11.4.5  網路與雲端運行
    11.4.6  晚期重檢
  11.5  跟蹤和結束
    11.5.1  FV的質量
    11.5.2  時間線跟蹤
    11.5.3  驗證何時才算完成
  11.6  總結
  11.7  本章實用建議
第12章  全新的具有FV風格的生活方式
  12.1  使用FV
    12.1.1  設計探索
    12.1.2  錯誤搜索FPV
    12.1.3  簽核級FV
    12.1.4  專用的FV應用程序
    12.1.5  形式化等價性驗證
  12.2  個人使用FV的準備
  12.3  啟動團隊的FV工作
    12.3.1  設定合理的期望
    12.3.2  培養「領軍人物」
    12.3.3  爭取各級的支持
    12.3.4  合理跟蹤FV的進展
    12.3.5  建立高效的基礎設施
  12.4  使管理層開心
    12.4.1  ROI計算
    12.4.2  錯誤複雜性排名

  12.5  FV工作者實際做了什麼
  12.6  總結
  12.7  本章實用建議
  進一步閱讀

同類熱銷排行榜

最近瀏覽的商品

形式化驗證(現代VLSI設計的必備工具包原書第2版)/集成電路科學與工程叢書