硬件设计验证--基于模拟与形式的方法

　　本书全面介绍硬件系统设计验证的技术和方法，主要涉及基于模拟和形式验证的方法，内容涵盖静态检验、模拟器体系结构、测试基准设计、模拟规划与策略、调试进程与验证周期，形式验证背景知识、判定图与sat问题、符号计算与模型检验。书中汇集大量设计验证的基本概念与技术，内容深入浅出，叙述详尽，既讨沦一般的测试原则又展示具体的实践方法，包含作者多午实践经验，实用性强。每章最后还配有各类习题，渎者可用来巩固所学的知识。.
　　 本书可作为高等院校电子科学与技术、计算机科学与技术等专业高年级本科生或低年级研究生教材，也可供相关专业工程师参考。..
　　 随着数字逻辑设计的规模越来越大，复杂度越来越高，功能验证已经成为设计过程中的首要瓶颈。缩短验证时间是项目取得成功的关键。本书系统地阐述了当今最具价值的基于模拟和形式方法的验证技术，帮助测试工程师和设计工程师为每个项目选择最佳的解决方法，最快地在设计中建立起自信，并将它移植到更快的制造过程中。
　　 本书作者william k．lam是设计验证方面的世界级一流专家，书中汇聚了作者广博的实践经验，既讨论一般的测试原则，也展示具体的实践方法，有些内容还提供了伪代码形式的算法，读者只需简单地改写为具体的程序设计语言，即可上机调试。无论高校学生还是企业的验证工程师都可以从本书获益。...

译者序.
前言
致谢
第1章 设计验证的缘由
1．1 什么是设计验证
1．2 验证的基本原理
1．3 验证方法学
1．4 基于模拟的验证与形式验证的比较
1．5 形式验证的局限性
1．6 verilog语言调度和执行语义简介
1．7 本章小结
第2章 编写验证的代码
2．1 功能正确性
2．2 时序正确性
2．3 模拟的性能
2．4 可移植性与可维护性
2．5 可综合性、可调试性与通用工具兼容性
2．6 基于周期的模拟
2．7 硬件模拟／仿真
2．8 2状态与4状态模拟

　　过去几十年，微电子技术高速发展所取得的巨大成就和人们对信息技术的大量需求，使得现代集成电路系统的规模和复杂程度日趋提高。这必将导致对未来集成电路系统的设计和制造提出更高的要求。.
　　一方面，要在包含数以亿计的晶体管的电路中避免出现设计错误，这是一项非常艰巨的任务。据报道，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@vlsi zju．edu．cn。...
　　王维维
　　2006年3月于浙江杭州
　　

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