Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs
Empirical Evaluation of IC3-Based Model Checking Techniques on Verilog RTL Designs
复制标题
Verilog RTL 设计中基于 IC3 的模型检查技术的实证评估
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
K. Sakallah
中科院分区：
文献类型：
--
作者：
Aman Goel;K. Sakallah
基于IC3的算法已经成为一种有效的可扩展的硬件模型检测方法。在这篇文章中，我们评估了六种基于IC3的模型检查器在一组公开可用的和专有的工业Verilog RTL设计上的实现。我们检查的六个验证器中有四个在位级操作，两个使用抽象来利用字级RTL语义。总体而言，使用数据抽象的词级验证器的表现优于其他验证器，尤其是在大型工业设计上。分析帮助我们确定了关于这些工具背后的技术、它们的优势和劣势、差异和共同点以及改进机会的几个关键见解。
IC3-based algorithms have emerged as effective scalable approaches for hardware model checking. In this paper we evaluate six implementations of IC3-based model checkers on a diverse set of publicly-available and proprietary industrial Verilog RTL designs. Four of the six verifiers we examined operate at the bit level and two employ abstraction to take advantage of word-level RTL semantics. Overall, the word-level verifier employing data abstraction outperformed the others, especially on the large industrial designs. The analysis helped us identify several key insights on the techniques underlying these tools, their strengths and weaknesses, differences and commonalities, and opportunities for improvement.