形式化验证在加速动态仿真过程中的应用  

Application of Formal Verification to Accelerate Dynamic Simulation

作　　者：晏阳 毕泽家 YAN Yang;BI Zejia(Shanghai Optical Flow Intelligence Technologies Co.,Ltd.,Shanghai 201210,China;Suzhou Emergetech Intelligent Technology Co.,Ltd,Jiangsu 215211,China)

机构地区：[1]上海光流智能科技有限公司,上海201210 [2]苏州涌现智能科技有限公司,江苏215211

出　　处：《集成电路应用》2023年第6期386-389,共4页Application of IC

摘　　要：阐述在验证芯片复杂场景的过程中,往往会由于激励的仿真时间过长或随机化程度不够,从而丢失掉部分的边界情况。形式化验证是一种通过数学的方式来对待测设计进行验证的方法,可以对模块的接口信号进行遍历,从而覆盖其约束范围内所有场景。通过形式化属性验证,对SoC中的轮询仲裁器模块进行验证,通过其得到的违例结果,反向指导SoC制造相应的激励,缩短了寻找边界场景的时间,大大提高了验证效率。This paper describes that some boundary cases are often lost due to the long simulation time of excitation or the insufficient 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 the 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.

关 键 词：形式化验证 轮询仲裁器 定向激励 

分 类 号：TN402[电子电信—微电子学与固体电子学] TP391.41[自动化与计算机技术—计算机应用技术]