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

By Ashish Darbari, Nicky Khodadad, and Nguyen Vu

The semiconductor industry continues to debate DPV versus FPV, but the real challenge is achieving scalable, trustworthy verification for AI-era silicon. Modern RISC-V, Arm, x86, GPU and AI accelerators rely on increasingly complex floating-point and transprecision datapaths where correctness is mission critical. The methodology argument has become a distraction from a much harder question: how do teams find the bugs that neither constrained-random simulation nor model-heavy equivalence flows are structurally capable of finding?

Why datapath verification matters

From the Intel FDIV incident to today’s AI accelerators, arithmetic correctness has become a first-order design requirement. Modern designs support IEEE-754, BF16, FP16, FP8 and custom AI formats, creating enormous verification complexity. The failure surface has also shifted. Bugs that used to sit in the data path — e.g., wrong quotients and wrong products — are now increasingly in the status path: correct-looking values delivered with the wrong flags, or with no flags at all. Although conventional test-based techniques and C/C++ equivalence methods can also catch flag issues, catching them in pipeline- and control-heavy, timing-optimized designs is exactly the class of defect that leaks silently past a value-only checker and shows up as a training instability, a lost gradient, or a silent data corruption event in production.

The promise and limitations of C-to-RTL equivalence checking

C-to-RTL equivalence checking has delivered tremendous value and found many RTL bugs. However, real silicon is deeply pipelined. Teams often create chains of model minimizations and abstraction models to achieve convergence, consuming engineering time and creating dependencies on EDA tool flows and application engineers. The verification effort ends up split between building the proof infrastructure and actually chasing bugs, and the balance tilts further toward infrastructure with every new precision, every new rounding mode and every new fused variant added to the ISA.

Who checks the checkers?

Recent research has highlighted potential soundness concerns in equivalence-checking flows, including false positives, missed corner cases and tool-specific weaknesses. The issue is not that equivalence checking is wrong, but that no single methodology should be a single point of failure. The industry needs independent, mathematically grounded checks that can be pointed directly at RTL without a chain of hand-crafted abstractions in between.

The floatrix approach

floatrix replaces model-centric verification with mathematically grounded verification IP. The property framework has been aligned against Berkeley HardFloat semantics, providing a trusted open-source IEEE-754 reference basis. floatrix supports IEEE-754 formats, AI formats, custom number formats and transprecision architectures. Environments are stood up in hours rather than weeks, run directly against microarchitectural RTL, and target both the value and the flag lattice as first-class outputs of every operation.

Why floatrix matters

The baseline reasoning behind using the equivalence checking approach for floating-point verification of hardware is that one can use a golden C/C++ model to validate the RTL against it. Out of the box, the tools rarely converge against a microarchitectural implementation, so a combinational RTL model is used for comparison with C/C++ models, which does provide better proof convergence.

Model minimization and the burden of proof for real silicon

A side-step of performing another EC step between the micro-architectural and the combinational model has to be performed, which poses significant challenges for proof convergence but can be overcome by FV experts with experience in helper assertions and micro-architectural knowledge. This is easier said than done. The reality of required human effort is significant and often leaves teams lagging behind schedule unless they resort to dynamic simulation, which becomes the de facto choice but comes with the risk of not covering all the corner cases and edge cases.

Validation problem

Now consider the problem where a C/C++ model has been tweaked to improve trade-offs between precision and PPA, and an HLS tool then generates the RTL. The golden model itself has been modified.

In this case, these questions become interesting for validation and verification.

• How does one ensure the correctness of the RTL now?
• How does one create a golden C/C++ model?
• How much time/effort would it take to redo the chain of sequential equivalence checking to establish that the actual microarchitectural RTL implementation is correct?

To address these gaps, holistically, what you need is an end-to-end golden model of floating-point operations in a format that is easy to extend for micro-architectural design changes and naturally allows proof decomposition, case-splitting, scenario reductions and a plethora of formal proof convergence techniques allowing direct verification of RTL changes — quickly and exhaustively. This requires a level of deep expertise that very few organizations have.

Coverage driven validation and verification with floatrix

Property checking naturally supports a decomposition-based flow: it compartmentalizes scenarios as assertions and covers, and provides cone-of-influence reduction by construction. This is where an SVA-based model becomes useful.  Our results have shown a marked increase in ease-of-use and turnaround time in verifying actual micro-architectural RTL implementations, resulting in exhaustive proof convergence finding failures (RTL bugs) and proofs of bug absence with six-dimensional coverage as useful and necessary sign-off criteria. The other benefit of using our SVA-based solution is that it can be run with any formal property checking tool, providing a side-by-side comparison of soundness and completeness of solvers which avoids any last-minute surprises.

Compliance for IEEE 754

Compliance and validation problems remain important, and for IEEE 754 compliance, our SVA model has been exhaustively proven to be correct against the Berkeley Hardfloat model using formal verification property checking tools. The Berkeley Hardfloat model has been proven correct in comparison to the Softfloat one, using either off-the-shelf C-to-RTL formal tools or simulation. We have not carried out the compliance of Hardfloat with Softfloat, so it naturally avoids common-mode errors.

By proving equivalence once, against the Berkeley models, we can ensure that IEEE 754 compliance is always adhered to by the RTL when our SVA property set, part of floatrix, has been proven exhaustively against the RTL. In addition to validating our model against the Berkeley Hardfloat one, we have also tested floatrix to verify other IEEE 754 compliant RTL implementations where we have found bugs. We capture some of these in the next section.

Public bug discoveries

The following four public bug reports were all found by floatrix, across four independent RISC-V vector and AI-accelerator FPUs. Constrained-random simulation, unit testing, and model-based equivalence flows are systematically missing defects at the edge cases. To the best of our knowledge, every one of these designs has passed extensive verification before floatrix was pointed at it.

1. Ocelot — vfwadd.vv does not raise Invalid (NV) on a signaling NaN input

What should happen

vfwadd.vv is a widening add: fp16 operands, fp32 result. IEEE 754-2019 §7.2 requires any operation given a signaling NaN operand to signal the invalid-operation exception, and RVV accrues vector FP exceptions into fflags exactly as the scalar unit does. Architecturally, the instruction is atomic — the fact that the implementation widens first and adds second is a microarchitectural choice that must not be observable in the flags. The result should be a quiet NaN with NV set.

What actually happens

The module converts the operand from fp16 to fp32 before performing the transprecision add. On a signaling NaN input, the conversion stage does not transfer the quiet bit — bit 9 in fp16 to bit 22 in fp32 — and raises the Invalid flag only locally inside that module. That local flag does not propagate to the ADD module, and because the conversion has already turned the operand into a qNaN, the adder sees nothing exceptional and produces no Invalid flag. The sNaN is silently laundered into a qNaN somewhere between the two units.

Waveform

tt_vfp_unit receives the sNaN operand (shown as 16’h7d00 in the report) as the first element in cycle 5. In cycle 7 the result is a NaN, but no invalid flag is asserted. The counterexample is attached to the issue as TT_add_fp16_fp32_sNaN_not_raised_Invalid_flag.zip. The two-cycle window is the whole story: the operand arrives signaling, the result emerges quiet, and the invalid flag never moves.

Why it matters

The data output is defensible. A NaN in, a NaN out, so any checker comparing only result values passes. The entire failure lives in the status output, which is the part software actually relies on to detect that something went wrong. Two distinct defects are stacked here: the quiet-bit transfer in the converter (signaling status is destroyed rather than the value being quieted with its payload preserved), and the flag-merge path between converter and adder. An sNaN exists specifically to be trapped or flagged; a unit that consumes one without a trace defeats its only purpose.

2. Saturn Vectors — vfwadd.vv does not raise Invalid on a signaling NaN input

What should happen

Identical requirement to Ocelot: a signaling NaN operand to a widening vector add must set NV in fflags and deliver a quiet NaN. The internal decomposition into convert-then-add is invisible to the architecture, so the flag lattice has to be disjunctioned across the composition.

What actually happens

The stimulus is the minimum-payload signaling NaN, 16’b0111_1100_0000_0001. Before doing the transprecision ADD the module first converts the operand from fp16 to fp32. The conversion does not transfer the quiet bit — bit 9 in fp16 to bit 22 in fp32 — and raises the Invalid flag only from within that module. That Invalid flag does not propagate to the ADD module, and since the input has become a qNaN through conversion, the ADD module produces no Invalid flag.

Waveform

The issue attaches the trace as saturn_xprec_fp16_fp32_add_NV_flag.zip, captured through the ExecutionUnitfp binding. The waveform shows the same signature as Ocelot: the sNaN encoding entering the pipe, the widened operand emerging already quieted, and the NV bit flat across the result cycle.

Why it matters

Two unrelated RISC-V vector implementations — a Tenstorrent BOOM fork and a Berkeley design — reproduce the same bug for the same architectural reason. Whenever a convert unit is composed with an arithmetic unit, two things must be engineered deliberately: the sNaN-ness of the operand has to survive the widening, and the exception flags of every sub-unit have to be OR-ed into the instruction’s architectural flags. Both designs got the data path right and the status path wrong, in the same place, independently.

3. CVFPU — BFloat16 DIV underflows to zero with no exception flags

What should happen

For operands 16’hae47 and 16’hf447, the unbounded exact result is 1 × 2⁻¹⁴⁰. Since that is out of range for bfloat16, it underflows to 16’h0000, and both inexact and underflow must be set. Under round-to-maximum-magnitude the expected result is 16’h0001, not zero. In general, when two regular numbers are divided, the exact result can never be zero.

Both operands carry the same 7-bit significand field, so the quotient significand is exactly 1.0 and the result is a clean power of two: 2⁻³⁵ ÷ 2¹⁰⁵ = 2⁻¹⁴⁰. BFloat16’s smallest subnormal is 2⁻¹³³, so the exact value is 128× below anything representable. A zero result delivered from a normal-by-normal division is by construction both tiny and inexact, making UF and NX unconditional rather than a judgment call.

What actually happens

Using THMULTI for bfloat16 DIV, the computed result is 16’h0000 with no exception flags raised. In round-to-nearest, the value is right, but the flags are absent.

Waveform

The issue carries a captured trace image of the DIV operation showing the operand pair driven in, the result bus settling to 16’h0000, and the status/fflags output remaining all-zero across the result-valid cycle — no UF, no NX. There is no partial flagging to debug around: the exception path simply never fires for this operand class.

Why it matters

This failure showcases an underflow flag not triggering for a clearly underflow case. In an ML pipeline, it is precisely the case that turns a small-but-real gradient into a hard zero with nothing in the flags to record that any information was lost.

4. RedMulE — underflow flag missing at the subnormal/normal boundary in the FMA

What should happen

Per IEEE 754, after-rounding underflow must be raised when a non-zero result computed as though the exponent range were unbounded would lie strictly between ±b^emin. The subtlety is that tininess detection requires its own rounding, distinct from the rounding that produces the delivered result: the tininess rounding is performed as if the exponent were unbounded, so its rounder input is always a normal number, whereas the final-result rounder is fed a subnormal when the value is too small to be normal in the target format. Two roundings, two different answers, and UF must be derived from the first.

What actually happens

With operand_a = 16’h03ee, operand_b = 16’h3c12 and operand_c = 16’h8000, the computed result lies at the subnormal/normal boundary and should be inexact with the underflow flag set — the flag is not set.

Working the numbers: a is an fp16 subnormal of 0.982421875 × 2⁻¹⁴, b is 1.017578125, and c is −0 and contributes nothing. The exact product is ≈ 0.99969 × 2⁻¹⁴, strictly inside the subnormal band. Rounded to the fp16 grid, it lands on exactly 2⁻¹⁴ (0x0400) — the smallest normal. The implementation evidently derives tininess from the delivered result, sees a normal number, and suppresses UF.

Waveform

The attached trace shows the three operands driven into a single compute element’s FMA, the result bus resolving to 0x0400, and the status output carrying NX but not UF on the result cycle. The diagnostic tell is the rounding-mode dependence: RTZ can never round up out of the subnormal range, so the bug is invisible there and appears in every other mode — the same signature recorded in cvfpu #94, where the class of failures affects the FMA multiply-based operations and the T-Head DIV, in all rounding modes except RTZ, in the corner case where the final result is ±b^emin but the unbounded-exponent value lies strictly inside the boundary.

Why it matters

RedMulE is a GEMM array of many compute elements, each with an FMA adapted from the open-source transprecision floating-point unit, running FP16 accumulation chains for on-chip training on ultra-low-power SoCs. Values drifting into the subnormal band is the normal operating regime for that workload, not an exotic corner, and the bug is replicated in every CE in the array. Losing the underflow signal removes the one architectural indicator a training runtime has that its precision is collapsing.

The common thread

All four issues explained above appear to be status-path ones rather than data-path, with the bfloat16 bug being the partial exception, since it also delivers a wrong value under directed rounding. Each produces a numerically plausible result while dropping or mis-deriving a flag. While trapping the flag bugs may not be that challenging with C/C++ equivalence checking strategies, the reality is that most of these manifest with the increase in micro-architectural optimizations and are therefore very hard to catch with equivalence checking and with test-based techniques.

Two of the four sit at a composition boundary: convert-to-add and tininess-detect-to-round. IEEE 754 semantics are defined over the whole operation, but the RTL is assembled from units that each only see their own slice.

5. CVFPU — Sqrt/Div operation processed without a valid input handshake

What should happen

This is a ready/valid handshake contract, not an arithmetic one. Under the standard AXI-stream-style protocol that fpnew_top implements, a transfer occurs on a cycle if and only if in_valid_i and in_ready_o are both asserted on that cycle. A request presented while in_ready_o is low has not been accepted, so no internal state may advance on it, and no result may ever be produced for it. Correspondingly, every output handshake must be traceable back to exactly one prior input handshake — one accepted request, one delivered result.

The readiness reported at the top must also be the honest conjunction of what every lane can accept. With a merged DIVSQRT block and EnableVectors = 1, the unit is shared across lanes: a single physical divider/square-rooter serves all of them. Whatever readiness lane 0 computes locally is only meaningful once the top has confirmed that the whole block, all lanes included, can take the request.

What actually happens

The failure is a lane-state divergence between a vector operation and a following scalar one. In the first cycle, a 16-bit Sqrt vector operation arrives, expected to take 7 cycles. Because the Sqrt/Div block is MERGED, all lanes run the same operation on the same operands. At cycle 7 the calculation completes, but the output of fpnew_top is backpressured — out_ready_i is low — so all the Sqrt/Div units are put into HOLD, waiting to be granted.

In the next cycle out_ready_i is asserted and another valid scalar Sqrt operation arrives, with in_valid_i high but not necessarily in_ready_o. Because this second operation is scalar and the output is now valid, only the first Sqrt lane switches from HOLD to BUSY, while the other lanes move from HOLD to IDLE. In that cycle, the lane-level in_ready goes high, so the first unit takes the operation and expects to produce a result.

The break is that this local readiness never becomes architectural readiness. The in_ready signal is not propagated to the top, creating the input-handshake problem: in_ready_o from lane 0 actually depends on the readiness of the other lanes as well, because the previous instruction was a vector. Since the in_valid_i of the second operation goes only to the first lane, the other lanes must move from HOLD to IDLE and their ready_in is low. The result is that the first lane accepts and acknowledges the scalar operation while the top module does not accept it, and a few cycles later a spurious result is produced.

So, the design ends up with two mutually contradictory views of the same cycle: lane 0 believes a transaction was accepted and starts computing, the top believes nothing was accepted and never records the request. The arithmetic proceeds regardless, and a result eventually falls out of a pipeline that, architecturally, was never given anything to do.

Waveform

The trace shows that although there is no valid input handshake at cycle 8, nor at any cycle from 2 through 13, there is still an output handshake at cycle 14. That single observation is the entire proof: an output transfer with no corresponding input transfer anywhere in the preceding window. The issue carries three further captures showing the lane state machines diverging: all lanes entering HOLD together at cycle 7 under backpressure, then splitting on the next cycle as lane 0 goes HOLD→BUSY on the scalar request while the sibling lane goes HOLD→IDLE and drops its ready.

The counterexample is short and self-contained: PipeRegs = 0 removes the pipeline registers that would otherwise mask the mismatch, and the backpressure at cycle 7 is what forces every lane into HOLD simultaneously and sets up the divergence.

Why it matters

This one is categorically different from the four previous issues.

Those corrupt a status bit while the data stays plausible; this corrupts the transaction stream itself. A spurious out_valid_o with no originating request means the consumer — a scalar core’s writeback stage, or a vector unit’s completion logic — receives a result it never asked for. Depending on how the surrounding logic tracks in-flight operations, that lands as a stray register write, a misattributed destination tag, a fflags update belonging to no instruction, or a permanently skewed request/response count that eventually deadlocks or desynchronizes the whole FPU.

The trigger conditions are also the reason simulation is unlikely to find it. It needs three things to coincide: a vector operation immediately followed by a scalar one on the merged DIVSQRT block, output backpressure landing precisely on the completion cycle, and PipeRegs = 0. Random stimulus rarely aligns a protocol stall with an operation-type change on the very next cycle, and directed tests for divide and square root normally focus on operand corners rather than handshake corners. Formal, by contrast, explores backpressure as a free variable and finds the alignment immediately.

The deeper point is the same composition lesson as the earlier bugs, transplanted from arithmetic to control: readiness is a property of the shared merged block, but it is being computed by an individual lane that has no visibility of the sibling lane’s state transition. Any fix has to make the top-level in_ready_o a genuine conjunction across all lanes — and, critically, make lane 0’s decision to leave HOLD conditional on that top-level handshake rather than on its own local view, so that no lane can start work on a request the top has not accepted.

6. CVFPU — Underflow flag spuriously set when the ADDMUL unit is configured to MERGED

What should happen

IEEE 754 signals underflow only when the result is both tiny and inexact. Tininess here is detected after rounding: the value is tiny if, computed as though the exponent range were unbounded and rounded, it lies strictly inside ±b^emin. Crucially, an exact subnormal result must not raise UF — the tiny-and-inexact conjunction is what separates a genuine loss of precision from a small-but-perfectly-representable answer.

The second requirement is a configuration-independence one, and it is really the heart of this bug. fpnew‘s ADDMUL block can be instantiated PARALLEL (one arithmetic slice per supported format) or MERGED (a single wide multi-format slice, sized to the widest format, that handles all of them). That choice is an area/timing trade-off. It must be architecturally invisible: the same operands under the same rounding mode must yield the same result and the same fflags in either configuration. A flag that depends on how the RTL was parameterized is a bug by construction, whichever of the two answers happens to be right.

What actually happens

In some edge cases where the underflow flag should be low because of after-rounding underflow detection, the flag still goes high when the ADDMUL unit is set to MERGED. The same cases behave correctly when the unit is set to PARALLEL. UF is being asserted on results that are tiny but exact, and the rounding step that would have made them inexact never actually removes any bits.

The reporter’s root-cause hypothesis points straight at the sticky-bit computation in the merged datapath: this may be due to sum_sticky_bits being zero inside the fmt_uf_after_round logic, because PRECISION_BITS is 53 and hence everything fits inside final_mantissa, leaving nothing to round. This only affects the underflow-after-rounding logic.

That mechanism is worth unpacking, because it explains exactly why MERGED and PARALLEL diverge. In MERGED mode, the shared slice is sized for the widest format: PRECISION_BITS = 53, i.e., double precision. When a narrower operation (fp16, bf16) runs through that oversized datapath, the entire exact product or sum fits inside final_mantissa with room to spare, so nothing spills into the sticky region and sum_sticky_bits is identically zero. The after-rounding tininess logic evidently reads that condition and concludes the wrong thing by treating “no sticky bits” as a case to flag rather than as proof that the result is exact and therefore must not be flagged. In PARALLEL mode, the slice is sized to the actual format, real bits fall off the end, the sticky computation behaves as the logic expects, and the bug never surfaces.

The behavior also exists with mixed-precision source and destination formats, including bf16 to fp32. That widens the blast radius considerably as it is not confined to one narrow format but affects the whole class of operations where the operand width is smaller than the merged slice’s internal precision.

Waveform

The issue carries screenshots of the two setups producing different results on the underflow flag. The same stimulus run twice, once MERGED and once PARALLEL, with the result buses identical and the UF bit differing. Here we isolate the defect to the flag-generation logic with no ambiguity about operands, rounding mode, or the delivered value, and it rules out any reading in which the arithmetic itself is at fault. Whatever the correct UF value is for those operands, the design cannot be producing it in both configurations.

Why it matters

This is the mirror image of the RedMulE and CVFPU underflow bugs described earlier: those miss an underflow that IEEE requires, this one invents one that IEEE forbids. Both directions are harmful, but false positives corrode trust in a different way. Software that traps on UF or polls fflags to detect precision collapse will fire on results that are perfectly exact: spurious traps, spurious rescaling in a mixed-precision training loop, or engineers learning to ignore the flag altogether because it cries wolf.

The configuration dependence is the more strategic concern. MERGED exists to save area, and it is the configuration a resource-constrained SoC is most likely to choose, so the bug preferentially hits the deployments least able to absorb it. It also means that verifying one configuration tells you nothing about the other: any sign-off that ran only PARALLEL would report a clean underflow story while the shipped MERGED instance misbehaves. Parameterized IP needs its flag semantics proven across the parameter space, not just at whichever setting the regression happened to build.

Structurally this belongs with the earlier composition bugs, but the seam is a different one: not between two units, but between a format and the datapath width it is executed on. The sticky-bit logic silently assumes the mantissa path is sized to the operation’s own precision. In MERGED mode, that assumption is false for every format except the widest one, and the exactness signal derived from it is meaningless.

In all the cases where we found the bugs, it took us a few minutes to an hour to integrate a new design (we do not have any prior knowledge of any designs we verified), and the proof outcomes came out within seconds to minutes.

Ten reasons to use floatrix

1. No model minimization
2. Direct microarchitectural verification
3. Vendor-neutral deployment
4. Reusable verification IP
5. IEEE-754, BF16, FP16, FP8 and custom format support
6. Transprecision verification
7. Easy to set up and does not require formal experts
8. Faster bug discovery on full RTL implementation
9. Cross-tool validation
10. Better schedule predictability

Conclusion

This is not really a DPV-versus-FPV debate. What actually scales across architectures, precisions and generations of silicon is a set of reusable mathematical verification assets. C-to-RTL equivalence checking will remain an important pillar for design bring-up and architectural evaluation when teams naturally have C models in place. However, once we go beyond proving the equivalence of initial RTL implementations, the burden of showing that complete, timing-optimized, heavily pipelined implementations are free from corner-case and edge-case bugs demands a property-checking solution that is vendor-neutral.

floatrix demonstrates that teams can spend less time building proof infrastructure and more time finding bugs. The more useful question is an empirical one: how many bugs are found, how quickly they are found, and how much effort it takes to find them. If your verification flow depends on abstraction chains and convergence exercises that take a very long time, it may be time to ask what your team could achieve with formal verification models that are ready to use out of the box and materially reduce the burden of proof engineering for real microarchitectural implementations.

Nicky Khodadad is a senior solutions engineer at Axiomise.

Nguyen Vu is a hardware verification engineer at Axiomise.

The post Verified. Until It Isn’t: Why Datapath Verification Needs A New Playbook appeared first on Semiconductor Engineering.