如何选择正确的芯片验证方法

当设计按照抽象级逐步推进时，要注意必须一直保持等效性，以确保最低层的抽象级能满足系统规范的要求。例如：

1)当 C 模型被置于一个系统环境并能够满足规范中所描述的所有系统要求时，芯片规范(一般是一个文本文件)与其 C 模型之间就达到了等效。这在实质上是功能等效。

2)通过比较 C 模型与HDL 实现的输出，可以在规范的C 模型与其 HDL 实现之间建立等效关系。在没有 C 模型的情况下，可使用“期望数据模型”。这在实质上也是功能等效。

3)HDL实现与门级(综合后的)之间通过应用“逻辑等效性检验”可以建立等效关系。这时，由于设计采取的形式是纯粹的逻辑门，而且功能能够被表示为逻辑表达式，因此，这在实质上是逻辑等效。

3 现有验证技术及发展趋势

目前可使用的验证方法及技术如图2所示。

3.1 动态功能验证

使用最为广泛的功能验证方法是动态的，之所以被称为动态是因为输入图形/激励信号是在一段时间(几个时钟周期)内生成并应用于设计的，相应结果会被用于与参考/黄金模型进行比较，以检验其与规范之间的一致性。

仿真器通常用于计算所有的信号值，并将其与指定的期望值进行比较。目前，有两类可供选择的仿真器：

1)基于周期的仿真器：这类仿真器不管在时钟周期内发生了什么事情，它只是在每个周期内对单脉冲信号进行一次求值，由于执行时间很短这类仿真器的速度通常很快。

2)基于事件的仿真器：这类仿真器在时钟周期内或者在时钟边界捕获事件，并在设计中传播这些事件，直到系统达到稳态。

3.2 随机/定向功能验证

在一个有时间限制的仿真过程中，动态仿真器只能验证芯片的典型行为，而不能验证所有可能的行为，这是动态仿真的主要缺陷。出现这个问题的主要原因是对芯片的定向测试是针对已知的测试空间，而不是未知的测试空间进行的。即使是仅对已知测试空间的测试也要花费很长时间。例如，假设推出每个运算数需要一个时钟，为了验证一个能对两个 32 位操作数进行加和运算的简单加法器的测试空间就需要 232x232个时钟周期。随着逻辑运算越来越复杂，验证空间也会相应增加。因此出现了随机动态仿真，通过为设计提供随机激励信号来增加验证的测试空间，这样能够使验证覆盖的功能空间最大化。但当设计规模很大且非常复杂时，随机测试空间会变得无限。为了解决这个问题，更高级的验证语言，如 Open-VERA、E 与SVL (SystemC 验证库)被推出。这些语言引入了诸如约束随机激励信号、随机激励信号分配与电抗性测试平台等概念。伴随着这些语言的运用，出现了一些用于对其进行解释的工具，如VERA、Specman与 OSCI 内核( Concentric System Studio ，CCSS)。

除了引入随机化功能以外，新的验证语言和工具还通过减少公司在构建不同测试场合/方案所花费的时间，来提高生产率。例如，测试方案可以采用最高的抽象级来编写，并能够通过采用功能强大的面向对象型结构而扩展至任何较低的抽象级。

当应用动态验证时，通常需要估计所覆盖的、可以量化的功能空间，包括：经过验证的代码行数(行覆盖率)，经过测试的逻辑表达式个数(表达式覆盖率)，一个 FSM 设计中能够达到的状态数(FSM 覆盖率)，在一个仿真运行中可以双向变换的端口及寄存器数目(变换覆盖率)，以及设计代码中覆盖的逻辑通道数目(通道覆盖率)。以上可以使用 Code Coverage 及 Lint 工具来实现。  

3.3 断言

设计者将断言用作一个占位符，用来描述与设计相关联的假设及工作特性(包括暂时的特性)。如果设计满足或未满足规范或假设，则断言将会在一个动态仿真过程中被触发。断言还可在形式/静态功能验证环境中使用。

3.4 混合功能验证

在该方法中通常执行动态仿真，仿真结果被用作静态验证的输入。在静态验证过程中，在设计中传播的是逻辑方程式/符号，而不象在动态仿真中那样传递数值。这种方法虽然不像形式验证详尽周全，但却具有比纯动态仿真更高的效率。

3.5 静态功能验证

在静态功能验证中，不向设计施加输入激励，而是将设计映射在一个图形结构中，用双择判决图(BDD)或其他数学表示方法来描述所有时间周期内的设计功能。利用这种图形结构来证实或反驳属性可以验证这些数学表达式，这是通过顺着或逆着信号流来传递数值，以确定数学结构中的矛盾式来完成的。

现有的工具通过以下两种方式来满足静态验证市场的需求：

1) 使用断言：这是在模型/设计当中规范并公式化的设计约束(使用SystemVerilog、Open-VERA、Verilog和VHDL等设计/验证语言)。   

2) 使用属性：这允许使用属性语言(如PSL和Sugar)对属性进行规范。