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

Application of Formal Verification to Accelerate Dynamic Simulation

阐述在验证芯片复杂场景的过程中,往往会由于激励的仿真时间过长或随机化程度不够,从而丢失掉部分的边界情况。形式化验证是一种通过数学的方式来对待测设计进行验证的方法,可以对模块的接口信号进行遍历,从而覆盖其约束范围内所有场景。通过形式化属性验证,对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.