Formal sequential equivalence checking of digital systems by symbolic simulation
Formal sequential equivalence checking of digital systems by symbolic simulation
复制标题
通过符号模拟对数字系统进行形式顺序等价检查
DOI：
10.0253/tuprints-00000113
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Gerd Ritter
中科院分区：
文献类型：
--
作者：
Gerd Ritter
提出了一种通过符号模拟在不同级别的抽象级别进行序性验证的新方法。自动正式验证工具已用于等效检查RT级别的结构描述及其相应的行为规格。已将商业合成工具的栅极级别的结果与行为或结构RT级别的规格进行了比较。该规范不必合成或循环等同于实施。此外，提出了该方法将来应用于财产验证。符号模拟沿两个描述中的逻辑一致路径进行引导，以进行比较。为了找到准确性和速度之间的良好妥协，使用了不同等价检测技术的开放库。基于决策图（OBDD）技术检测等效的角案箱。通过使用其他等效检测技术的结果，并仅通过决策图表示验证问题的一小部分，可以避免图形爆炸。通过在等效类中通知检测到的关系而不是操纵符号术语，可以使所有技术的合作以及良好的调试支持可行。
A new approach to sequential verification of designs at different levels of abstraction by symbolic simulation is proposed. The automatic formal verification tool has been used for equivalence checking of structural descriptions at rt-level and their corresponding behavioral specifications. Gate-level results of a commercial synthesis tool have been compared to specifications at behavioral or structural rt-level. The specification need not be synthesizable nor cycle equivalent to the implementation. In addition, a future application of the method to property verification is proposed. Symbolic simulation is guided along logically consistent paths in the two descriptions to be compared. An open library of different equivalence detection techniques is used in order to find a good compromise between accuracy and speed. Decision diagram (OBDD) based techniques detect corner-cases of equivalence. Graph explosion is avoided by using the results of the other equivalence detection techniques and by representing only small parts of the verification problem by decision diagrams. The cooperation of all techniques as well as good debugging support are made feasible by notifying detected relationships at equivalence classes instead of manipulating symbolic terms.