写在前面

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

      验证对于IC设计、FPGA设计的重要性无须赘述,现在验证已经成为IC设计技术中,发展最为迅速的领域。对验证有充分的理解和经验成为项目成功必不可少的因素,在国外很多IC设计公司,丰富的IC验证经验是成为项目经理所必须得。

      本文的主要目的是简单介绍验证的概念、方法,从中可以了解问题的背景、思路,有助于理解验证为什么如此重要、为什么如此复杂,也可以了解如果破解这个复杂的命题。

      文章主体分为4的部分,分别是
      1、什么是验证
      介绍问题的出处和背景

      2、验证工具
      验证离不开工具,毫不夸张的说,验证工作就是方法学加上各种各样的工具,对这些工具有充分的了解是做好工作的先决条件

      3、验证计划
      所谓计划就是思路和时间安排的总和,由于问题的复杂性,只有制定好验证计划,对需要验证的点、验证的思路、时间等做好安排,才能高质量地完成验证工作。

      4、仿真管理
      介绍如何实现仿真工作的协调开展。

      5、6。。。可能的其它章节

      文章的主要内容来自《writing testbench》一书,该书确实是验证领域的经典,本人从中获益匪浅,因此希望介绍给大家,也算是共同进步吧。

      由于工作比较忙,加上水平所现,行文可能不那么严谨,恳请大家指正。我一直认为一起做事情,共同探讨,是学习也是交朋友的最好方式。谢谢！
      
      验证不是一个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体系,如图2所示。

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

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

      如果编写RTL代码前需要理解规范,同时编写代码和验证工作由同一个人完成,那么验证的将是对规范理解后的实现,而不是规范本身的实现。也就是说如果理解上出现错误,将不能验证发现。
      转换过程中任何人为因素都是不确定性和不可重复性的来源,因此排除人为因素导致的错误非常重要。在设计中排除人为错误的方法主要包括Automation、Poka-Yoka和Redundancy。

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

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

      Redundancy是去除人为错误的最后选择,这是一种最简单但是成本最高的方法。它要求双倍的转换资源。由一个工程师完成的转换要由另外一个工程师进行验证,或者由两个工程师同时进行转换,然后比较结果是否一致。这种方法一般用于对可靠性要求很高的系统,例如空运系统,或者事后重新设计和替换缺陷部件的成本高于Redundancy本身的情况中,例如ASIC设计。下图所示为规范存在不确定性时使用Redundancy减小理解错误的汇聚模型,在硬件设计中,相应的转换过程为根据书面规范编写RTL代码,这时使用这种方法意味着需要一个专门的人做验证工作。图4为使用Redundancy减小理解错误的汇聚模型

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

      Formal verification分为Equivalence checking:和Model checking两大类。
      Equivalence checking通过一定算法,证明设计实现的逻辑一致性,保证设计的功能在实现过程中没有改变,其汇聚模型如图5所示。

      等效检查可以用于比较两个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。图7为功能验证的汇聚模型

      Functional verification的方法
      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之间转换。图8为验证和测试。