systemverilog

This paper presents the design and end-to-end formal verification of IEEE-754 binary32 and bfloat16 arithmetic for ARCH HDL, a hardware description language intended for AI model generation. The operators are proven correctly rounded using a hybrid approach combining exhaustive SMT equivalence checking and Lean 4 proofs, with synthesizable SystemVerilog output.