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

This paper presents a scalable, modular methodology for the formal verification of floating-point arithmetic that employs direct RTL-to-RTL model checking, counterexample-guided refinement, and AI-assisted property generation to overcome the limitations of high-level abstraction and achieve higher coverage efficiency.

The Gist

Imagine you are building a super-precise calculator chip for a spaceship. This chip needs to handle floating-point numbers (like 3.14159 or 0.000001) with absolute perfection. If it makes even a tiny mistake, the spaceship could miss its target or crash.

This paper is about a new, smarter way to check if that calculator chip is built correctly, without having to test every single possible number (which would take forever).

Here is the breakdown using simple analogies:

1. The Old Way vs. The New Way

The Old Way (The "Translator" Problem):
Previously, engineers tried to verify these chips by translating the complex hardware code (RTL) into a high-level programming language (like C) and comparing the two.

• The Analogy: Imagine you have a recipe written in a secret code (the hardware). To check if it's right, you hire a translator to turn it into English (C code), then you compare the English version to a master cookbook.
• The Problem: Translations are never perfect. The translator might miss a nuance, or the English version might be too simple. You end up checking the translation, not the actual recipe. Also, if the recipe is huge, the translation process is slow and messy.

The New Way (The "Twin" Method):
This paper proposes comparing the hardware code directly against a "Golden Reference" model (a perfect, theoretical version of the chip), both written in the same language.

• The Analogy: Instead of translating the recipe, you build a perfect, theoretical "Ghost Kitchen" that knows exactly how the dish should taste. You then put your actual kitchen (the chip) and the Ghost Kitchen side-by-side. If they don't produce the exact same dish at the exact same time, you know something is wrong immediately. No translation needed.

2. The "Divide and Conquer" Strategy

Checking a whole spaceship engine at once is too hard for a computer. It gets confused.

• The Analogy: Imagine trying to prove a whole house is built correctly. Instead of looking at the entire house at once, you break it down room by room.
  1. Room 1 (Mantissa Alignment): Did the workers line up the bricks correctly?
  2. Room 2 (Add-Round): Did they glue them together and smooth the edges correctly?
• How it works: The paper uses a "Divide and Conquer" approach. They check the first room. If it passes, they move to the second. If a room fails, the computer gives them a "Counterexample" (a specific clue like, "Hey, you used the wrong brick size here"). The engineers fix that specific spot and move on. This makes the job much faster and less confusing.

3. The "AI Co-Pilot" (Agentic AI)

Writing the rules (called "assertions") to check these rooms is hard work. Humans have to write thousands of lines of code to say, "If the input is X, the output must be Y."

• The Analogy: Imagine you are a manager trying to write a rulebook for your employees. It takes you days.
• The AI Solution: The authors used an "Agentic AI" system. Think of this as a team of AI interns:
  • The Planner: Decides what rules need to be written.
  • The Writer: Uses a Large Language Model (like a super-smart chatbot) to draft the rules.
  • The Critic: Checks the rules for errors.
  • The Human-in-the-Loop: A human expert steps in when the AI gets confused.
• The Result: The AI can write the initial rulebook much faster than a human. However, the AI sometimes gets a bit "chatty" or redundant (writing the same rule three times). The human expert acts as a editor, trimming the fat and making the rules sharp.

4. The "Stress Test" (Fault Injection)

How do you know your checking system is actually good?

• The Analogy: Imagine you have a security guard checking a building. To test if the guard is awake, you secretly leave a fake bomb in the lobby. If the guard finds it, they are doing their job. If they miss it, you need a new guard.
• The Experiment: The researchers intentionally broke their chip design (e.g., they made the chip ignore a specific number or flip a switch the wrong way). They then ran their new verification system.
• The Outcome: The system caught every single one of the fake mistakes. This proved that their method is robust and won't miss hidden bugs.

5. The Big Takeaway

The paper concludes that:

1. Direct Comparison is King: Comparing hardware directly to a perfect hardware model is better than translating it to software.
2. AI is a Great Assistant, but needs a Boss: AI can generate the checking rules very quickly, but it needs human guidance (HITL) to be precise and efficient. Without a human, the AI writes too many rules and misses the big picture.
3. It Works: This method found bugs faster, used fewer rules, and covered more ground than previous methods.

In a nutshell: They built a better way to check math chips by comparing them directly to a perfect twin, breaking the job into small rooms, and using a team of AI interns led by a human manager to write the inspection checklist. It's faster, smarter, and catches more mistakes.

Technical Summary

Here is a detailed technical summary of the paper "Formal Verification of Floating Point Arithmetic: High: Formal that 'Floats' High", presented at the 37th IEEE International Conference on Microelectronics (ICM) 2025.

1. Problem Statement

The formal verification of Floating-Point Units (FPUs) is a critical yet challenging task in hardware design due to:

• Non-linear Arithmetic: Floating-point operations involve complex interactions between control logic (e.g., exception handling, normalization) and arithmetic datapaths.
• Strict Compliance: Designs must adhere to IEEE-754 standards, handling edge cases like denormalized numbers, overflow, underflow, and precision loss.
• Limitations of Existing Approaches: Current methodologies often rely on high-level C models for equivalence checking against Register Transfer Level (RTL) designs. This introduces:
  • Abstraction Gaps: Semantic mismatches between C software and hardware execution.
  • Scalability Issues: Difficulty in verifying datapath-intensive RTL designs directly.
  • Translation Overhead: Significant manual effort required to maintain C reference models and translation flows.

2. Proposed Methodology

The authors propose a direct RTL-to-RTL model checking methodology that eliminates reliance on high-level C abstractions. The core strategy involves:

• Direct Comparison: The RTL implementation is verified directly against a cycle-accurate, bit-accurate golden reference model (also in SystemVerilog), ensuring architectural alignment.
• Hierarchical Decomposition (Divide-and-Conquer):
  • The design is partitioned into modular stages to reduce the "cone of influence" (COI) and proof complexity.
  • Case Study: A floating-point adder is decomposed into two stages:
    1. Mantissa Alignment Stage: Handles exponent difference calculation and mantissa shifting.
    2. Add-Round Stage: Performs addition, normalization, and rounding.
  • Theorem-Lemma Structure: A main correctness theorem (Result Equivalence) is proven by verifying intermediate lemmas for each stage.
• CEX-Guided Refinement: When the formal tool generates a Counterexample (CEX), the implementation or property set is iteratively refined to resolve the discrepancy until equivalence is proven.
• Agentic AI Integration: A multi-agent system (MAS) utilizing Large Language Models (LLMs) is employed to generate SystemVerilog Assertions (SVAs) from natural language specifications.
  • Workflow: A "Lead Agent" creates a verification plan; a "Property Generation Agent" drafts SVAs; a "Critic Agent" reviews logic; and an "Error Correction Agent" fixes syntax/semantics.
  • Human-in-the-Loop (HITL): Experts intervene to clarify design intent and resolve ambiguities when automated cycles fail to converge.

3. Key Contributions

1. RTL-to-RTL Model Checking: A scalable methodology that verifies floating-point arithmetic directly at the RTL level without C/C++ reference models, avoiding abstraction gaps.
2. Structured Proof Strategy: Implementation of a hierarchical decomposition approach using lemmas and helper assertions to manage complexity and improve proof convergence.
3. AI-Driven Property Generation: Integration of agentic AI (using models like GPT-5 and Llama3.3-70b) to automate the creation of formal properties, significantly reducing manual effort.
4. Robustness Validation: Systematic fault injection into the RTL design to test the sensitivity of the verification properties against precision-critical errors (e.g., sticky-bit distortion, rounding rule violations).
5. Comparative Coverage Analysis: A rigorous evaluation comparing handwritten properties vs. AI-generated properties in both RTL-to-RTL (with reference) and Standalone RTL (without reference) verification modes.

4. Experimental Results

The methodology was evaluated on a single-precision floating-point adder using the Cadence Jasper Formal Verification Platform.

• Bug Detection: The approach successfully identified and resolved two distinct implementation faults in the mantissa alignment logic (incorrect operand selection and faulty inversion logic) and two in the add-round stage (unconstrained exponent behavior and operand interchange).
• Fault Injection: All injected faults (e.g., carry-in manipulation, normalization shift errors) were successfully detected by the formal properties, confirming the robustness of the verification suite.
• Coverage & Efficiency (RTL-to-RTL with Reference):
  • Handwritten Properties: Achieved 98.42% formal coverage with only 2 assertions and a proof time of 0.073s.
  • AI-Generated Properties (Initial): Required 7–15 assertions and longer proof times (up to 12s) due to redundancy and lack of constraints.
  • AI-Generated Properties (with HITL): After refinement, AI agents produced concise sets (3–6 assertions) achieving 98.42% coverage with proof times comparable to handwritten versions (e.g., GPT-5 achieved this with 3 assertions in 1.318s).
• Standalone Verification (Without Reference):
  • Coverage dropped significantly (e.g., ~62% for Llama3.3-70b without HITL) due to insufficient constraints on valid design behavior.
  • HITL refinement was crucial to add micro-architectural checks (e.g., sticky-bit propagation), raising coverage to ~92% (GPT-5) but requiring significantly more assertions (21) and effort.

5. Significance and Conclusion

• Efficiency: The paper demonstrates that RTL-to-RTL model checking combined with AI-generated properties is more efficient than standalone verification, particularly when a golden reference model is available. It reduces the number of assertions required and accelerates proof convergence.
• Role of AI: While LLMs can generate formal properties, they currently lack the deep micro-architectural understanding required for standalone verification without human guidance. HITL refinement is essential to eliminate redundancy, resolve counterexamples, and enforce architectural constraints.
• Future Impact: This work establishes a foundation for scalable, AI-assisted formal verification of complex arithmetic datapaths. It suggests that future advancements in extracting "micro-architectural intent" from LLMs could further minimize human refinement efforts, making formal verification more accessible for complex FPUs (multipliers, dividers) and safety-critical systems.