机器学习辅助等价性检查：问题设定与个人评注

问题

大规模组合/时序等价性检查中，中间等价点与证明策略的选择强烈影响 runtime。纯启发式在深逻辑锥上容易超时。

方法（摘要）

• 从图结构与历史证明轨迹学习，对候选 cut-point 打分。
• 高分候选交给已有 equivalence checker；失败则更新特征。
• 强调 checker 结果是唯一合入标准，学习器不直接宣称等价。

注：本卡片为教学示例结构；录入真实论文时请替换 authors / venue / doi 并改写本节为该文原意。

贡献（作者自称 · 转述）

1. 可复现的 cut-point 排序基线。
2. 与工业 checker 的松耦合接口。
3. 在公开与内部基准上的超时率下降。

我的评注

• 与 AI4EDA 总体分工一致：提议 / 裁决分离值得保留。
• 需关注分布外设计（新标准单元库、新编码风格）时排序器是否崩坏。
• 后续可对照本站笔记「ABC rewriting」看「局部改写」与「等价证明」是否共用图特征。

行动项

• 找一开源 checker 复现最小 miter 实验。
• 把特征列表抄进 /notes 另开一页。

← 返回 Papers