This article has been accepted for publication in a future issue of this journal, but has not been fully edited. Content may change prior to final publication. 1 Word Level Predicate Abstraction and Refinement Techniques for Verifying RTL Verilog

Abstract—As a first step, most model checkers used in the hardware industry convert a high-level register transfer level (RT-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 RT-level 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 compu-tation 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 prob-lem by computing 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 significant improvements on a set of benchmarks. Index Terms—Register transfer level (RTL), verification, model checking, predicate abstraction, refinement, satisfiability (SAT). I