超越引理共享——属性定向可达性的新型并行化策略
Beyond Lemma Sharing -- Novel Parallelization Strategies for Property Directed Reachability
- Huawei Technologies Switzerland AG（华为瑞士技术有限公司）
机构由 AI 辅助整理，请以论文原文为准。
中文总结 AI 辅助
针对PDR并行化可扩展性难题，提出抢占式传播和ARPOS两种新策略，并在rIC3上验证，显著优于经典引理共享。
中文摘要 AI 辅助
属性定向可达性（PDR）是一种常用的自动化硬件模型检测技术，然而高效地并行化它仍然是一个重大挑战。现有的方法，如引理共享，随着处理器数量的增加往往面临可扩展性受限的问题。在这项工作中，我们提出了两种新颖的基于共享的并行化策略：抢占式传播和ARPOS，并将它们的性能与经典的引理共享进行了比较。为此，我们为最先进的rIC3硬件模型检测器开发了一个基于MPI的异步消息传递框架。在2025年硬件模型检测竞赛基准上的实验结果表明，我们的抢占式传播策略相比经典的引理共享带来了显著的性能提升。
英文摘要
Property Directed Reachability (PDR) is a commonly used technique for automated hardware model checking, yet efficiently parallelizing it remains a significant challenge. Existing approaches, such as lemma sharing, often suffer from limited scalability as processor counts increase. In this work, we present two novel sharing-based parallelization strategies, preemptive propagation and ARPOS, and compare their performance with classical lemma sharing. To this end, we develop an asynchronous MPI-based message passing framework for the state-of-the-art rIC3 hardware model checker. Experimental results on the 2025 Hardware Model Checking competition benchmark demonstrate that our preemptive propagation strategy yields a significant performance boost over classical lemma sharing.
