1、386 集成电路应用 第 40 卷 第 6 期（总第 357 期）2023 年 6 月Applications创新应用Verification）这两类4，相比于动态仿真，形式化验证不考虑实际应用场景，通过对模块端口信号进行遍历来实现约束范围内所有场景的覆盖因此有着较高的准确性5，此外形式化验证也不需要构建仿真环境，而是通过断言来进行属性验证，找到违反断言的情况6，这大大减少了调试环境所需要的时间，因此适用于SoC中存在风险的模块，对提高验证质量加快项目进度有着十分重要的作用。本文采用形式化属性验证对SoC中的轮询仲裁器（round robin arbiter）模块进行验证，查找模块中存在的问题
2、，然后通过形式化验证的结果反向指导SoC制造相应的场景，以减少芯片中存在的风险。1 轮询仲裁器简介轮询仲裁器（round robin arbiter）在SoC中是数据传输模块，通过握手来对多路的数据进行传递，基本框图如图1所示，运算单元对输入的信0 引言随着芯片复杂度的提升，验证所需要的时间占整个设计的50%以上1，其中通过动态仿真制造随机激励来寻找边界场景会消耗大量的验证时间，此外也无法将尽可能多的场景都遍历到，这往往导致设计中存在的bug无法被及时找出，为芯片的流片和实际的使用带来巨大的问题，因此及时的发现bug，有针对性的构建边界场景就显得尤为重要。目前比较普遍的验证方法是通过UVM搭建
3、仿真环境制造一些定向或者随机的激励来对RTL进行验证，以实现高效的开发与重用2，通过这种方式可以覆盖到大多数的场景，但该种方式对接口信号的遍历有限，因此往往会漏掉一些边界的情况，而且对于一些存在风险的模块无法做出充分的验证，会产生较为严重的后果。形式化验证是一种分析系统属性的数学方式3，分为FPV（Formal Property Verification）和MFV（Mainstream Formal 作者简介：晏阳，上海光流智能科技有限公司，苏州涌现智能科技有限公司；研究方向：芯片设计验证和仿真。毕泽家，上海光流智能科技有限公司，苏州涌现智能科技有限公司；研究方向：芯片设计验证和仿真。收稿日期
4、：2023-03-27；修回日期：2023-05-22。摘要：阐述在验证芯片复杂场景的过程中，往往会由于激励的仿真时间过长或随机化程度不够，从而丢失掉部分的边界情况。形式化验证是一种通过数学的方式来对待测设计进行验证的方法，可以对模块的接口信号进行遍历，从而覆盖其约束范围内所有场景。通过形式化属性验证，对SoC中的轮询仲裁器模块进行验证，通过其得到的违例结果，反向指导SoC制造相应的激励，缩短了寻找边界场景的时间，大大提高了验证效率。关键词：形式化验证，轮询仲裁器，定向激励。中图分类号：TN402，TP391.41 文章编号：1674-2583(2023)06-0386-04DOI：10.19
5、339/j.issn.1674-2583.2023.06.168文献引用格式：晏阳，毕泽家.形式化验证在加速动态仿真过程中的应用J.集成电路应用,2023,40(06):386-389.形式化验证在加速动态仿真过程中的应用晏阳1,2，毕泽家1,2（1.上海光流智能科技有限公司，上海 201210；2.苏州涌现智能科技有限公司，江苏 215211）Abstract This paper describes that some boundary cases are often lost due to the long simulation time of excitation or the ins
6、ufficient randomization degree in the process of verifying complex chip scenes.Formal verification is a method to verify the design under test in a mathematical way.It can toggle the interface signal of the module to cover all its scenes.In this paper,formal property verification is used to verify t
7、he round robin arbiter module in System on Chip(SoC).The violation results obtained can be used to reverse guide the SoC to produce the corresponding excitation,which reduces the time to find the boundary scene and greatly improves the verification efficiency.Index Terms formal verification,round ro
8、bin arbiter,directed excitation.Application of Formal Verification to Accelerate Dynamic SimulationYAN Yang1,2,BI Zejia1,2(1.Shanghai Optical Flow Intelligence Technologies Co.,Ltd.,Shanghai 201210,China.2.Suzhou Emergetech Intelligent Technology Co.,Ltd,Jiangsu 215211,China.)Applications 创新应用集成电路应用
9、 第 40 卷 第 6 期（总第 357 期）2023 年 6 月 387号进行运算，当运算完成后发出请求给到轮询仲裁器，轮询仲裁器会按照顺序接收运算单元的请求并返回相应的响应信号，握手成功后将运算单元算出的数据依次传出到下一个模块，来保证数据可以被依次上传。然而在实际工作中，轮询仲裁器常常会由于没有及时握手或者对于握手的处理机制不够完善，导致接收到的请求信号长时间挂起，造成数据丢失或数据在接口处堵住，芯片长时间无法返回结果。由于动态仿真无法将边界情况遍历完全，而轮询仲裁器往往会在一些比较边界的场景发生堵住的情况，因此，在这里采用形式化属性验证然后指导动态仿真制造相应的场景，以确保轮询仲裁器的
10、可靠性。2 动态仿真环境的搭建SoC的动态仿真环境采用UVM验证方法学，如图2所示，数据的发送是通过Driver将数据包驱动到接口。然后，进入RTL中的运算单元，运算单元算出的结果经过轮询仲裁器传出。最终，通过Scoreboard检查输出接口的信号来确认模块的交互是否存在问题。3 形式化属性验证动态仿真常常会因为没有覆盖到边界的场景而出现bug逃逸的风险，如图3所示，在其测试过程中信号经过的RTL都是固定的状态，要想尽可能覆盖到更多的情况需要加入大量的激励或消耗时间进行随机。形式化属性验证如图4所示，可以将RTL中所有的状态都遍历到，因此可以更加有效的发现bug，但对于一些复杂的设计会消耗大量
11、的内存和时间，甚至会因为内存不足而终止验证。3.1 形式化属性验证的流程轮询仲裁器的形式化属性验证的验证流程如图5所示。首先，完成调度脚本，设置轮询仲裁器模块编译参数以及时钟和复位，通过断言来对其各个信号的时序关系进行定义，在执行检查之后，对待出现的违例情况需要进一步确认，如果不符合实际图1 轮询仲裁器基本框图图2 动态仿真环境图3 动态仿真到达的状态图4 形式化属性验证到达的状态388 集成电路应用 第 40 卷 第 6 期（总第 357 期）2023 年 6 月Applications创新应用场景需要添加assume对信号进行约束7，如果违例会出现在实际的应用场景，则需要对RTL进行进一步
12、修改。3.2 SVA文件的编写为了确定RTL的行为是否符合预期，需要通过断言对其内部信号的行为进行判断，如果断言发生违例，则说明设计行为存在问题。轮询仲裁器的验证主要有以下几点。（1）进入的多个request请求信号都能够正常进入并依次完成握手。（2）完成握手后运算单元的计算结果会从轮询仲裁器中传出。（3）当没有request请求信号进入时轮询仲裁器的状态不会发生改变，且不会有信号传出。（4）当有request请求信号进入轮询仲裁器时，其轮询状态发生改变。3.3 SVA的执行过程与初步结果分析通过执行脚本启动形式化验证工具，将3.2节的断言转换成property，形式化验证通过自带穷举算法对D
13、UT发出激励并尝试给出反例，经过形式化属性验证之后的断言，最后的状态都为proven（如表1所示），没有得到反例，因此可以认为在正常工作状态下没有bug。形式化属性验证在一般的验证过程中是只将SVA文件中的复位信号进行约束再定义时钟，由于芯片随时可能会处于异常状态，因此复位行为会在任何时刻发生，仅仅只对复位之后稳定状态下的行为进行验证是不够充分的，通过取消复位的约束使得复位可以发生在任何时刻，往往会发现部分异常状态下的bug。3.4 不约束的SVA结果分析在这里我们将同样的断言不对复位进行约束，如表2所示，经过形式化属性验证结果显示出了大量的违例，这是由于复位可以随时发生造成的，其中部分的违例
14、是复位产生的正常行为，需要添加其图5 形式化属性验证检查流程表1 验证结果（对rstn进行约束）表2 验证结果（不进行rstn约束）Applications 创新应用集成电路应用 第 40 卷 第 6 期（总第 357 期）2023 年 6 月 389他约束进行限制，同时个别违例也存在复位带来的风险，例如断言assert_five_request_2_3，该断言的目的是为了验证当request进入时，轮询仲裁器内部的状态可以正常跳转，分析其波形（如图6所示）。可以看到，当request信号在传输过程中轮询仲裁器发生复位，会导致其request信号无法被正常响应因此无法跳转到下一个状态，这使得数
15、据无法正常传输，甚至可能会导致后面的数据将传输通道堵住，造成严重的问题。4 SoC的激励制造通过反例的波形可以看到，在运算单元传出request的过程中进行复位会造成一定的问题，因此SoC在动态仿真过程中，在request拉高后经过一拍然后拉低复位信号，即可造出和违例断言相同的场景，最后的波形如图7所示。从波形中可以看出，request_d信号被从中间打断，产生了两个request_d的信号，但实际的响应信号只会握手一次，多出的request信号会从轮询仲裁器中传出，由于没有握手会一直悬挂，在造成数据异常的同时也会导致之后的request信号没有被及时的处理，使得数据通路堵塞。这种场景在验证之
16、初的动态仿真过程中是没有被测到的，主要是由于复位行为在一个request拉起来的过程中发生，这是一种特殊时序下的行为，因此，很难通过随机的激励直接覆盖到。5 形式化属性验证结合动态仿真的优势编写调度脚本并进行形式化属性验证可快速定位到RTL存在风险的场景，再通过波形反向制造SoC的激励便可对场景进行复现，如图8所示，通过该流程相比于随机激励，能够节省70%的时间便可以遇到该种场景。因此通过形式化属性验证指导SoC制造定向激励可以更加快速有效的查找到RTL中的bug，缩短验证周期，大大提高验证效率。6 结语 通过形式化属性验证对轮询仲裁器进行了验证，及时发现不加约束断言中的隐患，通过指导SoC生
17、成相应的激励，确定了RTL中存在的bug，加快了验证速度，保证了轮询仲裁器模块的质量。由于形式化属性验证可以覆盖到模块约束范围内的所有场景。因此对SoC中存在风险的模块进行验证，可以有效地发现RTL中的边界情况，指导SoC制造出相应的激励来对其进行确认，在验证中期可以减少模块存在的风险，加快验证速度。参考文献1 朱峰,鲁征浩,朱青.形式化验证在处理器浮点运算单元中的应用J.电子技术应用,2017,43(02):29-32.2 赵赛,闫华,丛红艳,张艳飞.基于UVM的PCI Express总线控制器验证平台J.电子与封装,2022,22(02):84-88.3 BORCHERS K,FIRCHA
18、U T.Formal Property Verification of a Remote Memory Access Protocol IP-Core,2022C.IEEE Aerospace Conference(AERO),2022.4 赵亚雪,植玉,梁其锋,石义军.保序模块的formal fpv验证J.电子技术应用,2022,48(08):38-41+45.5 朱健,胡凯,张伯钧.智能合约的形式化验证方法研究综述J.电子学报,2021,49(04):792-804.6 ABBAS H,MITTELMANN H,FAINEKOS G.Formal property verification
19、 in a conformance testing framework,2014C.Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign(MEMOCODE),2014.7 CRISTIA M,FRYDMAN C.Formal and semi-formal verification of a web voting systemJ.International Journal of Web Information Systems,2015,11(2):183-204.图6 断言违例波形图7 SoC动态仿真生成的波形图8 形式化属性验证+定向激励与随机激励发现bug的时间比较
