AI 中文总结
该研究针对ARCH硬件描述语言设计并验证了FP32和BF16算术，通过单个位向量IR生成三种模型，在求解器可处理性边界处验证，对FMA重新实现并证明其与参考位相同，所有验证声明与开源版本关联。
AI 中文摘要
我们报告了针对ARCH（一种旨在由语言模型生成的硬件描述语言）的一流IEEE-754二进制32位（FP32）和bfloat16（BF16）算术的设计与端到端验证。每个运算符（比较、转换、加、减、乘和融合乘加）针对单个位向量IR描述一次，并从一个源以三种方式呈现：可综合的SystemVerilog、SMT-LIB模型和Lean 4证明模型。这三个工件在结构上不会分离，并且逐节点打印机对应关系经过机器检查。验证在求解器可处理性边界处进行划分，无乘法器运算符被证明与SMT-LIB浮点理论完全等效，含乘法器运算符在Lean中针对精确二进值的舍入规范被证明正确舍入。物理特性表明FMA是时序异常值，重新实现后证明其与精确宽度参考位相同。所有机器检查的声明都与带标签的开源版本相关联。
英文摘要
We report the design and end-to-end verification of first-class IEEE-754 binary32 (FP32) and bfloat16 (BF16) arithmetic for ARCH, a hardware description language intended to be generated by language models. Every operator - comparisons, conversions, add, sub, mul, and fused multiply-add (FMA) - is 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. The three artifacts cannot drift apart structurally, and the residual per-node printer correspondence is machine-checked: a Yosys-to-SMT miter proves the emitted SystemVerilog equivalent to the SMT model for all 24 operators. Verification splits at the solver-tractability frontier: multiplier-free operators (comparisons, add/sub over all 2^64 inputs, conversions, and all binary BF16 arithmetic) are proved exhaustively equivalent to the SMT-LIB FloatingPoint theory; the SAT-hard multiplier-bearing operators (FP32 mul and FMA) are proved correctly rounded in Lean, sorry-free, against a value-level round-to-nearest-even specification over exact dyadic values. Physical characterization exposed the FMA as the timing outlier: its exact-wide 470-bit datapath does not pipeline in our flow. We reimplemented it as a bounded 98-bit guard/round/sticky datapath that pipelines to 268 MHz on Nangate45, and proved, in Lean and over all 2^96 inputs, that it is bit-identical to the exact-wide reference, so it inherits the reference's proven correct rounding. The equivalence is tractable precisely because the shared multiplier appears on both sides and cancels: neither a SAT solver nor the proof ever solves a multiplier equivalence. (The BF16 FMA is deliberately an FP32-accumulating fusion, characterized as exactly that.) All machine-checked claims are pinned to a tagged open-source release.
Comments8 pages, 2 figures
