Aristotle 形式化验证 fpdiv 电路，仿真再揪出 5 类浮点 bug
thomasahle · x · 2026-10-29
thomasahle 与 Harmonic 交流的截图显示，其形式化验证系统 Aristotle 成功证明了 fpdiv（IEEE-754 FP32 浮点除法）电路的两项约定性质：确认端口为 32 位单精度（用户原说 FP64 系笔误），操作数为规格化有限数，商经向零截断为 24 位有效位；同时验证了 RTL 中组合 always 块的赋值性质。
有趣的是，在完成形式化证明后，Aristotle 又主动对约定范围之外的用例跑了仿真，发现多个疑似真实 bug：
- 负无穷被误判为 NaN（-∞/1.0 得 NaN 而非 -∞）；
- 除以负零未命中特殊分支，1.0/(-0.0) 返回有限值而非 -∞；
- 零结果恒为 +0，-1.0/+∞ 未得 -0；
- 指数上溢/下溢回绕，次正规数未处理；
- 结果为截断而非 IEEE 默认的就近舍入（1.0/3.0 尾数差 1）。
作者还提出一个值得思考的问题：既然仿真快得多，为何不先仿真后证明？系统展示的左侧面板可实时呈现已证明的性质。
所属事件:实测 Harmonic Aristotle 验证 Verilog：证明能过但产物遭质疑(6 条相关)→
「编程与Agent」频道最新
- qwen-code 合并 PR：Qwen4 全系上下文窗口定为 100 万 tokens — haider1 · 2026-10-29
- AI 工程师忠告:把自建 evals 当一等公民才是项目成败关键 — paulabartabajo_ · 2026-10-29
- 跑满 55 个 subagent：博主让 Claude Code 开批量工作流执行海量任务 — AlchainHust · 2026-10-29
- DataTalks.Club 联手 Nebius 推免费课：生产级生成媒体 AI Agent — Al_Grigor · 2026-10-29
- 开源 MCP 服务器让 Claude/ChatGPT 引用芯片数据手册页码作答 — Winter-Drop-1334 · 2026-10-29
- 用 Claude 写出浏览器 PS2 模拟器:GTA、生化4 可直接开玩 — yousriii · 2026-10-29