Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL

Research Approach

This paper addresses the challenge of creating trustworthy, high-performance floating-point arithmetic for hardware generated by language models. The author introduces a methodology where every operator—including comparisons, conversions, and fused multiply-add (FMA)—is defined once in a shared bit-vector intermediate representation (IR). This IR is then rendered into three distinct artifacts: synthesizable SystemVerilog for hardware, SMT-LIB for formal verification, and Lean 4 for structured proofs. By sharing the same IR and linearization, the author ensures structural identity across all three back-ends, leaving only the per-node syntax table as a potential source of divergence, which is further mitigated by machine-checked miters.

Verification Strategy

The verification process is split based on solver tractability. Multiplier-free operators are verified exhaustively using SMT solvers against the IEEE-754 FloatingPoint theory. For multiplier-bearing operators (FP32 multiply and FMA), which are notoriously difficult for SAT-based bit-blasting, the author uses a structured proof approach in Lean 4. By lifting bit patterns to algebraic values, the proof avoids the complexity of the 24x24 multiplier array, allowing for a 'sorry-free' proof of correct rounding.

Timing-Driven Design

Physical characterization revealed that the standard 'exact-wide' FMA datapath is a timing bottleneck that resists pipelining. To address this, the author implemented a 'sticky-fold' FMA that uses a bounded 98-bit datapath. This design pipelines effectively to 268 MHz on a Nangate45 process. The author provides a formal proof that this bounded datapath is bit-identical to the exact-wide reference over all 2^96 possible inputs. Because the shared multiplier cancels out in the equivalence miter, this proof is computationally tractable, allowing the faster design to inherit the formal correctness guarantees of the reference model.

This work demonstrates a scalable path toward building verified hardware libraries. By separating the specification (the exact-wide reference) from the implementation (the pipelined sticky-fold) and using formal methods to bridge them, the author provides a template for optimizing hardware without sacrificing mathematical correctness. This is particularly relevant for AI-generated hardware, where the ability to automatically verify complex arithmetic units is essential for reliability.