针对assertion based验证的一些“建议”和“不建议”

近年来，断言（assertions）在形式验证（formal）、EDA仿真验证（simulation）和emulation中普及的速度正在加快，因为验证工程师已经认识到在验证环境中使用断言监视RTL行为的巨大好处.

在设计层面，使用assertion-based verification (ABV)，设计人员可以在开发RTL时加入断言，然后进行模块级的形式验证完成冒烟测试。这相比搭建EDA仿真验证平台，可能会节省几个月的时间，并且断言检查能够提供更快的调试速度，因为断言报告的位置往往就在几个周期以内。

在验证层面，在使用形式验证作为EDA仿真验证补充时，这些断言会继续发挥作用，当然也可以新增断言做更加完备的检查。同时，在这个阶段断言除了能够检查设计的功能正确性，还可以使用断言覆盖率量化验证进展。

以上是断言在设计和验证层面具有的好处，但是实际上采用断言也会面临非常多的挑战。下面是针对assertion based verification(ABV)的一些“建议”和“不建议”。

建议：

• 专注于断言语言的productive subset（具有生产力的部分）。一下“吃”得太多，反而会增加出错的机率。想学习任何语言一样，我们没有必要马上精通整个语言的语法，逐步推进式学习能够更高效地吸收其中的核心思想。

. 考虑使用库。诸如Open Verification Library (OVL)和Incisive Assertion Library (IAL)这样的库包含共同的组件，恰恰就是上一条提到的“productive subset”

. 将眼光放远一点。在断言方面做的工作应该应用于整个验证流程甚至芯片研发流程中，包括模块级、芯片级和系统级。例如，为形式验证编写的断言应该应用于EDA仿真中。

. 考虑复用性。针对需要重复用到的断言，要考虑创建一个可参数化的可复用断言库，并且要在今后的项目中不断地复用和改进这些库。

. 在仿真中统计这些断言的覆盖率，以确认输入激励是否真的覆盖点这些测试点。

不建议：

. 为设计的所有测试点都编写断言。首先要把重点放在控制逻辑上，专注于高风险的场景。当然如果如果时间允许的情况下，可以小心地增加更多的断言。在做白盒分析时，需要特别关注其中的控制部分，因为大部分bug都藏在这里面，因此具有最大的价值。

. 害怕使用简单的VHDL或Verilog/SystemVerilog来生成更容易的条件以简单化断言检查。这样做可以减少由于创建错误断言而引起的风险。

. 消极等待引入断言。断言创建应该开始于设计开发过程中的早期阶段。当设计人员编写RTL时，验证人员在考虑端到端检查时就应该编写白盒补充断言。

Reference：《Assertion-based verification delivers rewards》