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

arXiv: https://arxiv.org/abs/2512.06850 · HTML: https://mlsanity.com/paper/2512.06850/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 23 references that are in the map.
- First posted on arXiv 7 Dec 2025.

## Builds on (most cited first, 2 of 2)

- [Hey AI, Generate Me a Hardware Code! Agentic AI-based Hardware Design & Verification](https://mlsanity.com/paper/2507.02660/) (2025)
- [CREST: Hardware Formal Verification with ANSI-C Reference Specifications](https://mlsanity.com/paper/1908.01324/) (2019)

## Built on by (most cited first, 1 of 1)

- [Benchmarking Large Language Models on Floating-Point Error Classification](https://mlsanity.com/paper/2606.31308/) (2026)

## Abstract (arXiv)

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.