Lean-Verified FP32 and BF16 Arithmetic for ARCH, an HDL Designed to Be Written by Language Models
ARCH is a hardware description language explicitly intended to be generated by language models, and this paper (arXiv 2607.23715) delivers first-class IEEE-754 binary32 and bfloat16 arithmetic for it with end-to-end proofs. All 24 operators are described once against a single bit-vector IR and rendered three ways from one source — synthesizable SystemVerilog, an SMT-LIB model, and a Lean 4 proof model — with a Yosys-to-SMT miter machine-checking that emitted SystemVerilog matches the SMT model. Multiplier-free operators are proved exhaustively equivalent over all 2^64 inputs; SAT-hard FP32 mul and FMA are proved correctly rounded in Lean, sorry-free. The FMA's exact-wide 470-bit datapath would not pipeline, so it was reimplemented as a bounded 98-bit guard/round/sticky path that hits 268 MHz on Nangate45 and was proved bit-identical to the reference over all 2^96 inputs.
↳ Follow the thread