Aristotle 形式化验证 1220 万门芯片模块，证明 185 条属性并降功耗 26%

satnam6502 · x · 2026-10-29

Harmonic 的形式化推理系统 Aristotle 在芯片公司 Tensordyne 的实战案例：面对一个 1220 万等效门规模的硬核验证模块，Aristotle 证明了 185 条属性、驳倒 56 条，发现深达 110,000 周期的 bug；随后从规格直接生成 RTL，并将功耗降低约 26%，每一步都重新形式化证明。

Tensordyne 验证工程师 Jonathan Ko 称这在传统工具下「不可想象」。这是「proof-driven synthesis」（证明驱动综合）在可信硬件设计上的标志性展示。