Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL

Shuqing Zhao

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 gen…