改善验证效率和可靠性的一个方法是自动化，自动化工具很多，有些是功能验证必不可少的，例如仿真器。有些工具可以代替人完成最繁琐的工作，并能提高功能验证的可信度，例如linting和代码覆盖率工具。

Linting tool

Linting tool根据设计的RTL描述代码结构做静态分析，推断描述代码存在的逻辑错误，但无法决定描述代码是否能够现实设计要求的功能。linting  tool可用于强制代码遵从编写规范，由于Linting工具是静态验证工具，因此运行速度会快，可以节省时间。其缺点是多疑，误报率高，产生大量不存在的错误警告，因此要对不存在的错误警告仔细过滤，注意避免滤出真实的错误警告，变量名最好符合命名惯例，有助于过滤。

由于Verilog不是强类型语言，使用Linting tool非常有用，可以检测race conditions 及数据宽度不匹配，可保证Verilog正确描述数据处理过程，避免造成数据的弃位及增位现象，这种错误通过仿真并不一定发现。因为verilog 语言的特点， 对Verilog描述的设计，Linting tool是一种有益的验证工具。因为VHDL 语言的特点，对VHDL使用Linting tool的作用不如对Verilog语言那么明显，但Linting tool还是能发现一些潜在的问题。

仿真器

仿真器通过忽略及简化设计的物理特性，对设计的实现进行模拟。仿真器通过执行RTL级的设计描述，模拟设计的物理实现，它无法确定设计真实的物理实现与设 计描述之间的区别。仿真的结果取决于设计描述是否准确反映了设计的物理实现。仿真器不是一个静态工具，需要Stimulus和Reponse。 Stimulus由模拟设计工作环境的testbench 产生，Reponse为仿真的输出，由设计者确定输出的有效性。

仿真器的类型分为3种类型，Event-driven Simulator（事件驱动仿真器）、Cycle-Based Simulator（基于周期的仿真器）、Co-Simulator（联合仿真器），分别介绍如下：

1．Event-driven Simulator
将信号的变化定义为一个事件，该事件驱动仿真执行，事件驱动仿真器能准确地模拟设计的时序特征，可模拟异步设计。时间驱动仿真器的工作过程如图9所示。

2．Cycle-based simulator
基于周期的仿真器的特点是忽略设计的时序，假定所有flip_flop的setup和hold时间都满足要求，在一个时钟周期，信号仅更新一次，从而信号 必须与时钟同步。仿真速度比事件驱动仿真器高。基于周期的仿真器的工作过程步骤是，首先编译电路，将组合逻辑压缩成单独的表达式，根据该表达式可确定 flop的输入，然后执行仿真，遇到时钟的有效沿，flip_flop 的值被更新。基于周期的仿真器的缺点是不能仿真异步电路，不能进行验证设计的时序。

3．Co-Simulators
联合仿真器对同一设计各个部分，分别用不同的仿真器仿真，如即含有同步设计又含有异步设计的电路，可用Event-driven
Simulator对异步设计仿真，用Cycle-based Simulator对异步设计仿真。联合仿真器中各个Simulator的操作是locked-step的，类似于电路的pipeline操作。其缺点是由于不同仿真器之间需要同步和相互通讯，Co-Simulators的仿真速度受到最慢Simulator的限制，因而影响仿真器的性能，而且在各仿真器传送的信息会产生多义性。

4．Hardware modeler

硬件模拟器创建一个物理芯片的逻辑模型，向仿真器提供该芯片的行为信息，芯片和仿真器的通信过是首先将物理芯片插入硬件仿真器，然后格式化来自仿真器的数 据，作为该芯片的输入，最后将该芯片输出的数据，包含时序信息，送往仿真器。硬件模拟器可以提供很高的仿真速度，但是设备价格高昂。需要注意的是，硬件模 拟器做的仍然是功能仿真，而不是时序仿真，因为芯片是降频运行的.

波形观察器

仿真调试的过程中波形观察器是必不可少的工具，它能提供信号状态和变化的详细信息，但是波形观察器不能用来判断一个设计是否通过验证，因为波形是不可重复的且无法用于递归仿真。

波形观察器的优点是可以观察仿真的整个过程，有利于设计及testbench  的诊断，缺点是由于要输出波形，影响了仿真的速度，因此应尽可能限制在波形图中显示的信号数量及时间长度。

波形观察器的另一个作用是波形比较，主要用于redesign，保证设计具有cycle-accurate的后向兼容性。在波形比较中，不能仅看表象，需 仔细分析，确认波形之间存在的差别是有意义的。例如，有时我们仅关心波形transitions之间的相对位置，而不关心它的绝对位置。

代码覆盖率

代码覆盖率（Code Coverage）可以指示Verilog代码描述的功能多少被验证。代码覆盖率有三种计算方法：

第一种是Statement coverage(block  coverage)，即语句覆盖率，指示验证过程中，设计代码被执行的语句数量。有时，我们会添加一些没有具体设计意义的语句，仅用于监视代码执行过程中的异常或标注一些设计中的假设。这些语句可不参与Statement coverage的统计；

第二种是Path coverage，即分支覆盖率，在设计中往往通过分支控制语句来完成对功能的控制，我们将所有分支控制语句的控制状态进行组合，产生一定数量语句执行path， Path coverage指示所有的语句执行path是否都得以执行；

第三种是Expression Coverage，即表达式覆盖率，指示分支控制语句的控制条件是否全部有效。

需要注意的是百分之百的Code Coverage仅仅表示了代码都被执行了，不能证明设计的正确性。代码覆盖率可以用于衡量验证工作是否完成。

验证的内涵和外延都非常大，常说的验证是指功能验证，占了大部分的工作量，因此大多数时候，人们往往把验证和功能验证等同使用，这里谈的主要也是功能验证。

验证不是一个testbench，也不是一系列testbench，验证是证明一个设计能正确实现其功能的过程。

使用汇聚模型可以从概念上清晰地描述验证过程，如图1所示，其中transformation可以是任何包含有输入输出的过程，例如根据 specification写出RTL代码、扫描链的插入、把RTL级代码综合为门级网表、根据门级网表布局布线等。Verification过程是一个 相反的过程，它从transformation的结果出发回到起点。汇聚模型请参考图1

Verification只能证明存在错误，不能证明不存在错误。Verification的结果宁愿为false-negative，避免为 false-positive，这里的false-negative是指testbench报告的错误在设计中不存在，false-positive指把 设计中的错误报告为正确。false-negative使验证能最大限度地发现设计中的错误，保证了设计的可靠性，而排除误报的、设计中不存在错误并不困 难。

在实际验证工作中，一般采用由TESTBENCH 和DUT(design under test)组成的Verification体系.

这是验证系统普遍适用的模型，Testbench为DUT提供输入，然后监视输出，从而判断DUT工作是否正确。注意到这是一个封闭的系统，没有输入也没有输出。验证工作的难度在于确定应该输入何种激励，相应的正确的输出应该是怎样的。

设计过程中的人为因素

如果transformation过程不是由始到终全部自动完成的，那么就要人去理解规范，并进行transformation，RTL代码的编写就属于这种情况。设计团队根据对书面规范的理解编写他们认为功能正确的可综合代码， 通常进行验证时，由写代码的工程师验证所写的代码功能正确。图3画出了这种情况下的汇聚模型。

如果编写RTL代码前需要理解规范，同时编写代码和验证工作由同一个人完成，那么验证的将是对规范理解后的实现，而不是规范本身的实现。也就是说如果理解上出现错误，将不能验证发现。

转换过程中任何人为因素都是不确定性和不可重复性的来源，因此排除人为因素导致的错误非常重要。在设计中排除人为错误的方法主要包括Automation、Poka-Yoka和Redundancy。

Automation自动化排除了人为的干预，但对于未能清楚定义的情况，以及象硬件设计这种需要人的智慧与创造性的工作，不可能全部自动化。

Poka-Yoka按照简化及标准化的原则，将整个工作过程分步实现，每一步都是极其简单不容易发生错误的，人只需根据渴望的结果决定步骤的顺序。这要求 我们对整个工作过程进行完整的、标准化的定义。根据目前的验证技术，我们还不能对验证过程做如此的定义，因此不能用在验证工作中。

Redundancy是去除人为错误的最后选择，这是一种最简单但是成本最高的方法。它要求双倍的转换资源。由一个工程师完成的转换要由另外一个工程师进 行验证，或者由两个工程师同时进行转换，然后比较结果是否一致。这种方法一般用于对可靠性要求很高的系统，例如空运系统，或者事后重新设计和替换缺陷部件 的成本高于Redundancy本身的情况中.

验证的对象

选择不同的起点和汇聚点决定了不同的验证对象，而起点和汇聚点经常由验证工具决定，因此为了知道验证的对象必须先要清楚验证的起点和汇聚点。Formal Verification、Functional verification由于起点和汇聚点的不同，验证的对象也各不相同。

Formal verification分为Equivalence checking和Model checking两大类。

Equivalence checking通过一定算法，证明设计实现的逻辑一致性，保证设计的功能在实现过程中没有改变.

等效检查可以用于比较两个RTL代码文件，以验证经过修改的RTL代码的功能和原来相同。等效检查也常用于比较两个网表，以保证一些网表后处理，例如扫描 链插入、时钟树综合和手工修改没有改变电路的功能。另一个重要作用是验证网表的功能与原来RTL代码的功能相同，如果认为综合工具是可靠的，那么这个过程 可以省略，但是综合工具是个大型的软件系统，其可靠性依赖于算法和器件库的信息，综合工具发生错误的事情并不少见。等效验证的可以用于保证综合工具的可信 性。例如，假设设计中含有超过48 bit的算术运算，在综合时，综合工具用synthetic lib 中的算术运算符进行映射。但在synthetic lib 的文当中指明该算术运算符不能超过48bit，对于这种 bug，可利用Equivalence checking检测。

Model checking用于检测设计是否违反用户定义的设计行为规则，这些行为规则用 Assertions（断言）来定义，如状态机的状态跃迁，接口的握手过程。Model checking的难点在于定义需证实的Assertions，一般对定义的Assertions，仅能证实它的一个子集。当前的技术对保证设计复杂功能实现的Assertions无法证实。图6为Model checking的汇聚模型。

Functional verification（功能验证）保证设计预定功能的实现，功能验证过程能显示出设计符合specification 的程度，但是不能证明设计实现了specification，通过功能验证，只能证明设计存bug，不可能证明设计不存在bug。

Black-box verification（黑盒验证）通过设计顶层接口，验证那些与设计实现技术（ASIC，FPGA或软件）无关的功能。黑盒验证不直接访问设计的内部状态，功能验证和设计实现可并行的进行，但是它很难进行功能隔离(可控性差），很难发现问题的来源（可见性差），不能对设计进行全面的验证。对于大型设计，需添加一些与功能实现无关的设计，增强验证可控性及可见性。如：增加软件可访问的寄存器及数据处理量的控制。

White-box verification（白盒验证）保证设计实现技术（ASIC，FPGA或软件）相关的功能正确实现，是Black-box verification的补充，对设计的内部结构及实现完全可控和可见的，但不可移植。

Grey-Box verification（灰盒验证）根据设计的内部结构写testcase，从设计顶层接口进行控制和观察， testcase 的目的是验证某种设计方法是否实现了一些主要特性，不关心其它的设计方法。

Verification（验证）和Testing（测试）比较相近，容易混淆。Verification（验证）的目的是保证设计功能的正确实现。测试目的是保证设计的silicon implements，由测试向量完成，测试向量可自动生成（ATPG），目的是保证设计内部物理节点能够在逻辑0，1之间转换.