Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

📄 arXiv: 2512.06850v1 📥 PDF

作者: Hansa Mohanty, Vaisakh Naduvodi Viswambharan, Deepak Narayan Gadde

分类: cs.LO, cs.AI, cs.AR

发布日期: 2025-12-07

备注: To appear at the 37th IEEE International Conference on Microelectronics (ICM), December 14-17, 2025, Cairo, Egypt

💡 一句话要点

提出一种可扩展的RTL级浮点算术形式化验证方法，结合AI辅助提升验证效率。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 浮点算术 RTL验证 模型检查 AI辅助验证 人机协同 芯片设计 硬件验证

📋 核心要点

  1. 现有浮点验证方法依赖高级C模型，存在抽象差距和转换开销，限制了RTL级验证的可扩展性。
  2. 提出直接RTL-to-RTL模型检查方法，结合分治策略和反例引导细化，实现更高效的验证。
  3. 引入AI辅助的形式化属性生成，通过人机协同提升验证覆盖率和效率，验证过程更鲁棒。

📝 摘要（中文）

浮点算术的形式化验证由于其非线性行为以及控制和数据通路逻辑的紧密耦合而极具挑战性。现有方法通常依赖于高级C模型进行等价性检查，但这引入了抽象差距、转换开销，并限制了RTL级别的可扩展性。为了解决这些挑战，本文提出了一种可扩展的方法，使用直接RTL-to-RTL模型检查，针对黄金参考模型验证浮点算术。该方法采用分而治之的策略，将验证分解为模块化阶段，每个阶段由辅助断言和引理捕获，共同证明一个主要的正确性定理。反例（CEX）引导的细化用于迭代地定位和解决实现缺陷，而有针对性的故障注入验证了验证过程对精度关键数据通路错误的鲁棒性。为了评估可扩展性和实用性，该方法扩展了基于Agentic AI的形式化属性生成，将大型语言模型（LLM）驱动的自动化与人机协同（HITL）细化相结合。覆盖率分析通过比较RTL-to-RTL模型检查和独立RTL验证设置中的手写和AI生成的属性来评估该方法的有效性。结果表明，直接RTL-to-RTL模型检查比独立验证实现了更高的覆盖率效率，并且需要更少的断言，尤其是在与通过HITL指导细化的AI生成的属性结合使用时。

🔬 方法详解

问题定义：论文旨在解决浮点算术在RTL（Register Transfer Level）级形式化验证中面临的可扩展性问题。现有方法通常依赖于高级C模型作为参考，进行等价性检查，但这种方法引入了抽象层面的差异，增加了转换的复杂度和开销，并且难以充分覆盖RTL设计的细节，导致验证效率低下。

核心思路：论文的核心思路是采用直接的RTL-to-RTL模型检查方法，避免使用高级抽象模型，直接将RTL实现与黄金参考模型进行比较。通过分而治之的策略，将复杂的验证任务分解为多个模块化的子任务，并使用辅助断言和引理来逐步证明整体的正确性。此外，利用反例引导的细化过程，迭代地定位和修复实现中的缺陷。

技术框架：该方法包含以下主要阶段：1) 模块化分解：将浮点算术的验证分解为多个模块，例如加法、乘法等。2) 属性生成：使用人工编写或AI生成的形式化属性来描述每个模块的预期行为。3) RTL-to-RTL模型检查：使用模型检查器验证RTL实现是否满足生成的属性，并与黄金参考模型等价。4) 反例引导细化：如果模型检查失败，则利用反例信息定位错误，并修改RTL实现或属性。5) AI辅助属性生成与人机协同：利用大型语言模型自动生成属性，并通过人工审查和修改来提高属性的质量和覆盖率。

关键创新：该方法最重要的创新点在于直接在RTL级别进行模型检查，避免了抽象带来的误差和转换开销。此外，结合AI辅助的属性生成，可以显著提高验证效率和覆盖率。与现有方法相比，该方法更接近硬件实现，能够更有效地发现和修复RTL设计中的缺陷。

关键设计：论文中关键的设计包括：1) 辅助断言和引理的设计：这些断言和引理用于捕获每个模块的预期行为，并逐步证明整体的正确性。2) 反例引导细化的策略：该策略用于迭代地定位和修复实现中的缺陷。3) AI辅助属性生成的prompt工程：设计合适的prompt，引导LLM生成高质量的形式化属性。4) 人机协同的流程：人工审查和修改AI生成的属性，确保属性的正确性和覆盖率。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，直接RTL-to-RTL模型检查比独立的RTL验证实现了更高的覆盖率效率，并且需要更少的断言。结合AI生成的属性，并通过人机协同进行细化，可以进一步提高验证效率和覆盖率。具体性能数据未知，但整体验证效率和覆盖率有显著提升。

🎯 应用场景

该研究成果可应用于高性能处理器、GPU、AI加速器等芯片的设计验证，确保浮点运算的正确性和可靠性。在金融计算、科学计算、图像处理等对精度要求高的领域具有重要价值。未来可进一步扩展到更复杂的硬件系统验证，提升芯片设计的质量和效率。

📄 摘要（原文）

Formal verification of floating-point arithmetic remains challenging due to non-linear arithmetic behavior and the tight coupling between control and datapath logic. Existing approaches often rely on high-level C models for equivalence checking against Register Transfer Level (RTL) designs, but this introduces abstraction gaps, translation overhead, and limits scalability at the RTL level. To address these challenges, this paper presents a scalable methodology for verifying floating-point arithmetic using direct RTL-to-RTL model checking against a golden reference model. The approach adopts a divide-and conquer strategy that decomposes verification into modular stages, each captured by helper assertions and lemmas that collectively prove a main correctness theorem. Counterexample (CEX)-guided refinement is used to iteratively localize and resolve implementation defects, while targeted fault injection validates the robustness of the verification process against precision-critical datapath errors. To assess scalability and practicality, the methodology is extended with agentic AI-based formal property generation, integrating large language model (LLM)-driven automation with Human-in-the-Loop (HITL) refinement. Coverage analysis evaluates the effectiveness of the approach by comparing handwritten and AI-generated properties in both RTL-to-RTL model checking and standalone RTL verification settings. Results show that direct RTL-to-RTL model checking achieves higher coverage efficiency and requires fewer assertions than standalone verification, especially when combined with AI-generated properties refined through HITL guidance.