适用于形式化验证的断言优化方法

Assertion Optimization Methods for Formal Verification

在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响锥模型不能分析断言中时序关系对状态空间的影响的问题,提出长序列模型,分析形式化验证中断言与状态空间大小的定性关系。在此基础上,提出适用于形式化验证的断言优化方法,方法包含断言逻辑化简、辅助验证逻辑、参考模型和断言禁用条件,并以某商用HDLC IP核为例,对比优化前后的验证结果,证明优化的有效性。

In practical industrial verification scenarios,the limitations of formal verification are mainly reflected in the non-determined results due to state space explosion.The assertion is always the main factor that directly affects the verification results,and the existing assertion optimization methods are not based on the analysis of the relationship between assertions and the size of the state space.This paper proposes a long sequence model to analyze the qualitative relationship between assertions and state space size in formal verification,in response to the problem that the cone of influence cannot analyze the impact of temporal relations in assertions on the state space.Based on the analysis,this paper proposes an assertion optimization method for formal verification,which contains assertion logic simplification,auxiliary verification logic,reference model and assertion disabling condition.In this paper,a commercial HDLC IP core is used as an example to compare the verification results before and after the optimization to prove the effectiveness of the optimization.