芯片形式化驗證原理、方法與實戰

王亮 譚永亮

芯片形式化驗證原理、方法與實戰
  • 出版商: 機械工業
  • 出版日期: 2025-07-01
  • 售價: $594
  • 貴賓價: 9.5 折 $564
  • 語言: 簡體中文
  • 頁數: 286
  • ISBN: 7111782682
  • ISBN-13: 9787111782681
  • 相關分類: 有限元素 Ansys

    • 立即出貨

買這商品的人也買了...

商品描述

本書系統介紹了形式化驗證的概念和原理，並通過豐富的實例生動展示了形式化驗證所需的TCL和SVA語言語法規則，同時揭示了其在商業上的潛在價值和廣闊前景。書中以目前廣泛采用的RISC-V架構為例，借助新思科技的VC Formal形式化驗證工具，深入淺出地講解了各種形式化驗證應用的流程、使用方法以及常見陷阱，為讀者提供了從基礎知識到 應用的學習途徑。 本書包括三個部分： ? 基礎篇（ ～6章），主要介紹形式化驗證的工具、語言和設計； ? 實戰篇（第7～13章），主要展示相關工具的使用方法、常見問題以及對應的解決方案； ? 進階篇（ 4～17章），主要探討簡化、簽核和加速等關鍵形式化驗證技術。 本書不僅適合芯片設計和開發領域的從業人員快速入門和實踐形式化驗證，也可以作為電子工程等相關專業的教學參考書。

作者簡介

王亮

IC工程師，2008年畢業於西北工業大學計算機系統結構專業，擁有接近20年的芯片行業工作經驗，先後就職於S3 Graphics（VIA，2年）、艾薩華科技（LSI，6年）、超微半導體（AMD，9年），目前就職於AMD GPU部門做GPU驗證工作。

譚永亮 

IC設計工程師，2008年研究生畢業於西北工業大學電路與系統專業，擁有接近20年的工作經驗，目前就職於某IC創業公司，擔任芯片設計經理。

目錄大綱

推薦序
前言
基礎篇
第1章 芯片驗證
1.1 什麼是芯片驗證
1.2 芯片驗證的種類和過程
1.3 驗證的現狀
1.4 本章小結
第2章 驗證策略概述
2.1 動態驗證
2.1.1 EDA仿真
2.1.2 硬件仿真
2.1.3 FPGA原型驗證
2.1.4 三種動態驗證方式的比較
2.2 靜態檢查
2.2.1 語法語義檢查
2.2.2 形式化驗證
2.3 形式化驗證和動態驗證的優缺點對比
2.4 形式化驗證的現狀和商業價值
2.5 學習形式化驗證能做什麼
2.6 本章小結
第3章 形式化驗證基本原理和算法
3.1 形式化驗證概述
3.1.1 等價性驗證
3.1.2 模型檢查
3.1.3 定理證明
3.2 硬件電路的形式化驗證原理
3.3 二叉決策圖概述
3.3.1 二叉決策圖原理
3.3.2 有序二叉決策圖
3.3.3 精簡有序二叉決策圖
3.3.4 BDD的不足
3.4 基於SAT的形式化驗證
3.4.1 SAT原理
3.4.2 有界模型檢查問題
3.5 BDD和SAT的比較
3.6 本章小結
第4章 形式化驗證的流程和方法
4.1 形式化驗證“三板斧”
——語言、工具和設計
……
實戰篇
進階篇
附錄 代碼包的目錄及說明
技術術語表
參考文獻

類似商品