Toroid：用 LLM 生成性质并自动证明芯片 RTL 正确性的形式化验证工具

灵魂体仓库发布开源工具 Toroid，读取规格与 RTL 模块后由 LLM（实测 claude-opus-4-8）综合形式化性质，再用开源模型检查器 Yosys + SymbiYosys 求解，自动完成硬件验证工程师的验证闭环。演示中它对正确 FIFO 证明了 full ⟺ count==DEPTH 不变式，并捕获注入的 full 标志 off-by-one 缺陷、给出反例波形，还支持 RTL-to-RTL 等价性检查（PROVEN/FALSIFIED）。所有结论均来自真实求解器运行，一次实测生成 9 条性质（5 条 assert + 4 条 cover）一次编译通过；仅支持 ≲500 行的单时钟小模块，只做 safety 性质，且不修改 RTL。