Agentic-IC3：在IC3模型检查中实现语义证明搜索

中文摘要 AI 辅助

IC3是一种最先进的硬件模型检查算法，通过增量构建由一组引理组成的归纳不变量来证明安全属性。其有效性依赖于识别有用引理并指导证明搜索的泛化启发式方法。然而，许多领先的IC3硬件模型检查器在降低后的位级表示上运行，在这种表示中，高层设计关系难以被利用来进行泛化。那些在更高层级运行的检查器在利用高层设计结构和语义方面仍然受限。我们提出了Agentic-IC3，它构建在Pono的字级模型检查基础设施之上，将语言模型代理集成到IC3中，利用寄存器传输级（RTL）设计信息来指导语义证明搜索。该框架为持久的IC3后端提供了一个面向代理的接口，使代理能够在整个验证过程中与显式且不断演变的证明状态进行交互。在连续的证明义务中，代理将中间证明状态和求解器反馈与RTL关联起来，并通过SAT和UNSAT泛化提出高层引理。除了泛化之外，代理还可以引入派生的观测信号来简洁地表达设计关系并获得更具信息量的反馈，并且可以回溯以修订导致无成效证明分支的提议。后端在更新证明状态之前检查提议，从而保持可靠性并为进一步推理提供反馈。在涵盖安全信息流验证以及通信协议、处理器和功能单元的功能验证的14个基准测试套件上，Agentic-IC3在一小时超时内解决了10个案例，其中包括所有三个评估基线（rIC3、Pono-IC3Bits和A-IC3）均未解决的4个案例。

英文摘要

IC3 is a state-of-the-art algorithm for hardware model checking that proves safety properties by incrementally constructing an inductive invariant consisting of a set of lemmas. Its effectiveness depends on generalization heuristics that identify useful lemmas and guide proof search. However, many leading IC3 hardware model checkers operate on lowered, bit-level representations, where high-level design relationships are difficult to exploit for generalization. Those operating at a higher level remain limited in exploiting high-level design structure and semantics. We present Agentic-IC3, built on Pono's word-level model-checking infrastructure, which integrates a language-model agent into IC3 to guide semantic proof search using register-transfer-level (RTL) design information. The framework exposes an agent-oriented interface to a persistent IC3 backend, allowing the agent to interact with an explicit, evolving proof state throughout verification. Across successive proof obligations, the agent relates intermediate proof states and solver feedback to the RTL and proposes high-level lemmas through both SAT and UNSAT generalization. Beyond generalization, the agent can introduce derived observation signals to express design relationships succinctly and obtain more informative feedback, and backtrack to revise proposals that lead to unproductive proof branches. The backend checks proposals before updating the proof state, preserving soundness and providing feedback for further reasoning. On a suite of 14 benchmarks spanning security information-flow verification and functional verification of communication protocols, processors, and functional units, Agentic-IC3 solves 10 cases within a one-hour timeout, including 4 unsolved by all three evaluated baselines: rIC3, Pono-IC3Bits, and A-IC3.

发表机构

• Princeton University（普林斯顿大学）

机构由 AI 辅助整理，请以论文原文为准。