书名：形式化验证：现代VLSI设计的必备工具包（原书第2版）
定价：129.0
ISBN：9787111796565
作者：[美]埃里克·塞利格曼（Erik Seligman）[美]汤姆·舒伯特（Tom
版次：1
出版时间：2026-01

内容提要：

《形式化验证：现代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