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.

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