SOC的形式化验证方法

摘 要：如何对片上系统(SOC)来进行验证，是一个比较复杂的问题。本文介绍了用形式化方法来验证SOC，讨论在对SOC进行等价性验证时应注意的几个问题以及解决的方法。最后给出了对SOC验证的一般方法。

关键词：片上系统；形式化验证；等价性验证；模型检验

引 言

　　随着设计规模的增大和设计复杂度的提高，片上系统(SOC)的验证问题已经成为缩短设计周期的瓶颈。任何一种EDA工具都不能完全解决SOC验证问题。因为验证必须在各个角度进行。例如从下面多个方面考虑：

(1)规范是否正确。在进行系统设计时，首先要对所设计的系统的要求有一个规范。此规范若用自然语言描述，可能产生歧义。用形式化的方法来描述，或者用一套符号体系来刻划就比较严格。

(2)设计队伍正确理解规范的问题。这是设计的基础。若没有正确的理解，那么下面的一切工作都建立在错误的条件下，也就无法实现设计要求。

(3)每个模块设计的正确性。在自顶向下的设计中，每个模块是否正确地实现了规范中的部分功能。

(4)模块之间的接口是否正确的问题。当每个模块都是正确时，并不能保证设计就是正确的，在模块正确的基础之上，还要考虑它们之间的接口是否正确。

(5)是否真正完全实现了所需要的功能。在以上各个问题都解决的情况下，还要考虑是否真正实现了所需要的功能。所以很难确定在什么情况下验证算是完成。

验证的困难体现在下面两个方面：

(1)验证的复杂性。对于一个基本触发器来说，状态数目是2个，要测试模式的数目是4个：对于Z80微处理器，有208个寄存器和13个基本输入，那么可能的状态数目为2²⁰⁸⁺¹³= 2²²¹，对于1MIPS的计算机来说需要花费1053年才能仿真完所有的转移，Z80大约有5k门。对于20M门的芯片、片上系统又要多长时间呢?

(2)验证的完整性。由于不能对设计的所有情况进行仿真和验证，那么验证又在什么情况下是完整的呢? 是当我们耗尽时间和金钱时、是当我们需要制造产品时、是当我们检查完HDL代码的每一行的执行时，还是当我们测试了一周，而没有发现一个新的错误时?

对于一个设计者来说，并没有理想的完整性。因为设计往往是非常复杂的，无法确保全部功能的覆盖，并且可能的矢量数目远远超过所允许进行测试的时间。在验证过程中，随着发现错误数目的减少，查找错误所需要花费的时间和金钱却在增加。所以验证需要解决好两个问题：多大程度的验证就足够了? 和什么时间验证开始进行?

SOC一般的验证的策略

一般的验证的方法
自顶向下的验证方法：从整个系统到单个部件来验证。自底向上的验证方法：从单个部件到整个系统来验证。基于平台的验证方法：在一个已经存在的平台中来验证开发好的IP。

基于接口的系统验证方法；在接口层模拟每一个模块。对于自底向上的方法来说，它进行的验证是局部的，对功能IP核能够比较容易和比较快地捕捉错误。然后，SOC的设计就是在这些高度可信赖的“无错误”的IP核上进行。而最后的综合验证是适合应用基于接口的系统验证方法。

典型的验证方法
仿真

———testbench ：把一个设计置于验证环境下，来验证输入信号经过该设计后是否得到希望的响应。测试环境通常是指testbench。一个验证环境通常包括一组部件：如总线功能模块、总线监视器、存储模块等，以及这些模块在所要验证的设计的相互连接，验证还要有适当的模式和矢量。

———随机测试：在没有工程师的参与下，创建测试脚本，来进行功能验证。

———逆向测试：避免由一个错误来引起其它的错误，逆向测试是可以自动完成的，它产生新的测试检验测试结果，并产生测试报告。以上的方法都是仿真，从电路的描述抽象出模型，然后将外部激励信号或数据施加到此模式中，通过观察该模型在外部激励信号作用下的反应来判断该电子系统是否达到了设计目标。仿真的方法是目前进行设计时常用的方法，根据不同的仿真层次，有不同的仿真工具。

形式化验证
利用定理证明的方法和数学推导的方法来验证设计结果的正确性。形式化验证是基于严密的理论体系，用理论证明设计项目是否正确，目前形式化验证已经由研究阶段进入了应用阶段。

形式化验证
形式化验证是不同于仿真方法的对逻辑设计结果进行的另一种验证方法。在自上而下的设计过程中，在设计的各个阶段和级别，每一级设计都是以上一级的设计作为设计目标，得到本级的设计结果的结构描述，这是设计和综合的过程。验证的任务就是证明所得到的结果正确的实现其设计要求。这里通常包括两个方面：

(1)下一级所实现的功能与上一级的设计目标所要求的功能相一致，既功能验证。

(2)下一级本身符合设计规则和条件制约，包括连接关系的限制、时间关系的配合等，这就包括结构验证、时序验证和规则验证。

由于计算机工业的迅猛发展对设计自动化的需求，以及计算机结构与逻辑体系的密切联系，形式化验证的研究也随之迅速发展。近年来，陆续有许多有效的方法问世，并逐步向实用化方向发展。

形式化验证的一般方法
一般情况下，在设计的各个阶段可以得到不同级别的实现结果，前一阶段的结果作为后一阶段的目标，因而从广义上来讲，就是要证明电路的两种实现的等价。

组合逻辑电路的逻辑验证
对于组合电路来说，不存在状态寄存器，其输出值Z[ t ]不依赖于前面的输出值Z[t-1]，(1≤t-1≤t)。这时只要对每个输入向量证明起输出向量是相同的。

时序逻辑电路的验证
对于一个时序逻辑电路来说，可以把它看成一个有限状态机( FSM)。电路功能的等价可以用有限状态机的等价来判断。假定两个状态机A和B，要对它们进行比较。直观的说，当A和B有相同的接口，而且从相同的初始状态出发，两者对任意有效输入序列产生相同的输出值序列，则可以说A和B等价。

常用的时序逻辑电路和逻辑验证方法有三种：

(1)定理证明技术。运用公理和已经证明的定理证明电路的描述是正确的。

(2)状态搜索技术。这里引入二叉判定树(BDD)表示状态集合，用深度优先和广度优先的方法搜索FSM图，使得这种方法可以用来验证具有大量状态的部件设计。状态搜索技术比理论证明更容易用计算机实现，便于用在验证实际的硬件设计。

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

理论上这种等价性验证可以在任何级之间，但目前我在RTL级与RTL级、RTL级与门级、门级与门级之间进行。



这三种方法都各有特点，其中定理证明虽然能够给出设计是否正确的一个确切的回答，但由于涉及很多数学推理方面的知识，这就要求用户有很强的数学功底，这也是这种方法不能推广的一个原因。而模型检验虽然是一种完全自动化的方法，但它也存在状态爆炸的问题。而等价性验证是验证不同阶段的设计是否相互等价的一个很好的方法。一个SOC设计是分为多个阶段进行的，那么下一个阶段的与上一个阶段的等价是设计的正确的一个保证。下面我们着重分析SOC设计时如何进行等价性的验证。

等价性验证在SOC设计验证中应注意的几个问题

　　在进行SOC设计时，可能是来自不同厂家的IP核的复用及应用，以及部分设计来自不同的硬件描述语言，因此，在进行等价性验证时要注意以下几个问题：

对“未知”(unknown)和“不关心”(don’t care)的理解
　　在仿真中，“未知”(unknown)和“不关心”(don’t care)可以取任何逻辑值。另一方面在综合中，与“不关心”比较一般视为False。

例1　“不关心”条件
always @(Bor sel)begin
out = 1’bx ；
case(sel)
　3’b000：out = b[0] ：
　3’b001：out = b[1] ：
　3’b010：out = b[2] ：
　3’b011：out = b[3] ：
　3’b100：out = b[4] ：
　3’b101：out = b[5 ] ：
　3’b110：out = b[6 ] ：
endcase
end

在这个例子中，综合工具将赋予“x”的值为“不关心”条件。因此当条件seL= 3’b111时，并不能推导出锁存器，即b[7 ]没有输出。如果形式化验证工具不将“x”的赋值视为“不关心”条件，在此条件下则视为锁存器，则将标记出综合网表与RTL的不匹配。

例2　“x”传播
if (A= = 1’bx)
out < = B；
else
out < = C；

在例2中，综合和仿真工具均将“x”视为False条件，因此，“输出”总是值“c”。这里也一定确保在等价性验证时对此有一致的解释。否则RTL和网表就回不匹与，这也是非常重要的。

综合附注
在综合时可以采用指示或附注来指导综合过程，重要的是在进行等价性验证时也要同样解释这些综合附注。

例如，按照定义用VHDL表示的事件描述中的不同分支是相互排斥的，既为用VHDL综合一个事件描述时并没有隐含的优化逻辑。与之相反的，按照定义用Verilog表示的事件描述中的不同选择并不相互排斥，因此，可用Verilog事件描述来综合优化逻辑。对于相互排斥Verilog编码的附注为paralleL-case语句说明此种情况，一个通常的应用就是用Verilog设计状态机，在给定的时间内不能多于一个状态，因此用来对状态机解码的事件描述时，必须使用附注paralleL- case来综合。

VHDL需要考虑事件描述中的表达式的所有不同值，而Verilog并无此要求。若知道事件表达式的所有可能值都已经考虑了，就可以使用综合附注fulL-case语句，这样就不会因为没有所有条件下给寄存器信号赋值而引起锁存器推断错误。

例3　fulL- case附注语句
always @(posedgeclk)
begin out = out ；
　case(sel) / /fulL- case
　2’b00：out = A；
　2’b01：out = B；
　2’b10：out = C；
　endcase
end

综合工具将fulL-case语句附注解释为当seL=“11”时未声明事件不会发生。尽管赋值out=out，综合工具也不会产生锁存器；重要的是在等价性验证时也要有类似的解释，否则它就会在RTL和综合网表间做一个不匹配的标志。

例4　paralleL- case语句附注
always @(Aor b)
begin
　case(sel) //paralle- case
　　A：out = 2’b00；
　　B：out = 2’b11；
endcase
end

综合工具将paralleL-case附注直接解释为两个事件(A和b)是相互排斥的。这避免了优先逻辑推理。但最好能赋给“out”一个明确的默认值以避免任何不匹配。而且，若等价性验证不能辨别parallel-case附注，就会发生不匹配。

时钟定义
等价性验证必须支持RTL编码中用来指定时钟边缘的方式。换句话说，在设计中时钟的定义必须保证综合和等价性验证都能解释时钟的定义。

锁存器推导
要确保所有信号都被初始化，而且当采用事件描述或嵌套描述时，要保证其定义是完全的，一个完全的定义可以防止锁存器的推断错误。

例5 　锁存器的推导
case(sel)　/ / fulL- case
00：begin
　A= 0；
　B= 1；
　end
01：B= 0；
endcase

综合工具将为信号A而不是信号B推导一个锁存器，这是因为B的值在每一个“sel”事件中都给出了确切的定义。确信RTL的目的是为推导出一个锁存器。另一方面，如果等价性验证不理解fulL-case附注，它将为信号A和B推导锁存器，这就导致综合设计和RTL间的不匹配。

事件敏感度
VHDL是一种事件不敏感语言，而Verilog是事件敏感的。在SOC设计中，部分设计可能有不同的资源———VHDL和Verilog，还可能包含不同HDL描述的外部第三方IP。在这种情况下，等价性验证在连接设计和不同语言时，应采用最少限制的命名规则，如连接VHDL实体和Verilog模块时就忽略了事件灵敏度。

等价性验证是在不要求任何测试向量的情况下，同一个设计的两种不同的表述在逻辑上是等价的。但等价性验证不能保证上一个阶段的设计是否正确，它是在假设上一个阶段的设计是正确的基础上进行的一种形式化验证方法。

小 结

片上系统(SOC)的验证已经成为进行设计的一个主要问题，形式化验证技术是它的一个很好的发展方向。本文讨论了在SOC上运用等价性验证不同阶段设计等价时注意的一些问题，以及解决的一些方法。而对于整个片上系统的验证仅靠一种方法是不够的，它需要各种方法结合起来，来对SOC进行验证。