SAT-based Property Directed Reachability (PDR) has become the key algorithmic development for unbounded model checking of gate-level sequential circuits, but it can be inefficient when applied to word-level problems with heavy arithmetic logic. To address this issue, word-level abstraction is often performed by replacing a whole set of signals with unconstrained new primary inputs. This paper introduces PDR-WLA, a word-level abstraction-refinement algorithm integrated into a modified PDR implementation. The algorithm uses efficient refinement and re-uses reachability information across iterations of refinement. PDR-WLA was implemented in ABC and evaluated on a large set of industrial Verilog designs. Experimental results show significant speedups on hard problems compared to the original PDR and to a naive word-level abstraction-refinement method.

Methods for word-level model checking based on purely bit-level techniques have difficulties with heavy arithmetic logic. Word-level and SMT approaches often are limited by relying on (incomplete) bounded model checking. UFAR, a hybrid word- and bit-level approach, addresses these issues, taking advantage of modern bit-level sequential techniques while heavy arithmetic logic is addressed by word-level abstraction and the use of uninterpreted function (UF) constraints. The methods and efficiency improvements developed for UFAR enabled it to prove 2422 of a set of 2492 industrial sequential model checking problems within a 1-hour limit, while a bit-level model checker super prove completed only 2115 of these within the same limit.

SystemC is a de-facto standard for modeling system-level designs in the early design stage. Verifying SystemC designs is critical in the design process since it can avoid error propagation down to the final implementation. Recent works exploit the software model checking techniques to tackle this important issue. But they abstract away relevant semantic aspects or show limited scalability. In this paper, we devise a symbolic model checking technique using bounded model checking and induction to formally verify SystemC designs. We introduce the notions of behavioral states and transitions to guarantee the soundness of our approach. The experiments show the scalability and the efficiency of our method.