hdl

本文介绍了为ARCH HDL（一种面向AI模型生成的硬件描述语言）设计并端到端形式化验证IEEE-754 binary32和bfloat16算术。这些算子通过结合穷举SMT等价性检查和Lean 4证明的混合方法，被证明具有正确的舍入，并输出可综合的SystemVerilog。

本文类比了C/C++中的安全漏洞与Verilog中的安全漏洞，指出硬件描述语言的设计导致了缺陷，并认为行业应投资于更安全的替代方案，类似于软件领域对内存安全编程语言的推动。