形式化驗證：現代 VLSI 設計的必備工具包 (原書第2版)

Erik Seligman目前是 Cadence設計系統公司的 產品工程架構師，負責規劃和支持 Jasper形式化驗證工具。此前，他在英特爾公司（俄勒岡州希爾斯伯勒）工作了20多年，涉足軟件、設計、仿真和形式化驗證等多個領域。業余時間，他主持“數學突變”（Math Mutation）播客，並曾當選為希爾斯伯勒學區董事會成員。Tom Schubert（現已退休）是波特蘭州立大學電子與計算機工程系的兼職教授，曾負責該校“設計驗證與確認”方向研究生課程長達8年。此前，他在英特爾公司工作17年，曾管理英特爾 的矽前驗證形式化驗證團隊，並在多個微處理器設計項目中推廣和應用 FPV 技術。他在加州大學戴維斯分校獲得計算機科學博士學位。M.V.Achutha Kiran Kumar是英特爾設計工程集團的英特爾研究員，負責領導公司形式化驗證中央技術辦公室，該團隊是 規模 的工業形式化驗證團隊之一。他擁有20多年經驗，曾在芯片設計流程的多個領域工作，包括 RTL 設計、結構設計、電路設計、仿真及多個驗證層級（包括形式化驗證）。

譯者序
第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中使用