Leveraging Datapath Propagation in IC3 for Hardware Model Checking

TL;DR

This paper introduces datapath propagation in IC3, a hardware model checking framework, to improve verification efficiency by reducing abstract state space through concrete value propagation and lemma generation.

Contribution

It presents a novel datapath propagation technique that tightens abstraction and enhances efficiency in IC3-based hardware verification.

Findings

Significant reduction in verification time compared to state-of-the-art methods

Effective use of concrete values to tighten datapath abstraction

Improved scalability in hardware model checking

Abstract

IC3 is a famous bit-level framework for safety verification. By incorporating datapath abstraction, a notable enhancement in the efficiency of hardware verification can be achieved. However, datapath abstraction entails a coarse level of abstraction where all datapath operations are approximated as uninterpreted functions. This level of abstraction, albeit useful, can lead to an increased computational burden during the verification process as it necessitates extensive exploration of redundant abstract state space. In this paper, we introduce a novel approach called datapath propagation. Our method involves leveraging concrete constant values to iteratively compute the outcomes of relevant datapath operations and their associated uninterpreted functions. Meanwhile, we generate potentially useful datapath propagation lemmas in abstract state space and tighten the datapath abstraction. With this technique, the abstract state space can be reduced, and the verification efficiency is significantly improved. We implemented the proposed approach and conducted extensive experiments. The results show promising improvements of our approach compared to the state-of-the-art verifiers.