核心能力
- 组合等价性检查 (CEC)：比较两个设计的组合逻辑等价性——常用于综合前后、优化前后验证。
- 时序等价性检查 (SEC)：考虑状态元素的时序等价性验证，适合 ECO 后或局部修改后的验证。
- 反例生成：当不等价时输出具体反例（输入向量 + 差异点），辅助调试定位。
- 外部适配层：当前通过适配器调用外部商业 formal 引擎，D1 shadow 阶段已完成接口定义。
- Agent 就绪：Python API 封装 CEC/SEC 提交，返回结构化等价性结果。
Agent 调用方式
cec = client.call("iFormal.check_equivalence",
design_ref="snap_a",
reference_ref="snap_b"
)
# cec.equivalent → bool
# cec.counter_example → dict | None (不等价时的反例)
# cec.proof_log → str (证明过程摘要)
输入 / 输出契约
| 方向 | 参数 | 类型 | 说明 |
|---|---|---|---|
| 输入 | design_ref | str | 待验证设计快照引用（如综合后网表） |
| 输入 | reference_ref | str | 参考设计快照引用（如原始 RTL 或黄金网表） |
| 输入 | mode | str (可选) | 验证模式：cec | sec，默认 cec |
| 输出 | equivalent | bool | 两设计是否逻辑等价 |
| 输出 | counter_example | dict (可选) | 不等价时的反例详情（输入向量、差异信号） |
| 输出 | proof_log | str | 证明过程日志，含检查点数量与耗时 |
在流程中的位置
01 综合
iMap
逻辑综合与工艺映射
02 验证
iFormal
综合后 CEC 等价性检查
03 物理设计
iFP · iPL · iCTS · iRT
布局布线全流程
04 ECO 验证
iFormal · iLVS
变更后等价性与 LVS 验证
iFormal 在综合后和 ECO 后两次介入：验证综合前后网表等价性，以及局部修改后功能未变。与 iLVS 构成完整的验证闭环。
相关资源
- iLVS — 版图与原理图一致性检查：物理层验证，与 iFormal 逻辑层验证互补。
- iMap — 工艺映射：综合工具，其输出是 iFormal CEC 的典型验证对象。
- EDA 工具总览：22 款点工具能力地图。