The semiconductor industry keeps debating DPV versus FPV, but that argument misses the real challenge: achieving scalable, trustworthy verification for AI-era silicon. Modern RISC-V, Arm, x86, GPU and AI accelerators depend on increasingly complex floating-point and transprecision datapaths where correctness is mission-critical — and the failure surface has shifted. Bugs used to live in the data path (wrong quotients, wrong products). Increasingly, they live in the status path: correct-looking values delivered with the wrong exception flags, or none at all. That’s the class of defect that slips silently past a value-only checker and surfaces later as training instability, a lost gradient, or silent data corruption in production.

Why equivalence checking isn’t enough. C-to-RTL equivalence checking has found real bugs, but real silicon is deeply pipelined. Teams build chains of model minimizations and abstractions just to get proof convergence — engineering effort that grows with every new precision, rounding mode, or ISA variant, and eats into the time actually spent chasing bugs. Recent research has also surfaced soundness gaps in equivalence-checking flows themselves: false positives, missed corner cases, tool-specific blind spots. No single methodology should be a single point of failure — the industry needs independent, mathematically grounded checks pointed directly at RTL.

The floatrix approach. floatrix replaces model-centric verification with mathematically grounded verification IP, aligned against the open-source Berkeley HardFloat reference for IEEE-754 compliance. It supports IEEE-754, BF16, FP16, FP8 and custom AI formats, stands up in hours rather than weeks, and treats both the value and the flag lattice as first-class outputs — not an afterthought.

Six real bugs, six passed designs. floatrix was pointed at six independently developed RISC-V and AI-accelerator FPUs — every one of which had already passed extensive verification. It found a bug in each:

• Ocelot & Saturn Vectors (two unrelated implementations) both silently “launder” a signaling NaN into a quiet one during widening add, losing the Invalid flag entirely.
• CVFPU’s BF16 divider underflows to zero with no exception flags — turning a small-but-real value into a silent hard zero, exactly the failure mode that corrupts ML training.
• RedMulE misses the underflow flag right at the subnormal/normal boundary — the normal operating regime for on-chip training, not an edge case.
• CVFPU’s Sqrt/Div unit produces a result with no valid input handshake behind it — a protocol bug, not an arithmetic one, that only appears under a precise, three-way timing collision simulation is unlikely to ever hit.
• CVFPU’s ADDMUL unit spuriously raises underflow — but only when configured MERGED instead of PARALLEL, meaning the same silicon logic gives different answers purely based on an area/timing configuration choice.

The common thread: these aren’t arithmetic mistakes. They’re composition bugs — living exactly at the seam between two units, where each half is locally correct but the end-to-end IEEE-754 guarantee falls through the crack in between.

The bottom line. This was never really a DPV-vs-FPV debate. What scales across architectures and silicon generations is reusable, mathematically grounded verification IP — not another abstraction chain. floatrix let the team spend less time building proof infrastructure and more time finding real bugs, with proof outcomes landing in seconds to minutes once a design was integrated.

Read the full article on Semiconductor Engineering

If you’d like to dive deeper into the bug families, real‑world examples and how nocProve scales to full mesh configurations, you can read the full blog post on SemiEngineering. 

👉 Verified. Until It Isn’t: Why Datapath Verification Needs a New Playbook