SoC验证方法学研究与应用
2012-09-05华更新刘鸿瑾
吴 军,华更新,刘鸿瑾
(北京控制工程研究所,北京100190)
SoC验证方法学研究与应用
吴 军,华更新,刘鸿瑾
(北京控制工程研究所,北京100190)
SoC系统功能日益复杂,规模也日益庞大,SoC验证面临着前所未有的挑战.对SoC验证方法学进行了研究和总结,包括验证流程、验证层次和验证技术.通过对基于DW 8051的SoC的验证实践,证明了这套验证方法学的可行性和有效性.
SoC;验证方法学;验证流程;验证层次;验证技术
目前SoC的研究和应用已经成为嵌入式计算机进一步发展的重要推动手段,其依托的原动力来自于半导体工艺的长足进步.随着设计复杂度的不断增大,验证变得越来越困难.目前的SoC开发队伍中,验证人员一般是设计人员的2~3倍,验证所花的时间和精力已占整个开发过程80%,验证已经成为整个SoC开发过程的瓶颈.本项目通过对SoC的验证进行了方法的总结和归纳,在此基础上利用对基于DW 8051微控制器的SoC的进行实践来检验总结和归纳的方法的正确性和有效性,目的是掌握SoC的验证体系,形成一套可信的验证流程.
SoC的运算核心基于Synopsys®DW 8051 IP,在此基础上增加了多种星敏感器的外围接口逻辑.它具有以下的特点以及相对基本的8051微控制器的增强特性[1]:
(1)兼容工业标准的803x/805x
1)标准的8051指令集;
2)参数可选的全双工串口;
3)3个Timer;
(2)高速体系结构
1)每个指令周期为4个时钟周期;
2)指令执行时间相比标准的8051可以有平均2.5倍的提高;
3)双数据指针.
1 验证方法学[2-6]
验证与测试的区别首先需要明确,因为在实践中往往存在有意混淆的倾向.在嵌入式软件开发过程中,由于技术手段的原因,往往会不太刻意去区分测试(testing)与验证(verification),虽然两者之间的区别原理上也是存在的,但是SoC本身是一个软件和硬件的混合体,本质是用软件实现了一个硬件,从最终的产品形态上和传统的ASIC并无差异,从来没有任何理论会认为开发ASIC的过程是在开发一个软件.SoC的开发过程存在采用EDA软件与板级硬件两种环境,实践中大量存在利用测试代替验证、重测试轻验证等不正确的做法(测试速度快,相对容易,但可控性差,很难达到高覆盖率),所以必须严格区分.
测试的目的是去考察设计是否被正确“制造”出来,而验证是为了确保这个设计能够满足需求规格说明所定义的功能和时序.图1描述了测试与验证之间的关系.简单来说,在EDA软件环境下叫做验证,硬件实现后叫做测试.由于EDA软件的特性,验证可控性高,可以做到高覆盖率,同时在EDA环境下所有的功能和时序特性和硬件测试完全一致,这是和传统嵌入式软件测试的最大不同,也是最大的优点.
图1 测试与验证之间的关系Fig.1 Relationship between test and verification
验证计划是整个验证的起点,它体现了验证方法学的各个层面.作为整个验证的需求规格说明,它来源于设计的规格说明.设计的规格说明相当于是验证计划的标准参考模型(golden reference).在验证计划中,需要明确以下几个方面,同时也是验证计划中必须包括的项目:
1)验证流程; 2)验证目标; 3)验证层次; 4)验证技术.
1.1 验证流程
验证流程除了要说明验证的计划流程之外,还要明确验证的技术流程.计划流程是时间为出发点安排项目的各个节点,技术流程是安排从需求规格说明到项目目标所进行的验证过程.计划流程依照一般的工程节点管理即可.图2是目前的从传统集成电路实现流程引申而来的简化SoC开发技术流程,其中包含了验证工作.
1.2 验证目标
验证往往被认为是永无止境的任务,所以验证计划必须提供整个验证流程成功的标志,也就是验证的终点.一旦这个标志被确定,才能够知道有多少验证用例需要被生成,它们的复杂度以及依赖关系.譬如:一旦RTL通过了所有的验证用例,而且对于覆盖率和故障率达到预先定义的满意值,则这个设计可以被通过了,而不是永无休止的验证.这就是明确验证目标所要达到的目的.
图2 包含验证的简化SoC开发技术流程Fig.2 Simplified SoC design flow with verification
在实际工程中,如果想要一次成功,必须定义在什么样的环境下,什么特点必须被执行到,同时会有什么样的期望反应.验证计划必须定义什么特点是必须被优先验证,什么特点是可选择被验证的.在验证时间流程的压力下,可能会故意从必须一次成功的点中放弃某些验证点,当然这样作必须经过充分的评审.所以在验证目标中需要明确定义以下几点:
(1)功能点提取
这也是验证目标中最难也是最精华部分.传统的做法是从设计说明书中提取功能点,用自然语言来描述.理想的状况是由设计工程师和验证工程师来共同完成,设计工程师在设计阶段就用文档的形式定义所设计的模块有哪些需要被验证,这对于提高验证的完整性有很大帮助,例如对于边界用例(Corner case)的验证就会有很大的帮助.最终,这些功能点由验证工程师将其由自然语言转换为验证用例或形式化的断言.本文将以举例的方式详细介绍基于DW 8051的SoC功能点的提取和描述方式.
(2)功能点响应
也就是正常工作状态下,在相应激励下的状态.
(3)功能点优先级
定义哪些功能点必须被验证,哪些是可选择完成的.
(4)验证结束标志
也就是让设计被验证通过的满意值.例如代码覆盖率和功能覆盖率分别需要达到的指标,通常代码覆盖率和功能覆盖率要求达到80%~90%,更高的指标往往会增加数倍的工作量.
1.3 验证层次
当准备一个验证计划时,需要解决的一个重要问题是要定义被验证设计的粒度和层次.一个设计会隐含地包括几个层次.一些设计会有一个物理分区,例如整个电路板.另外的设计会有一个逻辑分区,例如可综合的单元和块、可重用的 IP核或子系统.如图3所示.每一层的粒度仅仅只会最适合某一个特定的验证目标.更小的分区更容易被验证,因为它们提供更好的可控性和可观察性.比起一个SoC芯片,在单元级更容易设计环境和状态组合,更容易观察是否响应为所期望的.如果更大的分区能够被充分地验证,其中包含的更小分区的完整性是默认地被验证的,当然这是以更差的可控性和可观测性为代价.对于验证层次的规划,在验证计划中有以下三点需要注意.
(1)分区划分
任何待验证的分区都必须要有相对稳定的接口和实际意义的功能.如果接口一直在变化或者功能从一个分区移到另一个分区,那么验证用例将不得不随之改变,从而影响验证进度.一旦已经决定了某一个待验证的特定分区,它们之间的接口和整个功能必须被尽早定义以及尽可能保持稳定.理论上,每一个待验证的分区应该有各自的说明文档,或者至少在整个规格说明中有自己独立一节来说明.
(2)单元验证
与传统的嵌入式软件的单元不同,使用硬件描述语言描述的单元往往规模相对较小,一般也不具备有可独立出来的完整功能.而且它们通常也没有一个验证所需要的独立的规格说明.一般来说,单元验证需要特定的验证过程.设计者自己通过提供嵌入单元的断言或在临时的验证平台上,来验证单元的基本操作.验证的目标仅仅是去保证在RTL代码中没有语义错误,以及被操作的基本功能.它并不是为了去建立一个可收敛的验证平台以及得到很高的代码覆盖率.过多的设计单元会使验证过程在单元级耗费太多的时间.每一个单元往往都会需要专门的验证环境,完全没有可移植性,宝贵的验证资源往往耗费不正常的时间,只是为了一直都在变化的接口而去生成激励生成器和响应监视器.所以通常在SoC验证层次规划中,单纯而且大量的单元验证是没有必要的,花费大量的时间去写大量的简单验证用例还不如少一些但更复杂的验证用例.其实在更高一级的子系统中,仍然会需要去验证这些设计单元的完整性.原则上只推荐对一些非常复杂的单元去作专门的验证.
图3 验证层次[6]Fig.3 Verification hierarchy
(3)验证层次
和设计分区是紧密相关的,验证的重点到底应该放在那一层,到底是单元级、模块级或者是(子)系统级,这是验证计划需要明确的.目前的验证理论强调模块级应该是整个验证的重点.模块是由一些单元组成,验证构架需要确保模块级的验证尽可能地充分,如果能够保证模块的功能得到充分验证,其实它内部所包含的子单元的完整性也会被同时得到充分验证,而不需要去单独验证.这种观点仅仅适用于采用硬件描述语言实现的设计,对于嵌入式软件不一定适用.同时这样作还会有两个优点:首先是这样的构架容易建立可裁减和可重用的验证平台;另一点是能够提高验证的效率和产出.
1.4 验证技术
对于验证的结构以及在这个结构内采用哪些验证技术,其实这也是属于验证方法学的范畴.随着SoC设计复杂度的不断提高和设计规模的不断增大,高效的验证技术是提高验证验证完整性、效率和产出的重要因素.目前SoC验证技术可以分为两大类:基于仿真的验证和基于形式化方法的验证.在基于DW8051的SoC的验证中,同时采用了仿真验证和形式化验证.
1.4.1 仿真验证
基于仿真的,以覆盖率作为驱动的验证模型,是目前SoC验证的流行验证技术,基于DW8051的SoC的验证就是建立在这个模型之上的.在这个模型内,具体采用了覆盖率驱动的验证策略,一般以功能覆盖率(functional coverage)目标作为驱动,代码覆盖率(code coverage)仅仅作为参考.通常来说,覆盖率是被作为可信度建立的标准.它被用作为一个安全网络去确保整个验证计划的完整性,同时也确保设计被尽可能的全面验证.当大量的验证用例完成后,覆盖率的测量用来指明整个验证过程的终点.
在基于DW 8051的SOC的验证过程中,使用了基于分层结构的验证方法学,通过将验证平台分成功能不同的几个层面,增强了验证平台的封装性和结构性.此外,引入面向对象验证编程语言(system verilog),可以极大的提高验证工程师的验证能力.如图4中所示.验证用例被运行在整个分层验证环境的顶层.
图4 验证环境的分层结构Fig.4 Verification framework
1.4.1.1 层次结构
(1)信号层
这一层提供给验证对象信号级的连接,在这里验证对象是SoC设计.这一层提供给事件驱动信号名抽象以及连接.根据验证环境的参考信号,这层也会抽象出信号的同步和时序.在基于 DW8051的SoC验证中,验证对象是使用Verilog实现的,验证环境由System Verilog实现,信号层仅仅只包括System Verilog接口声明.System Verilog接口还定义了信号同步(时钟采样)和时序(建立与保持)时间.验证环境使用虚拟信号名而不是实际(通常是仿真器特定的)信号名.这样允许验证对象中信号和路径(包括一些时钟特性)改变后而不影响验证环境和用例.
(2)命令层
命令层包含与出现在验证对象中的不同接口和物理层协议关联的总线功能模块、物理层驱动和监视器.它提供一个到验证对象的固定的、底层的事务接口而不用去考虑验证对象是怎样被实现的.
(3)功能层
功能层提供必要的抽象层去处理应用级的事务和验证验证对象的正确性.不像以接口为基础的物理层,功能事务是更高级操作的一个抽象.一个功能级的事务往往在不同的接口上需要执行多个的命令层的事务.在整个运行时间里,根据具体的配置和激励,比较器会自动去验证验证对象响应的正确性.具体到基于DW8051的SoC的验证过程,比较器的输入是运行程序的指针.同时在功能层,非常重要的事务是去收集功能覆盖率,以此可以指导验证用例的生成.运用了仿真器与System Verilog相互配合生成了一个覆盖率模型,使用它记录了所有事务处理过程中关于验证对象的覆盖率响应信息,可以很容易地做到功能覆盖率的自动统计.
(4)场景层
这层提供了可控和可同步数据和事务生成器,它给验证对象提供了很广泛的激励.不同的生成器被用于在功能层的不同子层提供数据和事务.本层也包括一个验证对象的配置生成器.在基于DW8051的SoC验证项目中,采用了随机激励生成器.
1.4.1.2 覆盖率的指标
以覆盖率作为驱动的验证主要包含两个含义:首先,可以通过覆盖率指标来指导验证工程师对验证用例的生成;其次它可以明确验证的终点.单纯从覆盖率的角度,在SoC验证领域存在这四种覆盖率指标:代码覆盖(code coverage)、功能覆盖(functional coverage)、断言覆盖(asseration coverage)和形式化覆盖(formal coverage).在实际工程中,基于DW 8051的SoC验证中采用了代码覆盖率和功能覆盖率指标作为驱动,在运行过程中收集整个覆盖率信息.代码覆盖率高只是指明验证用例遍历了整个源代码,而不能保证它的正确性和完整性.高的功能覆盖率也并不意味着高的代码覆盖率.在基于DW 8051的SoC验证过程中主要收集了以下一些覆盖率信息.
(1)代码覆盖
1)语句覆盖(Line coverage);
2)表达式覆盖(Statement coverage);
3)区域覆盖(Block coverage);
4)翻转覆盖(Toggle coverage);
5)状态机覆盖(FSM coverage);
6)条件覆盖(Condition coverage);
7)分支覆盖(Branch coverage);
8)路径覆盖(Path coverage).
(2)功能覆盖
代码覆盖和功能覆盖在表1和表4中有统计结果.
1.4.2 形式化验证
形式化的验证理论已有很多年的历史,由于受到运算能力的限制在近几年才开始被用户采用.它主要包括:RTL规则检查、等价性检查和模型检查.
对于以仿真为基础的验证,探索边界用例的成功极大地依赖于验证工程师的个人能力.首先,验证工程师几乎不可能考虑到所有验证场景的组合可能,特别是在大型的设计里.其次,就算是有能力考虑到所有的边界用例,也没有足够的时间去实现.形式化验证隐含遍历整个状态空间或子空间,这样可以得到整个设计或部分设计的一个完整的验证.然而,形式化验证也不是一个万能工具,他所达到的完整验证取决于对设计特点表达的正确性.也就是说,形式化验证不可能证明所有的特性都被验证到.
1.4.2.1 形式化验证和仿真验证的比较
形式化验证,对比于传统的基于仿真的验证,需要更多的数学背景去理解和有效的执行.它们之间最显著的区别是前者不需要输入向量而后者需要.基于仿真的验证过程首先是去生成输入向量然后得到参考输出.而形式化验证过程正好相反.用户开始先规定什么样的行为是需要的然后让形式化检查器去证明.用户根本就不需要去关心输入激励.从另一个方面来说,仿真验证是由输入驱动的,而形式化验证是由输出驱动的.通常输入驱动的方式更加直接简单,所以这也就说明形式化工具使用难度较大,由输出来驱动验证不太容易掌握.
仿真一个向量从概念上可以被认为是验证了输入空间的一个点.从这个观点来看,仿真能够被看作是输入空间的采样.除非所有的点都被采样,否则存在一个错误被遗漏的可能.相对于在点一级工作,形式化验证工作在特性一级.给定一个特性,形式化验证工具会去遍历所有可能的或导致错误的输入和状态条件.如果从输出的观点来看,仿真验证在一个时刻验证一个点而形式化验证验证一组点(一组点组成一个特性).图5指明了它们之间的区别.这也使得在一个时刻验证一组点让形式化验证不那么直接和容易使用.
图5 从输出空间的角度比较仿真验证和形式化验证Fig.5 Comparison between simulation verification and formal verification as viewed from out space
形式化验证的主要缺点是在验证目标到达之前需要大量的内存和非常长的运行时间.当内存容量被超过时,形式化工具经常会屏蔽一些错误,或者只给用户很少的指导去修复错误.所以,一般的形式化验证只能够被用来去遍历中等大小的模块.
1.4.2.2 规则检查
在形式化验证中,应用了规则检查对源代码进行了潜在危险的分析和模型检查.一般的RTL规则检查是根据不同的编程标准和设计规则,由预先定义的规则包去检查用户HDL设计.使用规则检查的优点在于它有异常严格的检查规则,如果程序的确存在问题,几乎不可能通过规则检查.当然它的局限性在于它只能发现一些静态错误,无法发现算法和数据流的错误.另一个局限性在于它用绝对怀疑的态度去报告分析的结果,它会尽量去报告所有可能的问题,所以造成报告出大量可能根本不存在的问题,需要用户从大量的警告和错误报告中去筛选出真正的错误.
1.4.2.3 模型检查
模型检查被认为是最符合形式化的验证技术.模型检查器可以证明关于设计的一个特性或者断言是真或者假.一般来说,使用这个工具有两个用途:一个是用于验证这个设计的某个特定部分,另一个是用来查找一些用户无法想到或者无法用仿真来发现的错误.用户可以使用这些形式化的工具来增强验证.在本项目中,使用了模型检查器对Timer模块进行了功能验证.目前验证并且通过的功能:停止、启动和加计数.同时还对ALU模块进行了验证.
2 基于DW 8051的SoC验证
对于基于DW 8051的SoC验证是为了证明总结的验证方法和流程的有效性,不是本文的重点,所以简略介绍.基于DW8051的SoC的验证流程如图6所示,它也是由图2中简化的SoC开发技术流程通过研究和总结得到的.
图6 基于DW 8051的SOC验证流程Fig.6 DW8051-based SoC verification flow
以验证覆盖率为例,总共收集了以下覆盖率指标作为验证的驱动.
2.1 代码覆盖
其中语句覆盖的结果举例如表1所示.对于未能覆盖的代码均有分析.
2.2 功能覆盖
在本项目中,对功能点的提取和功能覆盖率的验证方法进行了定义,下面举例说明功能点的自然语言描述方法和功能覆盖率的验证方法和结果. 2.2.1 功能点的描述方法
关于指令级这项功能点的自然语言描述如表2所示,表2精确的描述了功能点在设计中发生的时间、位置和期望状态,其他对功能点的描述可以此为标准.
表1 语句覆盖Tab.1 Code coverage
表2 功能点的自然语言描述方法Tab.2 Description of function requirements by nature language
表3精确的描述了中具体到某一个指令的功能点的自然语言描述.
2.2.2 功能覆盖的实现和结果
(1)验证方法
使用了System Verilog实现上述这两个用自然语言描述的功能点,仿真器会根据System Verilog的定义自动得到功能覆盖率值.
(2)验证结果(见表4)
表3 功能点的自然语言描述举例Tab.3 Example of how to use nature language to describe function requirements
表4 功能覆盖率的简单描述Tab.4 Example of function coverage
3 验证总结
通过对基于DW8051的SoC的验证工作,从方法学的角度建立了一个完整的验证系统.在这样一个系统内,可以清晰地知道验证的具体目标和构架,以及在验证过程中,如何根据验证目标的不同去有选择的采取不同的验证技术,同时还将不同验证技术的适用范围做了一个清晰的定义.
本文总结的验证方法和流程,在随后承担的建立FPGA产品第三方验证体系的前期筹划工作中,为国内首次实现的FPGA产品第三方验证流程的制定打下了坚实基础.
[1] Janick B.W riting testbenches:functional verification of HDL models[M].New York:Kluwer Academic Publishes,2003
[2] Andrew P.Functional verification coveragemeasurement and analysis[M].New York:K luwer Academic Publishers,2004
[3] Paul W.Professional verification:a guide to advanced functional verification[M].New York:Kluwer Academic Publishers,2004
[4] Janick B,Eduard Cerny,Alan H,et al.Verification methodology manual for system Verilog[M].New York: Springer Science Business Media,2005
[5] Janick B,W riting testbenches using system verilog [M].New York:Springer Science Business Media,2005
[6] W illiam K L.Hardware design verification:simulation and formal method-based approaches[M].Upper Sodd le River,New Jersey:Prentic-Hall,2005
Verification M ethodology Research and App lication for SoC
WU Jun,HUA Gengxin,LIU Hongjin
(Beijing Institute of Control Engineering,Beijing 100190,China)
The explosion of scale and comp lexity of SoC is currently becom ing a challenge for the SoC verification.The methodology illustrated in this paper is established based on the practice of DW 8051 SoC verification and its suitability and validity has been proved.This methodology includes verification flow,verification level and verification technique.
SoC;verification methodology;verification flow;verification level;verification technique
V249
A
1674-1579(2012)05-0027-07
10.3969/j.issn.1674-1579.2012.05.005
吴 军(1976—),男,高级工程师,研究方向为SoC验证,容错技术,嵌入式计算机;华更新(1965—),男,研究员,研究方向为星载计算机体系结构设计;刘鸿瑾(1980—),男,高级工程师,研究方向为星载计算机设计、SoC设计、抗辐射加固设计.
2012-02-10