实测 Harmonic 数学 Agent:为形式化验证 Verilog 主动追问澄清问题

thomasahle · x · 2026-10-29

研究者 thomasahle 正在试用 Harmonic 的数学/形式化验证 Agent,称赞其"多轮澄清提问"设计。从截图看,Agent 在验证浮点除法模块 FPDivide.v 时,主动指出组合 always 块未在所有控制路径上赋值、会推断出 latch 导致形式验证受阻,并提出加两行默认赋值(用 ifndef 宏保护)以不改动原代码;另一条提问则要求用户明确"正确的商"到底指哪种行为(截断还是 IEEE-754 舍入)。Agent 还提供 Quick Answer 快捷选项,但会等待用户答复(倒计时约 8 分 45 秒)。作者吐槽:排队时间太长,10 分钟后自动选任务的设计让他喝完咖啡回来才轮到。