Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog
复制标题
用于验证 RTL Verilog 的字级谓词抽象和细化技术
DOI：
10.1109/tcad.2007.907270
复制
发表时间：
2008
影响因子：
2.9
通讯作者：
E. Clarke
中科院分区：
文献类型：
--
作者：
Himanshu Jain;D. Kroening;N. Sharygina;E. Clarke
作为第一步，硬件行业中使用的大多数模型检查器将高级寄存器传输级（RTL）设计转换为网表。然而，在网表级别操作的算法不能利用更高抽象级别的结构，因此可扩展性较低。硬件描述语言（如Verilog）的RTL类似于具有硬件设计的特殊功能（如位向量算术和并发性）的软件程序。本文使用谓词抽象，软件验证技术，验证RTL Verilog。在将谓词抽象应用于电路时存在两个挑战：1）在存在大量谓词的情况下的抽象模型的计算和2）用于抽象细化的合适的字级谓词的发现。我们使用一种称为谓词聚类的技术来解决第一个问题。我们解决第二个问题，通过计算Verilog语句的最弱的先决条件，以获得新的字级谓词在抽象细化。我们比较我们的技术与本地化减少，网表级抽象技术的性能，并报告一组基准测试的改进。
As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels and, thus, are less scalable. The RTL of a hardware description language such as Verilog is similar to a software program with special features for hardware design such as bit-vector arithmetic and concurrency. This paper uses predicate abstraction, a software verification technique, for verifying RTL Verilog. There are two challenges when applying predicate abstraction to circuits: 1) the computation of the abstract model in presence of a large number of predicates and 2) the discovery of suitable word-level predicates for abstraction refinement. We address the first problem using a technique called predicate clustering. We address the second problem by computing the weakest preconditions of Verilog statements in order to obtain new word-level predicates during abstraction refinement. We compare the performance of our technique with localization reduction, a netlist-level abstraction technique, and report improvements on a set of benchmarks.