日志

验证的方法篇之二：静态检查

已有 4273 次阅读| 2016-8-25 18:27 |个人分类:验证系统思想

与动态仿真相对的是静态检查，它本身不需要仿真、波形激励，通过工具的辅助，验证人员即可以发现设计中存在的问题。静态检查方法较为分散，且关注的验证领域也不为一致，我们将目前主要的方法概括为：

语法检查（syntax check）
语义检查（linting check）
跨时钟域检查（CDC，cross-clock domain check）
形式验证（formal verification）

语法检查

如大多数编译器（compiler）自带的功能一样，各种硅前验证的工具一旦需要建立模型（无论是针对动态仿真还是静态检查的模型），都需要其编译器对目标语言提供语法检查。对于硅前阶段，各种编译器带来首要的好处是帮助检查明显的语法错误，例如拼写、声明、引用、例化、连接、定义等等常见的语法错误。

不同仿真工具对于同一语言标准的解释和理解也可能存在偏差或者不同的严格程度，所以在使用不同厂商、不同工具提供的编译器时需要注意的地方包括：

理解不同的语法格式或者实现途径，可能在编译器A面前可以通过，却不见得在编译器B之前可以通过。这种差别通常来讲，跟仿真器的特性和支持也有关系。如果在同一个硅前周期使用了不同的工具，那么我们要做的应该是让目标代码（无论是设计代码还是验证代码）满足所有工具的要求，确保它们跟工具之间良好的语法认可度。
由于语言本身也有不同年份的标准，所以我们需要在编译过程中注意加注不同的选项，例如如果默认编译器按照VHDL93标准来编译VHDL文件，那么要显式地声明VHDL文件是87格式，需要额外加注编译选项。
除过语法检查，编译器选项中也会包含一些检查设计代码风格是否符合可综合规范，建议在编译阶段加上这些选项，它们会帮助检查设计中较明显的漏洞。
对于SystemVerilog，值得注意的是，最新的SystemVerilog2012中的标准并没有全部被编译器支持，而且不同工具的支持程度也是不尽相同的。如果你在使用一个看起来较“偏门”的功能，在实现它之前可以查看一下工具支持文档，或者看编译器的编译结果来查看是否被支持。

对于初步认识仿真工具的人而言，可能不同编译器对于同一项语法错误给出的错误提示也不相同。这里我们能够给出的建议是：

认真阅读错误信息。没错，请你认真阅读错误信息。
在认真阅读无果的情况下，根据错误信息的代码可以通过工具命令结合错误代码来查看错误信息的具体解释。
如果你对前面两个步骤仍然免疫，请找一位更有经验的领路人帮你一起检查错误，并且给你一些如何阅读错误、查找语法错误点的方法。

语义检查

语义检查和语法检查相比，是在设计可行性上做深入检查的（当然前提也是首先通过了语法检查）。语义检查是通过专用的工具来协助完成的，例如0-In（Mentor）以及Spyglass。常见的语义检查包括的范围有：

常见的设计错误
影响覆盖率收敛的问题
可能会产生‘X'以及受其影响的设计部分

进一步细化这些检查项，它们会检查设计的这些部分：

验证收敛性检查

无法达到的逻辑部分
无法跳转到的状态机状态
无法完成的状态机跳转逻辑

硅效用检查

寄存器被固定赋值
寄存器未初始化
X值的传播

功能问题检查

状态机检查
总线检查
case语句检查
数学逻辑检查

这些静态检查最大的便捷在于，一些功能实现以外的设计问题可以在更早期就被发现，而且这些静态检查也有助于完善设计编码风格，使其更有助于覆盖率的收敛和后端综合以后的逻辑实现保持（例如寄存器未初始化或者固定赋值）。语义检查最明显的两个优势在于：

不需要验证环境：即无论设计人员还是验证人员可以几乎同设计同步来检查设计中明显的设计问题，这对仿真之前扫清明显障碍、保证设计质量很有帮助。
不需要写断言：这跟我们接下来介绍的形式验证方式有关。由于语义检查无关乎设计从功能描述到功能实现的翻译准确度，所以也就无需要断言参与进来。

跨时钟域检查

大多数复杂的设计都拥有不止一个时钟，而且多个时钟之间也是异步的关系。对于设计中的不同功能模块如果被不同的时钟驱动，那么就会形成不同的时钟域（clock domain）。对于单一时钟域的设计而言，它的设计方式和验证环境都较为简单。而对于多时钟域而言，不同时钟域之间的逻辑通讯就需要考虑同步问题了。在这里，用来验证这些设计要求的过程就被称为跨时钟域检查。

之所以需要同步是由于不同时钟域的时钟是异步的关系，这使得从时钟域A的信号进入时钟域B被采样时，每个周期都会有相对时钟B不同的延迟，这种随机性可能会导致建立或者保持时间无法满足（setup timing or violation timing violation），进而导致不可预期的功能失败。

这种跨时钟域问题无法通过常规的验证方法分析，例如动态仿真，也不能被静态时序分析（static timing analysis）判断出来。而这里通过静态的跨时钟域检查就可以分析这一问题。通过该方法可以在早期的RTL阶段来识别出跨时钟域的通信电路上面是否有合适的同步处理。

所以跨时钟域检查（CDC）是为了保证所有的CDC信号都能够得到正确的同步，而进一步来看，CDC检查是为了解决更大的问题：

是否CDC信号同步逻辑防止数据在跨时钟域采样以后不准确？

目前支持CDC检查的商业工具有Spyglass、0-In（Mentor）。

形式验证

形式验证分为两种方式：

等价检查（EC，Equivalence Check）：用来保证两个电路的行为是等价的，可以用来检查不同抽象级的电路是否是一致的，例如RTL级和网表之间。
属性检查（PC，Property Check），又称之为模型检查（MC，Model Check）：电路的行为通过验证语言来描述其属性（property），随后通过静态方式来证明在所有状态空间下都满足该条件，否则举出反例（counter example）来证明设计行为不符合属性描述（property description）。

我们在这里介绍的是属性检查，即通过验证语言（PSL、SVA）来描述设计行为，用断言（assertion）的方式结合设计源进行检查，来证明设计行为同属性描述保持一致。属性检查的流程通常如下：

在动态仿真验证中，我们是通过生成各种测试序列来去访问待验设计中的状态（state）的，而理论上所有可能仿真的设计状态被称作可及状态空间（reachable state space）。对于动态仿真而言，要遍历可及验证空间的所有状态是一项非常大的挑战，这种通过访问状态、检查结果的方式需要覆盖率反馈来衡量可及状态空间还有多少未被访问。

然而动态仿真验证的方式实际上无法来穷举所有可能的序列去访问设计的可及状态空间，而形式验证可以通过数学方式来穷举出所有的状态空间，彻底验证设计。从下图可以看到，在仿真过程中，通过随机和覆盖率反馈的形式，我们可以产生不同的测试序列来访问状态空间，直到我们发现新的缺陷。这是一种实用的测试办法，但是另外一方面，动态仿真验证没有办法去确定设计中不存在缺陷，因为图中其它隐藏缺陷依然有待于去挖掘更多的状态空间才能被发现。

而形式验证可以通过数学的方法来遍历状态空间，进而证明设计行为符合属性描述（property description）。在遍历过程中，一旦遇到反例，形式验证工具便会停止下来，报出反例情景，由用户来核对错误是否属实，再考虑修改设计或者进一步约束属性使其更精确地描述设计行为。下图中可以看到，在大量的状态空间中，形式验证工具只需要针对某一项属性描述举出反例，即可报告给验证人员，而并不需要穷举所有的反例。等待设计缺陷一旦确认、经过修正之后，验证人员可以继续通过工具来对设计和所有的属性进行检查。