新書推薦：
《
日本首都圈空间结构与协同发展
》
售價：HK$
140.8
《
《欧罗巴的悲剧：经济危机、绥靖政策与第二次世界大战的爆发》
》
售價：HK$
83.6
《
中药炮制学科发展集萃
》
售價：HK$
239.8
《
君士坦丁堡深仇400年：俄土战争（1877—1878）（全2册）
》
售價：HK$
226.6
《
城市文明蓝皮书：全球城市文明发展报告（2024-2025）
》
售價：HK$
140.8
《
未来生活金融指南
》
售價：HK$
63.8
《
《法官如何裁判》（在法律规范体系的框架下如何寻求个案公正的判决之道，麦读译丛18）
》
售價：HK$
86.9
《
自由的危机：全球视角下的英国内战史
》
售價：HK$
173.8
|
| 編輯推薦： |
|
在集成电路设计领域，验证方法主要分为两种：一种是依据激励响应模式的UVM（Universal Verification Methodology）方法，另一种则是基于数学定理证明的形式化验证方法。作者结合自己多年的形式化验证经验，系统地阐述了形式化验证的概念和原理，通过丰富的实例生动地展示了形式化验证所需的TCL语言和SVA语言语法规则。书中以目前广泛采用的RISC-V架构为例，借助业界领先的新思科技VC Formal形式化验证工具，全面展示了该工具中六种应用的使用方法、常见问题及其解决方案，为读者提供了从基础学习到高级应用的学习之路。 全书内容分为三个部分：第1至6章深入探讨了形式化验证的优势、基础原理以及编程语言的语法规则；第7至12章首先对比介绍了三大EDA厂商提供的形式化验证工具集，随后给出六种形式化验证工具的实战部分，详细阐述了每种工具的用途、流程、使用方法和关键问题解决策略；第13至15章则聚焦于形式化验证的高级技术，包括形式化验证的关键技术—如何简化设计，以及如何通过自动化脚本和复用仿真环境的约束和检查器来提高验证的效率等。本书旨在帮助广大的IC工程师和学生快速入门和实践形
|
| 內容簡介： |
|
本书系统介绍了形式化验证的概念和原理，并通过丰富的实例生动展示了形式化验证所需的TCL和SVA语言语法规则，同时揭示了其在商业上的潜在价值和广阔前景。书中以目前广泛采用的RISC-V架构为例，借助新思科技的VC Formal形式化验证工具，深入浅出地讲解了各种形式化验证应用的流程、使用方法以及常见陷阱，为读者提供了从基础知识到高级应用的学习途径。 本书包括三个部分： ? 基础篇（第1～6章），主要介绍形式化验证的工具、语言和设计； ? 实战篇（第7～13章），主要展示相关工具的使用方法、常见问题以及对应的解决方案； ? 进阶篇（第14～17章），主要探讨简化、签核和加速等关键形式化验证技术。 本书不仅适合芯片设计和开发领域的从业人员快速入门和实践形式化验证，也可以作为电子工程等相关专业的教学参考书。
|
| 關於作者： |
|
王亮IC工程师，2008年毕业于西北工业大学计算机系统结构专业，拥有接近20年的芯片行业工作经验，先后就职于S3 Graphics（VIA，2年）、艾萨华科技（LSI，6年）、超微半导体（AMD，9年），目前就职于AMD GPU部门做GPU验证工作。谭永亮IC设计工程师，2008年研究生毕业于西北工业大学电路与系统专业，拥有接近20年的工作经验，目前就职于某IC创业公司，担任芯片设计经理。
|
| 目錄：
|
|
目 录推荐序前言基础篇第1章 芯片验证 21.1 什么是芯片验证 21.2 芯片验证的种类和过程 31.3 验证的现状 51.4 本章小结 7第2章 验证策略概述 82.1 动态验证 92.1.1 EDA仿真 92.1.2 硬件仿真 112.1.3 FPGA原型验证 132.1.4 三种动态验证方式的比较 142.2 静态检查 152.2.1 语法语义检查 152.2.2 形式化验证 152.3 形式化验证和动态验证的优缺点对比 192.4 形式化验证的现状和商业价值 212.5 学习形式化验证能做什么 262.6 本章小结 27第3章 形式化验证基本原理和算法 283.1 形式化验证概述 283.1.1 等价性验证 283.1.2 模型检查 323.1.3 定理证明 323.2 硬件电路的形式化验证原理 333.3 二叉决策图概述 343.3.1 二叉决策图原理 343.3.2 有序二叉决策图 363.3.3 精简有序二叉决策图 363.3.4 BDD的不足 383.4 基于SAT的形式化验证 383.4.1 SAT原理 383.4.2 有界模型检查问题 403.5 BDD和SAT的比较 423.6 本章小结 42第4章 形式化验证的流程和方法 434.1 形式化验证“三板斧”——语言、工具和设计 434.1.1 语言 444.1.2 工具 444.1.3 设计 444.2 形式化验证相关的重要概念 454.2.1 安全属性和活性属性 454.2.2 断言的反例 454.2.3 有界证明和有界证明深度 454.2.4 过约束与欠约束 464.2.5 假成功 464.2.6 简化 474.3 形式化验证规划 484.3.1 形式化验证工具的适用场景 484.3.2 时序等价性检查的适用场景 494.3.3 不可达检查的适用场景 504.3.4 连接性检查的适用场景 504.3.5 X态传播检查的适用场景 504.4 形式化验证流程 514.4.1 验证计划 524.4.2 搭建验证平台 534.4.3 调试迭代 544.4.4 收集覆盖率和断言证出率 554.4.5 签核 554.5 形式化验证示例——定时器 554.5.1 定时器设计概述 564.5.2 定时器验证计划 594.5.3 定时器形式化验证过程 604.5.4 定时器形式化验证小结 674.6 本章小结 68第5章 形式化验证断言语言 695.1 断言概述 695.1.1 什么是断言 695.1.2 为什么用断言 695.1.3 如何实现断言 705.2 断言语言SVA 735.2.1 断言结构及分类 735.2.2 序列 765.2.3 蕴含操作符 765.2.4 延时 785.2.5 SVA系统函数 795.2.6 重复操作符 805.2.7 disable iff 825.2.8 s_eventually 825.2.9 序列操作符 835.2.10 参数化 865.2.11 局部变量 865.2.12 合入断言的方式 875.2.13 多时钟 885.3 基于断言的设计 885.3.1 X态检查 895.3.2 独热码检查 895.3.3 格雷码检查 905.3.4 计数器溢出检查 905.3.5 仲裁器检查 905.3.6 先进先出队列 915.3.7 数据完整性检查 925.3.8 死锁检查 925.4 对形式化验证友好的SVA代码风格 925.5 本章小结 93第6章 形式化验证工具命令语言 946.1 TCL简介及其在IC中的应用 946.2 TCL高频语法 956.2.1 TCL例程 966.2.2 TCL数据类型和基础操作 976.2.3 TCL分支和循环等控制流操作 1076.2.4 TCL子程序、命名空间 1096.2.5 TCL文件操作 1116.2.6 TCL正则表达式 1136.3 本章小结 115实战篇第7章 形式化验证工具介绍 1187.1 概述 1187.2 新思科技的VC Formal 1197.3 楷登电子的JasperGold 1207.4 西门子的Questa Formal 1217.5 工具的对标比较 1217.6 本章小结 124第8章 形式化属性验证——FPV 1258.1 基于RISC-V的微型SoC 1258.1.1 RISC-V SoC的特性列表 1258.1.2 RISC-V SoC的设计框图 1268.1.3 RISC-V SoC的顶层接口 1278.1.4 RISC-V SoC的地址映射 1278.1.5 RISC-V SoC概述 1288.1.6 Wishbone总线概述 1318.1.7 RISC-V SoC各个子模块的功能 1348.2 RISC-V SoC的FPV验证计划 1378.2.1 验证策略和验证对象功能规范 1378.2.2 形式化验证平台描述 1378.2.3 验证对象的断言规则描述 1388.3 FPV和RISC-V SoC验证平台 1448.4 验证平台搭建和常见问题集锦 1468.4.1 常见问题一：TCL脚本中没有指定正确的复位信号 1468.4.2 常见问题二：错误的约束导致前置条件不成立 1478.4.3 常见问题三：个别标准单元没有Verilog模型，导致被黑盒化，功能和预期不符 1488.4.4 常见问题四：约束有冲突，导致运行终止并报错 1498.4.5 常见问题五：内部子模块使用的复位信号不是顶层指定的复位信号，导致断言失败 1508.4.6 常见问题六：约束的SVA语法有误，导致约束“不符合预期” 1508.4.7 其他常见问题 1518.5 RISC-V SoC的验证过程和结果 1528.5.1 形式化验证重要建议——加入覆盖属性 1528.5.2 RISC-V SoC形式化验证发现的RTL缺陷和断言缺陷 1548.5.3 形式化验证只能发现RTL缺陷吗 1618.5.4 约束、断言和覆盖属性的实现方式 1628.6 本章小结 163第9章 时序等价性检查 1649.1 时序等价性检查应用场景 1659.1.1 门控时钟插入验证 1659.1.2 不改变功能的功耗优化验证 1669.1.3 重新切割流水线和时序优化验证 1679.1.4 删除某个不需要的特性或者删除一些冗余代码 1679.1.5 新增功能不影响原有功能 1689.1.6 工程变更命令相关验证 1689.1.7 硬编码到参数化的设计改动验证 1689.1.8 寄存器从带复位的改成不带复位的 1699.1.9 在可测性设计使能扫描模式下，确保X态不会传播到下游逻辑 1699.2 验证环境和脚本流程 1709.3 时序面积优化验证示例 1729.3.1 流水线级数不变的多位数据按位异或设计 1729.3.2 32位加法器从一级增加到两级流水线 1749.4 RISC-V SoC门控时钟案例 1759.5 使用SEQ工具验证的常见问题 1789.5.1 使用SystemVerilog语法中的bind操作错误 1789.5.2 真正的设计缺陷 1799.6 简化和签核 1819.7 本章小结 184第10章 不可达检查 18710.1 什么是不可达检查 18710.2 常见的代码覆盖率的种类 18810.3 常见的不可达的场景 18810.3.1 信号值固定 18910.3.2 某些功能的禁用导致不可达 18910.3.3 RTL存在冗余代码 19010.3.4 RTL中信号存在多余位 19010.3.5 信号之间存在依赖关系导致不可达 19110.3.6 RTL代码本身存在缺陷导致不可达 19110.4 不可达检查流程 19210.5 不可达检查的使用阶段 19310.5.1 早期验证阶段 19310.5.2 动态仿真测试平台可用阶段 19310.5.3 动态仿真测试平台成熟阶段 19410.6 不可达检查实例 19410.6.1 不读入覆盖率数据库的RISC-V SoC的不可达检查 19410.6.2 动态仿真的覆盖率结果 19510.6.3 读入覆盖率数据库文件的不可达检查 19610.6.4 动态仿真和形式化验证合并的覆盖率结果 19610.6.5 子模块的不可达检查结果合并 19710.7 本章小结 197第11章 连接性检查 19811.1 连接性检查概述 19811.2 连接性检查方法学 20011.3 基本流程示例 20211.4 实例——RISC-V SoC的连接性检查 20211.4.1 RISC-V SoC的设计规范 20211.4.2 连接规范对应的电路 20311.4.3 表格形式的连接规范 20511.4.4 检查结果 20611.5 本章小结 207第12章 X态传播检查 20812.1 什么是X态传播 20812.2 形式化X态传播检查工具的用途 21012.3 实例——RISC-V SoC的X态传播检查 21112.3.1 RISC-V SoC的X态传播分析 21112.3.2 RISC-V SoC的X态传播检查流程 21312.3.3 RISC-V SoC的TCL脚本及运行结果 21312.4 本章小结 214第13章 事务级等价性检查 21513.1 为什么使用事务级等价性检查 21713.2 DPV流程和示例 21713.3 DPV实践 21913.4 本章小结 220进阶篇第14章 形式化验证关键技术——简化 22214.1 形式化验证的复杂度问题 22414.2 复杂度简化策略 22514.2.1 初始值简化 22514.2.2 合理的过约束 22614.2.3 断开设计中的某个信号 22714.2.4 黑盒化 22814.2.5 压缩设计单元大小 22914.2.6 分治法 23114.2.7 使用简化模型 23214.2.8 使用符号变量、局部变量或者加辅助代码 23314.3 常见单元的简化示例 23714.3.1 计数器的简化 23714.3.2 存储器的简化 24214.4 本章小结 243第15章 形式化验证签核 24415.1 形式化验证签核概述 24415.2 形式化验证签核的要素 24615.2.1 断言 24615.2.2 约束 24615.2.3 复杂度 24715.2.4 覆盖率 24815.3 形式化验证签核的流程 25115.3.1 计划阶段 25115.3.2 验证平台编写阶段 25215.3.3 回归阶段 25315.3.4 签核阶段 25515.4 形式化验证签核的挑战 25515.5 本章小结 256第16章 形式化验证加速 25716.1 复用AIP或断言库 25816.1.1 使用EDA厂商提供的AIP 25916.1.2 自研AIP——Valid-Ready协议 26016.1.3 断言库 26416.2 开发自动化脚本 26516.3 最大化利用机器资源 26616.3.1 使用形式化验证工具提供的拆分任务的命令 26616.3.2 使用形式化验证工具提供的AI加速命令 26616.3.3 选择引擎 26716.4 本章小结 267第17章 形式化验证的道与术 26817.1 形式化验证的道、法、术、器 26817.1.1 道 26917.1.2 法 26917.1.3 术 26917.1.4 器 27017.2 形式化验证与动态仿真融合 27017.2.1 区分形式化验证和动态仿真的模块 27017.2.2 合理规划形式化验证的应用程序 27117.2.3 复用断言和约束 27117.2.4 动态仿真和形式化验证融合，加速覆盖率收敛 27217.2.5 回片后的调试 27417.3 如何解决形式化验证遇到的问题 27517.3.1 不理解设计 27517.3.2 工具使用问题 27617.3.3 断言语法问题 27617.3.4 不确定断言是否生效 27617.3.5 运行结果与预期不一致 27717.3.6 无法完全证明 27717.4 形式化验证的三重境界 27717.5 本章小结 278附录 代码包的目录及说明 280技术术语表 281参考文献 285
|
| 內容試閱：
|
|
前 言我在2008年获得计算机系统结构硕士学位后，加入集成电路（Integrated Circuit，IC）公司参与芯片设计工作，也是从那时候开始，芯片验证就始终伴随着我的工作，这也印证了芯片行业内的共识——设计验证不分家。验证技术目前有两种主流方式：动态验证（Dynamic Verification）和形式化验证（Formal Verification，FV）。动态验证主要包括EDA仿真、硬件加速器仿真和FPGA原型验证三种方式，目前阐述动态验证的书籍已经琳琅满目，但是有关形式化验证的书籍却凤毛麟角，国内出版的参考书更几乎是空白。所以，我通过市场调研，萌发了总结归纳自己在芯片行业十几年的工作经验和技术积累的想法，并通过编著成书的形式分享给读者，方便读者快速入门、学习参考。在我十几年的从业经历中，接触过很多验证方法学和验证语言。从最早的基于Verilog硬件描述语言搭建的验证平台，到后来的基于验证方法指南（Verification Methodology Manual，VMM）的验证平台，直到三大电子设计自动化（Electronic Design Automation，EDA）厂商对芯片验证统一采用通用验证方法学（Universal Verification Methodology，UVM）；从基于C语言参考模型打印输出和寄存器传输级（Register Transaction Level，RTL）仿真打印输出的非实时对比，到使用SystemVerilog语言的直接编程语言接口（Direct Programming Interface，DPI）进行实时动态激励对比；从基于属性规范语言（Property Specification Language，PSL）到基于SystemVerilog断言（SystemVerilog Assertion，SVA），验证语言、方法和技术一直在更新演进。奈何几乎在我参与的每个项目中都有或大或小的缺陷，所以芯片验证其实很难说有“验证完毕”的时候，业内也有“验证无止境”的说法，即验证是项目进度和资源的平衡。动态验证已经在工程中被广泛应用，但是它无法遍历所有的合法状态空间，可能会漏掉一些测试场景，导致缺陷未能被发现，而形式化验证以其独有的原理和策略，对动态验证做了很好的补充。它利用数学分析方法，对目标电路建立模型，然后通过算法引擎对待测设计的状态空间进行穷尽式的验证。相比于动态验证，形式化验证属于静态验证（Static Verification），它主要有以下优势：1）能覆盖待测设计的完整状态空间，不会漏掉边角场景（业内称为Corner Case）。2）无须产生复杂的验证平台（Test Bench，TB），只需要约束和断言即可，因此建立TB的速度快。3）运行时间短，有利于尽早尽快地改正设计中的缺陷，缩短验证周期。目前，形式化验证已经广泛用于各大IC公司，如Intel、AMD和NVIDIA等，但在行业内，这方面的参考书籍还很缺乏。我在形式化验证的实践过程中，只能硬着头皮查手册，花费大量时间尝试不同方法，内心忐忑地请教其他组的同事，一路上磕磕碰碰，问题一个接一个地出现，就像是翻不完的山、趟不完的河，一路上记录问题并寻找解决方法，最终按照项目节点完成了一个个验证任务。我常常想，如果当初有一本书能把形式化验证的方方面面展示出来，那么我也就不需要走那么多弯路了。但是长期以来，市面上也没有这样的中文书籍。我不知道此时此刻有多少IC工程师被FV的问题卡住，我觉得我应该做些什么。我一直热爱分享，渴望把自己的经验分享给大家，如果能够让大家少走弯路，提高验证效率和质量，我将会倍感幸福，也会觉得做了一件有意义的事情。本书分成三个部分：1）基础篇（第1～6章）。2）实战篇（第7～13章）。3）进阶篇（第14～17章）。读者可以根据自己的水平来选择相应的章节阅读。对于学生或者入门者，由于没有太多经验，建议从头到尾阅读；对于芯片设计或者验证工程师，由于有项目经验，但没有接触过形式化验证，可以首先阅读基础篇的第1～6章，然后跳到实战篇开始用实际例子学习；对于已经有一定的形式化验证基础，想要提高验证工作质量和效率的读者，可以直接阅读本书的进阶篇。在我萌生编著本书的想法之后，多亏了教研室师兄安建峰帮我牵线机械工业出版社。所以首先感谢安建峰师兄和机械工业出版社给予我的帮助，没有他们的帮助就没有本书的出版。衷心感谢新思科技在技术和形式化验证工具的使用上提供的大力支持。新思科技VC Formal产品总监张劲博士审阅了书稿，细心纠错，并提出了很多宝贵的建议；高级工程师Sai Karthik Madabhushi审阅和修订了书中相关的形式化验证脚本；高级工程师Siddarth Papineni和R&D工程师Luke Hassell耐心地帮我解决烦琐的IT问题。他们的专业和敬业精神令人感动和敬佩。感谢我在上海工作时的领导和同事，尤其是Jeffrey Wang，在我做形式化验证工作遇到困难的时候，他总是热情地解答我的问题，三言两语点醒“梦中人”感谢Wenmin Lin、Chris Liu、Zhiwei Li和Yin Huang等，谢谢他们对我的验证工作的支持；感谢Prosper Chen审阅书稿，使得本书得以通过公司的保密审核流程；感谢郭向东在休假期间也耐心地解答我的技术问题。最后还要感谢我的家人。感谢母亲，她的拼搏、勤劳、刚强、克勤克俭的精神时刻影响着我，让我这个平凡的人也有了出书的勇气；感谢公公婆婆做好了所有的后勤工作；感谢我志同道合的爱人谭永亮和我共同完成了此书；感谢我的儿女们，他们永远是我快乐的源泉和奋斗的动力！热切希望本书能够帮助广大读者掌握形式化验证技术。随书附赠的代码包中的示例代码都经过了验证，读者可以通过访问https://solvnetplus.synopsys.com/s/article/VC-Formal-examples-for-the-book-Formal-Verification-for-IC-Designs-Principles-and-Practice来下载学习。本书附录给出了该代码包的目录结构和内容说明。由于作者水平有限，书中的疏漏之处在所难免，敬请广大读者批评指正（联系邮箱：fv_book@163.com）。王亮
|
|
購物車/收銀台(0) | 在線留言板
| 付款方式
| 運費計算
| 聯絡我們
| 幫助中心 |
加入書簽
HOME
新書上架
