Harmonic 数学模型形式化证明 200 行 Verilog 浮点除法正确性

thomasahle · x · 2026-10-29

一位开发者分享了用 Harmonic 的数学定理证明模型验证硬件设计的体验：对一个仅 200 行的简单 Verilog 浮点除法（fpdiv）文件，模型成功证明了「商寄存器 bit 23 置位」和「正常输入下除法结果按向零舍入逐位正确」等属性，界面左侧实时显示已证明/被反驳的属性清单。

他也吐槽痛点：验证过程长时间卡住时没有任何进度指示或思维链可见，希望未来能显示推理进展。这一案例展示了 AI 形式化验证在硬件正确性上的实际落地。