Verification Overview

本文探讨验证(Verification) 这个主题,从芯片验证领域的各种技术的出现原因入手,
力求将各种技术理顺,串联成一个整体得到一幅Verification的全景。

验证的目的是100%地证明设计实现完全符合设计规范的要求,
即确保设计实现是“正确”的 。要完成这样的任务,需要以下2方面:

1. “正确”的定义

要证明设计是“正确”的,首先得有个参考标准,设计规范(Specification)担当了这个角色。
Spec当中详细定义了预期的设计行为,是整个设计工作的唯一参考。
但是,spec大多由自然语言写成,而自然语言会有二义性,不可能如程序般精确。
再者,同样的描述,各人的理解也不相同,况且由这种人工的理解再去转化成具体的验证程序,这中间又有一层。

解决这个问题的传统方法是用程序写一个Reference Model,以这个model作为参考,而非不精确的spec。这种方法多见于processor的设计中。因为这类设计大多会提供给软件人员一个模拟器,模拟processor的行为,甚至会精确到周期。所以正好可以用这个model来嵌入到验证环境当中,用它去比对设计实现的行为。

但是这个model的书写比较耗时, 所以不常见于processor之外的应用领域。

还有验证model正确性的问题,即如何保证model是符合spec的,不过model的描述层次和设计实现的层次是完全不同的,不容易出现同样的错误。

正是因为model会有如上的问题,所以出现了如今比较流行的解决方法ASSERTION。

ASSERTION语言用精确的程序表述spec所期望的行为,但这种表述与具体的实现无关,它只负责明确地表述要求,不关心如何实现这个要求。而这个ASSERTION表述可以被验证工具理解,工具会在运行过程中去检查设计是否符合了ASSERTION的要求。

这种类型的验证过程称做 “Assertion Based Verification”。而这种ASSERTION写成的规范又一个称呼是”Executable Specification”,即这种规范可以被工具所理解,可以被工具去直接执行。

2. TestBench

设计是用来完成某个工作的,spec定义的行为自然是动态的。

如果设计静止不动,什么也不做,即使我们知道了它的正确行为是什么,也无法判断他是否正确。

只有它实际动作起来,我们才能够比对其行为是否与SPEC一致。

所以我们需要TestBench, 需要一个环境让设计跑起来。

如何在最短的时间内比对完所有的动作,这是TestBench的关键。

设计大多是确定性的线性系统,有什么样的输入,就会有确定的内部动作和输出结果。

所以,设计的动态性,决定于其输入,这就使激励的生成,成了TestBench的核心主题。

任何工作都需要一个目标,TestBench的目标就是使得spec中定义的行为都被覆盖到,这样我们才能保证设计完全符合了spec的定义。我们还需要方法确定某个spec定义我们是否已经覆盖过。对于已经覆盖过的,我们不必浪费时间再做一次,这样可以最优化激励的效率。

使用前面的assertion, 我们已经描述了spec中我们需要验证的每一个行为,这每一条,恰好就是需要覆盖的点,而assertion是工具可以理解的,所以工具在检查assertion的同时,可以给出该assertion是否覆盖。这种基于function或者说assertion的覆盖率,就称做 functional coverage.

有了functional coverage作为评判标准,我们可以开始设计最优的激励。而随着设计的复杂度上升,激励的组合情况也越来越复杂。人工书写所有的激励十分困难而且耗时。而程序又不可能知道什么样的激励对应着什么样的功能,所以现在的激励越来越倾向于随机生成( Randomization Verification)。有的时候,我们可以对随机化做一些控制,使其偏向某个方向,这称做 Biased Randomization。而这里的BIAS仍然需要人工去控制。不过曾看到有种叫做 Genetic Algorithm的办法,通过不断的迭代,使得最初的BIAS能够自动的根据测试结果向高覆盖率的方向收敛,至于如何控制这个收敛,有待研究。

各种验证技术包括验证语言都是围绕spec和testbench 展开的。具体的验证技术比较,另开一帖。

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-Share Alike 2.5 License.