随着数字逻辑设计的规模越来越大，复杂度越来越高，功能验证已经成为设计过程中的首要瓶颈。缩短验证时间是项目取得成功的关键。本书系统地阐述了当今最具价值的基于模拟和形式方法的验证技术，帮助测试工程师和设计工程师为每个项目选择最佳的解决方法，最快地在设计中建立起自信，并将它移植到更快的制造过程中。
　　本书作者William K. Lam是设计验证方面的世界级一流专家，书中汇聚了作者广博的实践经验，既讨论一般的测试原则，也展示具体的实践方法，有些内容还提供了伪代码形式的算法，读者只需简单地改写为具体的程序设计语言，即可上机调试。无论高校学生还是企业的验证工程师都可以从本书获益。

本书译者提供的勘误表：
http://mypage.zju.edu.cn/wangww/581846.html

无

对于一个成功的设计项目而言，有两组人员是不可或缺的：一组是设计人员，另一组是验证人员。设计人员通常受过学校的正规教育。许多学院开设关于逻辑设计的详细课程，其范围从数字设计导论一直到高等计算机体系结构。与此相反，大多数的验证工程师是从工作中学到相关技术的。虽然许多学校开始讲授验证的课程，但是很少有高等院校专门培养验证工程师。事实上，大多数验证工程师出身为设计师但逐渐转向设计验证。与设计使用的技术与方法不同，验证所需的知识广博而又组织松散，并且是通过日常的动手实践而获得。此外，验证的范围正在快速扩展：验证技术的全景图每6个月就有新技术、标准和工具出现。然而，经过时间检验并且证明是验证的奠基石的原理和技术并没有改变。
　　本书汇集并系统介绍业界常见的使用广泛的数字设计验证技术和方法，主要讨论数字逻辑设计和验证，但并不包括混合信号或射频元件电路的验证。本书的目标之一是将大量的验证知识传授给大学学生和工程师，使他们能够更好地为就业作准备，并加速他们的学习进度。写一本10分钟速成的验证工程师手册，列出可以在工作中立即可用且详细的实用诀窍是非常诱人的，但是这种救急的窍门往往很快就过时。另外一方面，只是讲解理论对于工程师来说也是非常不现实的。因此，本书在两者之间取得了平衡，不仅讨论常用的实践方法同时也提出验证的原理。作者的观点是，只有通过理解原理才能真正掌握实践的要旨，并在使用时体现出创造性。
致读者
　　本书的读者对象包括三、四年级的本科生和低年级的研究生。本书假设这些读者对一门硬件描述语言非常了解，最好是Verilog。因为Verilog语言在大多数教科书中作为描述的目的而使用。如果另外还对逻辑设计有初步了解则更好。本书是设计验证的入门教程。通过学习，学生们将会学到在基于模拟验证中使用的主要思想、工具和方法，还将学会形式验证的内在原理。本书所提供的材料是经业界测试及广泛使用的。在每章的末尾安排习题，可帮助复习章内所覆盖的知识。对于想深入了解某些专题的读者，请参考本书参考书目中所列出的资源。
　　本书的读者对象还包括拥有一些验证经验的验证工程师，这些读者也许需要系统地了解验证的不同领域并理解形式验证的基本原理。这些读者也需要掌握基本的系统设计知识和一门硬件描述语言。本书的第一部分详细描述基于模拟的验证方法，并可以作为专业验证师的复习材料或入门读物。对于大多数实践工程师而言，形式验证工具似乎是一种需要深奥的数学知识才能理解的魔术。本书对这些工具和形式验证的工作原理作了解释。在深入讨论形式验证之前，第7章介绍了为充分理解验证算法所需要的基本数学知识和计算机算法。
　　与任何技术一样，没有什么东西能取代动手的经验。这里鼓励读者通过运行本书中的一些例子和习题，或通过设计一个能使用所论述的工具的项目来认识验证工具。诸如Verilog模拟器、测试基准开发工具以及波形观察软件等自由CAD软件可以在www.verilog.net/free.html上找到。
致教师
　　本书由两部分组成。第一部分论述传统的验证策略，即基于模拟的验证；第二部分论述在学术界建立完善、并在业界已得到证实的形式验证的各个方面。这两个部分是自成一体的，可以根据需要而独立讲授。
　　第一部分描述许多验证工具。由于这些工具的专长因厂商的不同而不同，并且随着时间的推移也不同，所以本书只使用伪通用命令。为了强化学习这些工具，建议把业界的工具作为验证实验的一部分（比如，模拟器、波形观察程序、覆盖工具、错误跟踪系统和修改控制系统）。同样，为巩固形式验证的知识，应当在实验环节中使用商用的形式验证工具，比如硬件描述语言的linter程序、模型检验程序和等价检验程序。
　　本书有配套的教师手册，其内容含有每章末尾所有习题的解答。需要的教师可以填写书后面的“教学支持说明”，然后与出版社联系。
本书的组织
　　本书作为设计验证的入门书籍，仍需要读者对基本的Verilog结构有所了解。虽然本书把Verilog语言作为硬件描述语言，但还是尽量给出独立于Verilog的思想。在不可避免需要使用Verilog的地方使用最简单的Verilog结构，让不熟悉该语言的读者掌握其主要思想。
　　正如前所述，本书由两部分组成。第一部分讲解基于模拟的验证，第二部分讨论形式验证。基于模拟的验证是迄今为止应用最为广泛的方法，是对所有验证工程师的一项最低要求。形式验证则相对是一项新技术，是基于模拟验证的补充。作者相信，要最好地使用一项技术，人们必须先对该项技术内部的原理有深入的理解。因此，本书不仅在用户层次上讨论验证工具的操作（这个内容比较适于写成用户手册），还用很多篇幅讲解模拟和形式技术的基本原理。
　　第一部分模拟技术由第2～6章组成。这些章节的安排顺序与通常模拟验证过程的操作顺序相似。我们从第2章开始，对静态错误进行检测。这些错误无须输入向量即可探测出来，并且必须在更广泛的模拟开始之前消除。在第3章，我们研究模拟器的基本体系结构。首先提出事件驱动和基于周期的模拟算法，随后讨论模拟器的操作以及协同模拟、对设计的描述、常见模拟器选项和用户界面的应用。
　　在人们能开始模拟之前，必须建立一个用于系统设计的测试基准。第4章讨论测试基准设计、初始化、激励生成、时钟生成网络、错误注入、结果评估及测试配置。当某个系统设计不存在静态错误、并被嵌入一个测试基准以后，模拟即可开始。但是，应当如何模拟系统设计呢？第5章提出模拟什么以及如何度量模拟的质量。我们将考察测试规划设计、测试规划中测试项目的生成、输出响应评估、断言（特别是SystemVerilog断言）和验证覆盖。
　　在对电路进行模拟并发现错误之后，下一步就是对在模拟过程中发现的问题进行调试。第6章提出广泛使用的调试技术，包括范围压缩、检测指示、错误跟踪、踪迹转储及正向和反向调试。此外，第6章还考察系统设计的4种基本视图：RTL代码视图、图式视图、波形视图和有限状态机视图，然后考查错误修复之后的构想(scenario)。所讨论的工具和方法包括修改控制系统、回归测试机制及流片（tapeout）标准。
　　本书的第二部分形式验证由第7～9章组成。本书第一部分的若干章节可以与第二部分一起学习。比如，第2、4、5、6章也适用于形式验证。
　　理解形式验证的关键在于理解其内在的理论。第7章提供后续章节所需的基本数学背景。这些材料涵盖布尔函数及表示、对称布尔函数、有限状态机和等价算法，以及诸如深度优先搜索和宽度优先搜索、强连通分量的图算法。
　　第8章给出判定图的概况，并重点论述二叉判定图。然后学习SAT（可满足性）问题作为判定图的另一种替代方法。该章最后考察判定图和SAT问题在等价性检验和符号模拟中的应用。
　　第9章对符号模型检验进行深入研究。首先给出自动机与计算树逻辑作为模拟有公平性约束的时态行为的方法，然后讨论在一个时态规范对比下的模型检验。根据模型检验算法，给出有效的符号模型检验算法，其中的图运算通过布尔函数计算完成。接着，再次阐述对不存在一一对应的一般电路的等价性检验问题。最后，研究更有效地处理符号计算的算法。
勘误
　　如此篇幅的书籍必然包括错误和需改进之处。请将错误报告和评论发送至作者的电子邮件：williamlamemail@gmail.com。
图P1本书各章概览


致谢
　　首先和最重要的是感谢我的妻子Serene，感谢她的耐心、理解和鼓励。她的爱与支持支撑着我度过这一段漫长且孤独的旅程。我也要感谢我的母亲Grace和父亲James Lam，感谢他们一贯的指导与支持。
　　感谢所有的书评者花费宝贵的时间阅读本书的手稿，并指出错误及改进的方向。特别感谢Rajeev Alur、K.C.Chen、Thomas Dillinger、Manoj Gandhi、YuChin Hsu、Sunil Joshi、Shrenik Mehta、Vigyan Singhal、Ed Liu、Paul Tobin及John Zook对本书真知灼见的评论、建议和勉励。Verilog的自由软件的站点是Thomas Dillinger建议的。此外，非常感激Bernard Goodwin的热情与鼓励，感谢Prentice Hall出版公司编辑的敬业精神。

第1章设计验证的缘由
1.1什么是设计验证
1.2验证的基本原理
1.3验证方法学
1.3.1基于模拟的验证
1.3.2基于形式方法的验证
1.4基于模拟的验证与形式验证的比较
1.5形式验证的局限性
1.6Verilog语言调度和执行语义简介
1.6.1并发进程
1.6.2不确定性
1.6.3调度语义
1.7本章小结
第2章编写验证的代码
2.1功能正确性
2.1.1语法检查
2.1.2结构检查
2.2时序正确性
2.2.1竞争问题
2.2.2时钟选通
2.2.3时间零与零时间毛刺
2.2.4域交叉毛刺
2.3模拟的性能
2.3.1抽象的更高层次
2.3.2模拟器可识别组件
2.3.3向量与标量
2.3.4与其他模拟系统界面的最小化
2.3.5低层次/组件层次优化
2.3.6代码描述
2.4可移植性与可维护性
2.4.1项目代码布局
2.4.2集中的资源
2.4.3RTL设计文件格式
2.5可综合性、可调试性与通用工具兼容性
2.5.1可综合性
2.5.2可调试性
2.6基于周期的模拟
2.7硬件模拟/仿真
2.82状态与4状态模拟
2.9linter程序的设计与使用
2.10本章小结
2.11习题
第3章模拟器体系结构与操作
3.1编译器
3.2模拟器
3.2.1事件驱动的模拟器
3.2.2基于周期的模拟器
3.2.3混合模拟器
3.2.4硬件模拟器与仿真器
3.3模拟器的分类与比较
3.3.12状态与4状态模拟器
3.3.2零时延与单位时延模拟器
3.3.3事件驱动的模拟器与基于周期的模拟器
3.3.4解释型与编译型模拟器
3.3.5硬件模拟器
3.4模拟器的操作与应用
3.4.1基本模拟的文件结构
3.4.2性能与调试
3.4.3时序验证
3.4.4设计描述
3.4.52状态与4状态
3.4.6用封装的模型协同模拟
3.5增量式编译
3.6模拟器控制台
3.7本章小结
3.8习题
第4章测试基准组成与设计
4.1测试基准的分类与测试环境
4.2初始化机制
4.2.1寄存器传输级初始化
4.2.2编程语言接口初始化
4.2.3时刻零的初始化
4.3时钟生成与同步
4.3.1显式与倒换方法
4.3.2绝对跃变时延
4.3.3时刻零时钟跃变
4.3.4时间单位与分辨率
4.3.5时钟倍频器与分频器
4.3.6时钟独立与抖动
4.3.7时钟同步与Δ时延
4.3.8时钟生成组织
4.4激励生成
4.4.1异步激励程序
4.4.2指令代码或可编程激励
4.5响应评估
4.5.1设计状态的转储
4.5.2黄金响应
4.5.3时态规范的检查
4.6验证实用程序
4.6.1错误注入程序
4.6.2错误与警告的告警机制
4.6.3存储器装载与转储机制
4.6.4稀疏存储器与内容可寻址存储器
4.6.5断言例程
4.7测试基准至系统设计接口
4.8常见的实际技术与方法
4.8.1验证环境配置
4.8.2总线功能模型
4.9本章小结
4.10习题
第5章测试构想、断言与覆盖
5.1分层验证
5.1.1系统层
5.1.2单元层
5.1.3模块层
5.2测试规划
5.2.1从体系结构规范中抽取功能
5.2.2功能分级优先
5.2.3建立测试用例
5.2.4跟踪进程
5.3伪随机测试生成程序
5.3.1用户接口
5.3.2寄存器与存储器分配
5.3.3程序构造
5.3.4自检机制
5.4断言
5.4.1定义所断言的内容
5.4.2断言组成
5.4.3编写断言
5.4.4内建商用断言
5.5SystemVerilog断言
5.5.1立即断言
5.5.2并发断言
5.6验证覆盖
5.6.1代码覆盖
5.6.2参数覆盖
5.6.3功能覆盖
5.6.4条目覆盖与交叉覆盖
5.7本章小结
5.8习题
第6章调试进程与验证周期
6.1故障捕获、范围压缩与错误跟踪
6.1.1故障捕获
6.1.2范围压缩
6.1.3错误跟踪系统
6.2模拟数据转储
6.2.1空间相邻点
6.2.2时态窗口
6.3潜在故障原因的隔离
6.3.1参考值、传播与分支点
6.3.2正向与反向调试
6.3.3跟踪图
6.3.4时间框架
6.3.5负载、驱动源与锥形跟踪
6.3.6存储器与阵列跟踪
6.3.7零时间回路结构
6.3.8系统设计的4个基本视图
6.3.9典型调试器的功能
6.4系统设计更新与维护：修改控制
6.5回归、发布机制与流片标准
6.6本章小结
6.7习题
第7章形式验证初步
7.1集合与运算
7.2关系、划分、偏序集与格
7.3布尔函数与表示
7.3.1对称布尔函数
7.3.2不完全指定的布尔函数
7.3.3特征函数
7.4布尔函数运算符
7.5有限状态自动机与语言
7.5.1积自动机与状态机
7.5.2状态等价与状态机最小化
7.5.3有限状态机的等价
7.5.4图算法
7.5.5深度优先搜索
7.5.6宽度优先搜索
7.6本章小结
7.7习题
第8章判定图、等价检验与符号模拟
8.1二叉判定图
8.1.1二叉判定图上的运算
8.1.2变量排序
8.2判定图的变异
8.2.1共用二叉判定图
8.2.2边属性二叉判定图
8.2.3零抑制二叉判定图
8.2.4有序功能判定图
8.2.5伪布尔函数与判定图
8.2.6二叉瞬时图
8.3基于判定图的等价检验
8.4布尔可满足性
8.4.1消解算法
8.4.2基于搜索的算法
8.4.3蕴涵图与学习
8.5符号模拟
8.5.1符号验证
8.5.2输入约束
8.5.3利用特征函数的符号模拟
8.5.4参数化
8.6本章小结
8.7习题
第9章模型检验与符号计算
9.1性质、规范与逻辑
9.1.1使用自动机的时序规范
9.1.2时态结构与计算树
9.1.3命题时态逻辑：LTL、CTL*与CTL
9.1.4公平性约束
9.1.5CTL*、CTL与LTL的相对表示性
9.1.6SystemVerilog断言语言
9.2性质检验
9.2.1使用自动机的性质规范
9.2.2语言包含
9.2.3CTL公式的检验
9.2.4有公平性约束的检验
9.3符号计算与模型检验
9.3.1符号有限状态机表示与状态遍历
9.3.2反例的生成
9.3.3等价检验
9.3.4语言包含与公平性约束
9.4符号CTL模型检验
9.4.1不动点计算
9.4.2有公平性约束的CTL检验
9.5计算改进
9.5.1早期量化
9.5.2一般化余因数
9.6模型检验工具的使用
9.7本章小结
9.8习题
参考文献
缩写词汇表

过去几十年，微电子技术高速发展所取得的巨大成就和人们对信息技术的大量需求，使得现代集成电路系统的规模和复杂程度日趋提高。这必将导致对未来集成电路系统的设计和制造提出更高的要求。
　　一方面，要在包含数以亿计的晶体管的电路中避免出现设计错误，这是一项非常艰巨的任务。据报道，1994年Intel公司生产的Pentium芯片中的浮点除法运算错误是在其大量进入商用后才被一位用户发现的，虽然这种错误发生的概率为几亿分之一，但这个设计错误还是给Intel公司造成4.75亿美元的经济损失和难以估量的形象损失。另一方面，从集成电路设计角度看，系统设计是否满足规范的需求，以及在设计的各个阶段的等价性检验等都对设计验证提出很高的要求。
　　William K. Lam博士所著的这本书正是全面而系统地阐述如何应对上述两方面挑战的入门读物。它汇集并整理大量的数字硬件设计验证的技术和方法，提出许多设计验证的原则及实际算法；更值得一提的是，本书叙述深入浅出，为想进入形式验证这一具有“高深数学门槛”的领域的读者提供了一种很好的学习方法。
　　本书的主要内容围绕着对硬件设计进行验证的两大方法（基于模拟和形式验证的方法）展开。第1～6章论述基于模拟的验证。在引入设计验证的一些基本概念以后，作者提出硬件设计代码的编码风格准则及排除静态错误的方法；第3章介绍模拟器的基本体系结构与操作；第4章则对测试基准的组成与设计进行全面阐述；第5、6章分别讨论进行模拟时的测试规划和测试构想，以及研究错误查找周期中不同环节的方法和过程。第7～9章对形式验证这一当前技术热点的若干主题进行循序渐进的讨论。第7章为不熟悉有关形式验证所需的数学预备知识的读者提供很好的入门材料；第8章则花费大量篇幅讨论二叉判定图（BDD）的构造、简化及相应的检验技术；第9章详细讨论模型检验、符号模拟技术，并对所用到的时态逻辑知识点作了精心的安排，使读者能更好地理解这些非常抽象的符号。当然，如果读者事先具备命题逻辑和一阶逻辑的背景知识则更好。
　　本书作为为数不多的硬件设计验证的系统论著，有其鲜明的特点：对内容的叙述非常详尽。比如，既讨论一般的原则也展示具体的实践方法，有些内容还提供伪代码形式的算法，读者只需简单地改写为具体的程序设计语言，即可上机调试。此外，本书作者William K. Lam博士是Sun公司的资深经理及高级工程主管。他在Sun和惠普公司任职期间，致力于设计验证、低功耗设计及分析、逻辑综合及自动测试生成（ATPG）等工作。正因为这样，本书不是枯燥无味的从理论到理论的陈述，而是包含大量实例，从而更为实用。
　　正如作者在前言中所说，本书的读者可以是在校的学生，也可以是企业的验证工程师；他们都可以从本书中获得“一站式”的现代硬件设计验证指南。
　　据译者所知，目前在国内还没有关于硬件设计验证的论著出版。因此，引入这方面的国外论著是一件非常有意义的工作。本书的翻译遵从忠实于原著的原则，但对于原著中出现的一些明显错误做了修正。另外，还根据原书作者提供的勘误表改正了原文的一些错误。由于本书涉及大量电子科学、计算机科学及数学的一些知识，译文中对一些汉语中没有对应现成译名的名词（尤其是集成电路领域的术语）都给出原文，供读者对照；另外，译者还专门编写了原书中出现的术语缩写词英汉对照表。
　　在翻译本书的过程中，得到家人的理解和支持。机械工业出版社华章分社的编辑做了大量工作。此外，还得到我的同事俞水根先生的协助。在此，一并对他们表示衷心感谢。
　　虽然尽了最大努力，但由于水平有限，译文中难免会有错误和不当之处，敬请读者不吝赐教。我的邮件地址为：wangww at vlsi.zju.edu.cn

王维维
2006年3月于浙江杭州