Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction
Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction
复制标题
使用具有语法引导抽象的 IC3 对 Verilog RTL 进行模型检查
DOI：
10.1007/978-3-030-20652-9_11
复制
发表时间：
2019
影响因子：
7.4
通讯作者：
K. Sakallah
中科院分区：
文献类型：
--
作者：
Aman Goel;K. Sakallah
虽然用于硬件模型检查的基于位级IC3的算法代表了对先前方法的重大进步，但它们对命题子句学习的依赖为具有宽数据路径和复杂字级操作的RTL设计带来了可扩展性问题。在本文中，我们提出了一种新的技术，结合IC3与语法指导的抽象（SA），允许可扩展的字级模型检查使用SMT求解器。SA定义的抽象隐式从语法的输入问题，具有高粒度和抽象的状态空间大小完全独立于设计的寄存器的位宽。我们展示了如何有效地集成IC 3与SA，并证明其有效性的一套开源和工业Verilog RTL设计。此外，SA很容易与使用非解释函数的数据抽象保持一致。我们演示了如何IC3+SA与数据抽象允许推理，是完全独立的变量的位宽，并成为可扩展的状态空间大小或操作的复杂性无关。
While bit-level IC3-based algorithms for hardware model checking represent a major advance over prior approaches, their reliance on propositional clause learning poses scalability issues for RTL designs with wide datapaths and complex word-level operations. In this paper we present a novel technique that combines IC3 with syntax-guided abstraction (SA) to allow scalable word-level model checking using SMT solvers. SA defines the abstraction implicitly from the syntax of the input problem, has high granularity and an abstract state-space size completely independent of the bit widths of the design’s registers. We show how to efficiently integrate IC3 with SA, and demonstrate its effectiveness on a suite of open-source and industrial Verilog RTL designs. Additionally, SA aligns easily with data abstraction using uninterpreted functions. We demonstrate how IC3+SA with data abstraction allows reasoning that is completely independent of the bit width of variables, and becomes scalable irrespective of the state-space size or complexity of operations.