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.

翻译：IC3是一种著名的用于安全验证的比特级框架。通过引入数据路径抽象，可以显著提高硬件验证的效率。然而，数据路径抽象会导致抽象粒度较粗，所有数据路径操作都被近似为无解释函数。这种抽象层级尽管有用，但在验证过程中需要广泛探索冗余的抽象状态空间，从而增加计算负担。本文提出了一种名为数据路径传播的新方法。该方法利用具体常数值迭代计算相关数据路径操作及其关联的无解释函数的结果，同时在抽象状态空间中生成潜在有用的数据路径传播引理，并收紧数据路径抽象。通过这一技术，抽象状态空间得以缩减，验证效率显著提升。我们实现了所提出的方法并进行了大量实验。与现有最先进的验证工具相比，实验结果显示我们的方法具有显著的改进效果。