《形式化验证：现代VLSI设计的必备工具包（原书第2版）》全面介绍了数字电路设计与验证的实用方法，结合丰富的工程实践经验，帮助读者将先进的验证技术有效融入实际工作。形式化验证（Formal Verification，FV）作为一种以数学方法直接分析寄存器传输级（RTL）设计特性与质量的技术，能够显著缩短验证周期，加速设计收敛，提升产品可靠性。
以 SystemVerilog 为基础，本书深入讲解了FV的核心原理与工程实践，揭示了其在英特尔等国际领先企业设计流程中的成功应用。通过阅读本书，读者将掌握在实际项目中引入并高效部署 FV 技术的系统方法，从而显著提升设计与验证效率。

译者序
第2版序
第1版序
致谢
第1章　形式化验证（FV）：从梦想到现实 1
1.1　FV是什么 2
1.2　为什么是这本书 3
1.3　一个鼓舞人心的轶事 3
1.4　FV：更深层次 5
1.4.1　FV的整体优势 5
1.4.2　FV的一般使用模型 6
1.4.3　完整覆盖的FV 6
1.4.4　本书未讨论的FV方法 9
1.5　实用FV的出现 10
1.5.1　早期自动推理 11
1.5.2　计算机科学应用 11
1.5.3　模型检查变得切实可用 11
1.5.4　断言的标准化 12
1.6　实施FV的挑战 13
1.6.1　数学的基本局限性 13
1.6.2　复杂性理论 13
1.6.3　好消息 14
1.7　增强形式化的力量 15
1.8　充分利用这本书 16
1.9　本章实用建议 17
进一步阅读 17
第2章　基础形式化验证（FV）算法 19
2.1　验证过程中的FV 19
2.2　一个简单的自动售货机示例 20
2.3　模型比较 22
2.4　影响锥 23
2.5　规范操作定义 24
2.5.1　智能构建真值表 24
2.5.2　添加顺序逻辑 24
2.6　布尔代数符号 25
2.6.1　布尔代数基本定律 26
2.6.2　规范比较 27
2.7　二元决策图（BDD） 28
2.7.1　计算电路设计的 BDD 30
2.7.2　使用BDD进行模型检查 30
2.8　布尔可满足性（SAT） 31
2.8.1　有界模型检查 32
2.8.2　解决SAT问题 32
2.8.3　Davis-Putnam SAT 算法 34
2.8.4　Davis-Logemann-Loveland SAT 算法 35
2.9　总结 36
进一步阅读 37
第3章　SystemVerilog断言简介 38
3.1　基本断言概念 38
3.1.1　一个简易仲裁器实例 39
3.1.2　断言是什么 39
3.1.3　假设是什么 40
3.1.4　覆盖属性是什么 40
3.1.5　断言语句的说明 41
3.1.6　SVA语言基础 41
3.1.7　即时断言 42
3.1.8　编写即时断言 43
3.1.9　过程代码的复杂性及采用assert final的动机 44
3.1.10　过程块中的位置 45
3.1.11　布尔构建块 46
3.1.12　并发断言基础和时钟控制 46
3.1.13　采样和断言时钟 47
3.1.14　采样值函数 48
3.1.15　并发断言的时钟边沿 49
3.1.16　并发断言的重置（禁用）条件 50
3.1.17　设置默认时钟和重置 51
3.2　序列、属性和并发断言 53
3.2.1　序列语法和示例 53
3.2.2　属性语法和示例 56
3.2.3　命名序列和属性 60
3.2.4　断言和隐式多线程 60
3.2.5　常量的挑战 61
3.2.6　编写属性 62
3.3　总结 68
3.4　本章实用建议 69
进一步阅读 70
第4章　形式化属性验证（FPV） 72
4.1　什么是FPV 72
4.2　本章示例：组合锁 75
4.3　搭建基础的FPV环境 76
4.3.1　编译RTL 77
4.3.2　创建覆盖属性 77
4.3.3　创建假设 78
4.3.4　创建断言 79
4.3.5　时钟和复位 81
4.3.6　运行验证 81
4.4　FPV与仿真有何不同 86
4.4.1　可以运行哪些类型和规模的模型 87
4.4.2　如何达到目标行为 88
4.4.3　检查哪些值 89
4.4.4　我们如何约束模型 89
4.4.5　如何处理内部节点的约束 90
4.4.6　我们用什么进行调试 91
4.4.7　典型轨迹有多长 92
4.5　决定在哪里以及如何运行FPV 92
4.5.1　运行FPV的动机 92
4.5.2　使用设计探索FPV 93
4.5.3　使用错误搜索FPV 94
4.5.4　使用签核级FPV 94
4.5.5　使用特定应用FPV 95
4.6　总结 96
4.7　本章实用建议 97
进一步阅读 98
第5章　用于设计探索的有效形式化属性验证（FPV）99
5.1　本章示例：交通灯控制器 100
5.2　创建设计探索计划 103
5.2.1　设计探索目标 103
5.2.2　设计探索的主要属性 104
5.2.3　复杂性分级计划 105
5.2.4　退出标准 108
5.2.5　整合计划 108
5.3　设置设计探索FPV环境 109
5.3.1　覆盖属性 109
5.3.2　假设 110
5.3.3　断言 110
5.3.4　时钟和复位 111
5.3.5　健全性（sanity）检查 111
5.4　波形调试迭代（wiggling）设计 112
5.4.1　wiggling过程 112
5.4.2　wiggling阶段1：我们的第一个短波形 113
5.4.3　调试另一个短波形 114
5.5　探索更关键的行为 117
5.5.1　回答一些新问题 117
5.5.2　证明断言 120
5.6　移除简化并探索更多行为 122
5.6.1　面对复杂性问题 124
5.7　总结 125
5.8　本章实用建议 126
进一步阅读 127
第6章　有效形式化属性验证（FPV） 128
6.1　确定FPV目标 129
6.1.1　错误搜索FPV 131
6.1.2　签核级FPV 132
6.2　FPV工作的分阶段进行 132
6.3　本章示例：简单的ALU 133
6.4　理解设计 135
6.5　FPV验证计划的制定 137
6.5.1　FPV目标 137
6.5.2　FPV主要属性 137
6.5.3　处理复杂性 140
6.5.4　质量检查与退出标准 143
6.5.5　初始覆盖属性 148
6.5.6　扩展wiggling 149
6.5.7　扩展覆盖属性 154
6.6　去除简化和探索更多行为 154
6.6.1　演进到签核级FPV 155
6.7　总结 156
6.8　本章实用建议 156
进一步阅读 158
第7章　针对特定问题的形式化属性验证（FPV）APP 159
7.1　可重用协议验证 160
7.1.1　可重用属性集的基本设计 161
7.1.2　属性方向问题 162
7.1.3　验证属性集一致性 164
7.1.4　完整性检查 166
7.1.5　动态验证兼容性 167
7.2　不可达覆盖消除 167
7.2.1　在UCE中使用断言的作用 168
7.2.2　覆盖组和其他覆盖类型 170
7.3　连通性验证 170
7.3.1　连通性模型构建 171
7.3.2　指定连通性 172
7.3.3　可能的连通性FPV复杂性 173
7.3.4　连通性FPV的覆盖率 175
7.4　控制寄存器验证 176
7.4.1　指定控制寄存器要求 177
7.4.2　控制寄存器的SVA 178
7.4.3　控制寄存器验证的主要挑战 180
7.5　硅后调试和反应性FPV 182
7.5.1　硅后FPV的挑战 183
7.5.2　UNEARTH：一种实用的硅后FPV方法 183
7.6　总结 190
7.7　本章实用建议 190
进一步阅读 192
第8章　形式化等价性验证（FEV） 194
8.1　等价性检查的类型 195
8.1.1　组合等价性 195
8.1.2　顺序等价性 197
8.1.3　事务级等价性 197
8.2　FEV用例 199
8.2.1　RTL到网表FEV 199
8.2.2　网表到网表FEV 200
8.2.3　RTL到RTL FEV 200
8.3　运行FEV 205
8.3.1　选择模型 205
8.3.2　关键点选择和映射 206
8.3.3　假设和约束 211
8.3.4　调试不匹配 212
8.4　额外的FEV挑战 213
8.4.1　状态元素优化 213
8.4.2　条件等价性 214
8.4.3　不关心空间 215
8.4.4　复杂性 216
8.5　总结 221
8.6　本章实用建议 222
进一步阅读 224
第9章　形式化验证最大的失误：误报的危险 226
9.1　滥用 SVA 语言 228
9.1.1　缺少分号 228
9.1.2　两个时钟边沿均置位 229
9.1.3　带断言的短路函数 229
9.1.4　信号采样的微妙影响 230
9.1.5　非生命状态的活性属性 231
9.1.6　错误地假设一个序列 232
9.1.7　预防与 SVA 相关的误报 232
9.2　空洞问题 233
9.2.1　误导性的覆盖属性与糟糕的重置 234
9.2.2　经过验证但模拟失败的内存控制器 234
9.2.3　假设与约束的矛盾 235
9.2.4　队列永远不会满，因为它永远不会开始 236
9.2.5　防止空洞工具和用户的责任 238
9.3　隐含或未说明的假设 240
9.3.1　具有实施假设的库 240
9.3.2　对多重驱动信号的期望 241
9.3.3　无法到达的逻辑元素：需要吗 242
9.3.4　防止误解 243
9.4　分工 244
9.4.1　胶合逻辑缺失 244
9.4.2　缺失案例的拆分 244
9.4.3　撤销临时黑客攻击 245
9.4.4　安全分工 245
9.5　总结 246
9.6　本章实用建议 247
进一步阅读 248
第10章　应对复杂性 249
10.1　设计状态和相关复杂性 249
10.2　本章示例：内存控制器 251
10.3　观察复杂性问题 252
10.4　简单的收敛技术 253
10.4.1　选择正确的战斗 253
10.4.2　时钟和复位 254
10.4.3　引擎调校 255
10.4.4　黑盒化 255
10.4.5　参数和尺寸减小 256
10.4.6　案例拆分 257
10.4.7　硬案例与软案例拆分 258
10.4.8　属性简化 259
10.4.9　切点 261
10.4.10　增量FEV 263
10.5　辅助假设与非辅助假设 264
10.5.1　编写自定义辅助假设 264
10.5.2　利用已证实的断言 265
10.5.3　您是否有太多的假设 266
10.6　使用自由变量进行概括分析 267
10.6.1　利用刚性自由变量的对称性 267
10.6.2　自由变量的其他用途 268
10.6.3　自由变量的缺点 268
10.7　降低复杂性的抽象模型 269
10.7.1　反抽象 269
10.7.2　序列抽象 271
10.7.3　内存抽象 272
10.7.4　影子模型 274
10.8　半形式化验证 275
10.9　规避复杂性问题：设计和验证协同工作 277
10.10　总结 277
10.11　本章的实用建议 278
进一步阅读 280
第11章　实际项目中的形式化签核 282
11.1　整体签核方法论 282
11.2　规划和架构 283
11.2.1　分治法识别DUT 284
11.2.2　审查设计流程 284
11.2.3　选择应用程序 285
11.2.4　定义FPV细节 285
11.2.5　填补空白 286
11.2.6　制定应急计划 286
11.2.7　FV融入设计节点中 287
11.3　应用和实施 289
11.3.1　确保定期进展 289
11.3.2　做好应对反应性FV的准备 290
11.4　覆盖和回归 290
11.4.1　代码覆盖 290
11.4.2　覆盖属性 291
11.4.3　FV回归 291
11.4.4　机器学习和回归 292
11.4.5　网络与云端运行 293
11.4.6　晚期重检 293
11.5　跟踪和结束 293
11.5.1　FV的质量 293
11.5.2　时间线跟踪 295
11.5.3　验证何时才算完成 295
11.6　总结 296
11.7　本章实用建议 296
第12章　全新的具有FV风格的生活方式 298
12.1　使用FV 299
12.1.1　设计探索 299
12.1.2　错误搜索FPV 299
12.1.3　签核级FV 300
12.1.4　专用的FV应用程序 300
12.1.5　形式化等价性验证 300
12.2　个人使用FV的准备 301
12.3　启动团队的FV工作 302
12.3.1　设定合理的期望 302
12.3.2　培养“领军人物” 303
12.3.3　争取各级的支持 304
12.3.4　合理跟踪FV的进展 305
12.3.5　建立高效的基础设施 307
12.4　使管理层开心 308
12.4.1　ROI计算 308
12.4.2　错误复杂性排名 310
12.5　FV工作者实际做了什么 311
12.6　总结 313
12.7　本章实用建议 314
进一步阅读 314

第2版序

当Erik Seligman在2014年与我联系，提到他正在与Tom Shubert和M. V. Achutha Kiran Kumar合作编写一本关于形式化验证的书时，我感到非常兴奋。多年来，我曾在各种会议和活动中与这些作者互动，我们都对先进的功能验证技术充满热情。事实上，在我看来，准确地将形式化验证应用于项目中的第1版书籍的出版时间恰到好处。我坚信，这在今天甚至更为成立，因此，我由衷地欢迎第2版的出版。
多年来，我们的行业面临着许多由不断增加的复杂性带来的挑战。我还记得1997年，半导体制造技术战略联盟（SEMATECH）在行业中拉响了警报，警告说IC制造的生产力增益以40%的年均复合增长率增加，而IC设计的生产力增益只增长了20%的年均复合增长率。这个问题在1999年的《国际半导体技术路线图》报告中也得到了重申。尽管有关于硅容量与设计能力之间差距的警报，但该行业避免了危机。为什么？是由于两个主要因素防止了设计生产力差距的发生：①不断改进的设计自动化；②引发了一个生产力设计复用策略的硅IP经济的出现。
在过去的十年里，关于验证方面出现了更为严峻的生产力差距。虽然硅复杂性以摩尔定律的速度增长，但验证复杂性却以双指数速度增长，而用来填补设计生产力差距的方法将不足以填补验证生产力差距。国际商业战略公司（IBS）在2022年《设计活动和战略影响报告》中量化了当今验证差距对 IC 项目验证和确认成本与减小工艺节点特征尺寸的影响。一个“先进”的28nm IC设计的平均验证和确认成本约为1800万美元，而一个3nm IC设计的验证和确认成本约为1.68亿美元。
其他行业研究还衡量了验证生产力差距对IC项目的影响，如2022年威尔逊研究集团的功能验证研究。例如，尽管自2007年以来出现了多次摩尔定律的迭代，但一个项目中设计工程师的平均峰值人数仅增加了50%，而验证工程师的平均峰值人数却增加了令人震惊的147%。事实上，如今在ASIC/IC项目上平均有更多的验证工程师在工作，而不是设计工程师。然而，即使在项目人数增加的情况下，76%的ASIC/IC项目经历了一个或多个重新设计，而84%的FPGA项目在生产中经历了一个或多个非常规的错误逃逸。此外，三分之二的ASIC/IC和FPGA项目都没有按原计划完成。显然，我们正面临着一个需要以新的思维方式看待我们现有方法的验证危机。
与可能通过正确的输入序列来演示错误的模拟不同，形式化验证承诺在数学上证明错误的缺失。然而，仅有36%的ASIC项目采用了形式化属性检查。这并不是因为没有尝试过。事实上，根本问题是行业内缺乏在应用形式化属性检查时实现投资收益最大化所需的技能。从很多方面来看，它与先进的模拟技术没有什么不同。如果我提议一位项目经理采用受限制的随机、覆盖驱动的模拟方法，问题是，他们会成功吗？答案是否定的，直到企业部门发展了其成熟的面向对象的编程和覆盖建模技能。形式化属性检查也是如此。这就是我为什么对《形式化验证：现代VLSI设计的必备工具包（原书第2版）》感到兴奋的原因。这是我见过的最全面的一本书，涵盖了成功将形式化属性检查整合到项目的整体验证流程中所需的流程和技能。
对于任何寻求提升其形式化验证科学和实践技能的人来说，这本书是必读的。我予以最高推荐。


Harry Foster　　
西门子电子设计自动化部门首席科学家　　
曾任设计自动化大会（DAC）主席　　
威尔逊研究集团功能验证研究的创始人　　




第1版序

复杂的超大规模集成电路（VLSI）设计已经渗透到现代生活的方方面面。我们对于手机、防抱死制动系统、网络服务器等技术的存在不加思考地视为理所当然。作为用户或顾客，我们还理所当然地认为这些设备会正常运行。未被察觉的功能性故障的影响从轻微的烦恼到重大的灾难都可能发生，其潜在的成本，不论是对个人、公司还是整个社会，都可能是巨大的。以1994年英特尔的Pentium®“FDIV”错误为例，这一错误导致英特尔公司损失4.75亿美元，用于承担替换有缺陷的中央处理器（CPU）的成本。
未被察觉的功能性故障的危险性因半导体工艺技术不懈的进步（摩尔定律）而加剧，后者使我们能够将越来越复杂的设计放入单片硅芯片中。随着这种复杂性的增加，出现了越来越多的错误，这些错误需要在设计能够符合生产使用的要求之前被发现并修复。随着设计周期缩短和市场竞争压力增加，验证现在成为通向生产的关键路径。2011年《国际半导体技术路线图》的作者们将验证描述为“一个已经达到危机规模的瓶颈”。
传统的动态测试方法用于设计验证，步骤包括：
1.在整个设计或部分设计周围创建一个验证封装器或测试平台（testbench）。
2.编写专门的测试或生成有指向性的随机测试以激励设计。
3.在设计的可执行软件模型上运行这些测试[通常编写在寄存器传输级（RTL）]。
4.调试产生的所有故障，修复有问题的组件（无论是RTL、测试平台还是测试本身），然后重新运行测试直到设计“干净”。
然而，这种方法存在一些缺点：
1.测试平台的开发可能需要很长时间，对于复杂的设计来说，通常需要数月时间。
2.测试平台的开发是一个容易出错的活动，往往会产生与实际RTL中存在的错误数量相等或更多的测试平台中的错误。
3.测试执行是一项昂贵的工作，英特尔投入了成千上万台高性能计算服务器来运行这个问题，全天候运行，还有专用的仿真硬件和基于FPGA的解决方案。
4.测试本身可能包含错误，这些错误可能掩盖RTL中的问题（假阳性），或错误地指示实际上并不存在的错误（假阴性）。
5.失败测试的调试是一个主要的工作量消耗，通常是验证工作量中最大的单一组成部分，部分原因是故障通常是在发生点之后很长时间才被检测到。
6.通常很难判断设计的多少部分被任何给定的一组测试所覆盖，所以即使所有测试都通过，设计是否真的“干净”仍然不清楚。
7.通过动态测试进行错误检测是一个固有的顺序过程，通常被称为“剥洋葱”，因为错误可能隐藏在其他错误后面。
8.一些错误，如前面提到的Pentium®“FDIV”错误，是数据相关的，或者涉及复杂的微架构条件，很难通过RTL模型上的随机测试来找到。
形式化验证（Formal Verification，FV）作为近年来用于动态测试的替代方法，获得了广泛的认可，它更加快速、节省工作量，并且更加全面。本书的目的是解释FV是什么，为什么它至少在一定程度上提供了动态测试局限性的解决方案，以及如何、何时、何地应用它。
FV是一种强大的技术，使设计或验证工程师能够直接分析和数学化地探索RTL设计的质量或其他方面，为设计空间的大型子集提供100%的覆盖，无须创建仿真测试平台或测试矢量。在过去的20年中，它在英特尔的使用和发展一直在增长，现在越来越被认为是设计和验证的主流技术。
本书的作者从描述他们的目标开始：帮助专注于RTL的VLSI设计师和验证人员通过利用FV技术更有效、更高效地完成工作。这种方法有时被英特尔称为FV的民主化，或称为“FV适用于所有”（FV for All），意图是将FV的使用扩展到FV专家领域之外，使更多的人能够广泛地使用FV工具和技术。他们简要描述了FV的历史：早期人工智能概念如何引导了FV；对FV的理论异议以及为什么它们不是真正的阻碍问题；用于抽象问题的一般技术，以使它们对于FV更加可处理。
第2章详细描述了基本的FV算法，以充分说服读者，FV不是某种“黑魔法”，这些技术确实能够在不需要详尽（并且计算上不可行）的仿真周期的情况下实现全面的覆盖。特别是，布尔可满足性（SAT）问题得到了解释，并对能解决许多类问题的模型检查算法和工具进行了描述。
第3章介绍了SystemVerilog断言（SVA）：它们是什么（以及不同类型的SVA，如简单的布尔条件、时间断言等）以及如何将它们组合成序列和属性。
第4章在此基础上进一步介绍了形式化属性验证（Formal Property Verification，FPV）的概念：包括它的定义、与动态仿真的比较，以及其在设计探索、缺陷查找、有限验证和完备验证等方面的应用模式。
本书的核心在第5章和第6章，解释如何有效地使用FPV进行设计实践和验证。作者在将FPV应用于实际问题方面的丰富经验几乎贯穿了这两章的每一页，包括来自当前和过去的英特尔开发项目的示例，以及许多有用的提示，这将使初学者能够有效地使用FPV工具。
第7章转向描述如何使用FPV为不同的设计领域创建应用程序，例如硅后错误重现、SoC连接性检查、标准（非项目特定的）协议验证、不可达覆盖消除以及控制寄存器访问策略。这些应用程序使得没有FV背景的设计和验证工程师能够快速将FV方法应用于目标领域，而不是依赖于昂贵且耗时的动态仿真。
第8章讨论了形式化等价性验证（Formal Equivalence Verification，FEV），这是最成熟的FV技术之一，英特尔已经在许多年前内部部署了这项技术，以确保RTL与原理图匹配，从而确保RTL仿真或FV的验证结果将适用于实际硅片的功能正确性。
第9章“FV最大的失误：误报的危险”本身就值得这本书的价格。它讨论了形式化方法的一些局限性，特别是所谓的“空洞”（Vacuity）问题，即一种或一组假设排除了合法数据，从而导致了误报（缺少反例）。本章给出的示例以及避免这些现实问题的提示是非常宝贵的！
尽管FV可以提供所有这些好处，但敏锐的读者可能会想知道为什么这种技术尚未作为VLSI设计流程的一部分被广泛使用。答案是，设计复杂性以及处理它所需的容量，甚至可能超过了最好的FV工具。第10章解决了这个关键问题，首先描述了复杂性和NP完全性的一般概念，然后识别了可以用于使FV成为可处理解决方案的复杂性约简技术，如黑盒化、情况分割和属性简化。同样，作者在处理复杂的实际问题方面的经验使他们能够对看似令人生畏的问题提供实际的建议和解决方案。
第11章阐述了如何将本书描述的技术引入企业组织中，并有效地将其部署以增加设计和验证的生产力。这里再次强调的还是要解决现实问题，通过小实验来展示FPV技术的威力，获得可衡量的结果和数据，以说服怀疑者。
本书对于形式化工具和方法的资深使用者和初学者而言，都是极具价值的藏书之选。我极力推荐它。

Robert Bentley　　
英特尔FV专家中心前主任