一、引言

　　在片上系统的设计与实现中，验证这一环节日益重要，整个过程中花在验证的时间比重越来越大，主要原因在于随着SoC 芯片复杂度的提高，验证的规模也成指数级的增加。系统芯片的时代已经到来，在RTL级硬件设计的抽象层次上已经无法应付数以百万和千万门系统的设计和验证。据统计，两年来，一次投片成功率已经由50%降低到39%。不能一次成功的设计必须再投入几个月的设计验证时间和数十万美元的费用。这种风险已经变得不可接受了。因此设计验证出现了所谓的“验证危机”[2]。功能验证已经成为集成电路设计和开发的瓶颈，这就使得验证的方法逐渐受到业界人士的高度重视。工程师们在设计时不可能考虑到万无一失，所以很多系统行为是不能紧紧通过测试文件就能保证系统功能的正确性。

　　二、SOC验证的特点

　　片上系统(SoC)是一种建构技术，主要由处理器(MCU)以及一些外围设备如UART，MAC，控制器等构成，系统结构图如图1。SoC的验证和ASIC的验证工作有很多相同地方：首先都要进行模拟，检查设计是否符合规则，使用各种方法对芯片进行测试。但是，SOC的验证又比较特殊，存在一些特殊挑战。

　　1.整合：验证SoC的首要重点就是检查各种元件之间的整合程度，这里隐含的基本假设就是每一部件都已经完成自我检查。

　　2.软硬件协同验证：处理器中运行的软件必须和硬件部分产生关联才能进行验证。或者我们应该把软硬件当作一个完整的测试中元件(Device Under Test),对涉及软硬件结合状态的方案进行测试。所以我们要找到一种方法来检验我们编写的测试，以及在涵盖的测试范围中，软硬件之间的关联性。

　　3.IP核复用：对于可重用的IP核要建立可重用的验证元件。建立可重用的验证元件，会遇到重大挑战，但同时也会因此而获得更大利益。

　　SoC代表的是一类极其复杂的系统。一个典型的SoC需要一个或多个微处理器，还需要一些其他部件，如DSP、Memory等。为验证SoC，首先需要验证每个部件的正确性，然后要验证部件间连接和通信的正确性。SoC验证问题实际上就是：如何针对具体的验证任务，选择适当的验证工具并加以整合。

　　三、当前常用的验证方法

　　关于验证的方法有很多，但是到现在为止还没有任何一种方法可以非常有效地对系统芯片进行功能验证。概括来看，迄今的验证方法可分为模拟、仿真和形式验证三种[3]。

　　1、模拟验证

　　模拟验证是将激励信号施加于设计，进行计算并观察输出结果，并判断该结果是否与预期一致。

　　优点：模拟验证是传统的验证方法，而且目前仍然是主流的验证方法。

　　缺点：非完备性，即只能证明有错而不能证明无错。因此，模拟一般适用于在验证初期发现大量和明显的设计错误，而难以胜任复杂和微妙的错误。模拟验证还严重依赖于测试向量的选取，而合理而充分地选取测试向量，达到高覆盖率是一个十分艰巨的课题。由于设计者不能预测所有错误的可能模式，所以尚未发现某个最好的覆盖率度量。即使选定了某个覆盖率度量，验证时间也是一个瓶颈。

　　2、仿真验证

　　从电路的描述抽象出模型，然后将外部激励信号或数据施加到此模式中，通过观察该模型在外部激励信号作用下的反应来判断该电子系统是否达到了设计目标。仿真的方法是目前进行设计时常用的方法，根据不同的仿真层次，有不同的仿真工具。

　　优点：仿真比模拟的验证速度快得多，

　　缺点：代价昂贵，灵活性差。

　　3、形式验证

　　形式化验证是不同于仿真方法的对逻辑设计结果进行的另一种验证方法[4]。在 自上而下的设计过程中，在设计的各个阶段和级别，每一级设计都是以上一级的设计作为设计目标，得到本级的设计结果的结构描述，这是设计和综合的过程。

　　优点：完备性，能够完全断定设计的正确性。

　　缺点：首先要对原始设计进行模型抽取，这对使用者有数学技能和经验上的要求。而且，有的工具需要人工引导(如定理证明)，有的工具存在状态空间爆炸 问题(如模型检验)。

　　类型：

　　(1)等价性检验[5]

　　它是用数学方法验证参考设计与修改设计之间的等价性。(如图2)利用等价性验证工具可对这两种设计方案进行彻底的检验以保证它们在所有可能的条件下都有一样的性能。还可利用等价性验证来验证不同的RTL或门级实施方案的等价性。

　　从整个数字系统的设计流程看，等价性问题几乎存在于每个上下相邻的设计层次中，见图2。

　　(2)定理证明技术。

　　运用公理和已经证明的定理证明电路的描述是正确的。

　　这两种方法各有特点，其中定理证明虽然能够给出设计是否正确的一个确切的回答，但由于涉及很多数学推理方面的知识，这就要求用户有很强的数学功底，这也是这种方法不能推广的一个原因。而等价性验证是验证不同阶段的设计是否相互等价的一个很好的方法。一个SOC设计是分为多个阶段进行的，那么下一个阶段的与上一个阶段的等价是设计的正确的一个保证。

　　四、新型的验证方法

　　针对SOC验证出现的各种问题现在还没有一种完全行之有效的方法出现，解决办法之一是基于断言的验证(ABV)[6]，它是把形式化方法集成到传统模拟流程中的一种有效的方法。设计团队在RTL设计中插入设计意图(断言)并且进行模拟，然后用形式化技术检查断言，限制条件，也就是合法接口行为的断言，和其他断言同时一同参加模拟。断言检查的结果改进模拟的有效性。即使利用传统的模拟验证，断言也可以大大提高模拟的效率。基于断言的验证要由用户写出断言，断言表示要验证的性质，因此需要性质描述语言。例如逻辑和时序方面的性质。这就需要尽快找到一种能实现上述功能的语言。SystemVerilog正是在这种情况下产生的，正逐渐被业界人士接受。

　　五.结论

　　形式化方法最近几年取得了长足进展，特别是等价性检验已经集成到标准验证流程中。设计和验证方法的进步应当是渐进的，不可能发生革命性的改变。因此在可以预见的几年内，混合验证方法应当成为主流的验证方法。

　　基于断言的验证是结合形式化验证和传统的模拟验证可行的途径。支持这种途径的统一的设计和验证语言是SystemVerilog。该语言已经得到很多EDA厂商和用户的支持，预计将会流行起来。