数据路径与控制路径模块的形式等价验证

SNUG China 2022 2022 29 页

形式等价验证是确认两个设计表示之间功能一致性的方法。它在芯片设计流程中有三种主要形式：

方法	工具	检查范围
布尔等价	Synopsys Formality	比较组合逻辑的布尔扇入逻辑
时序等价（SEQ）	Synopsys VC Formal SEQ	假设相等输入和初始状态，比较每个周期的输出（无界证明）
事务等价（DPV）	Synopsys VC Formal DPV	比较非时序事务级模型与周期精确模型在事务结束时的输出

对于数据路径密集型模块（如算术运算单元），RTL 与高级参考模型（如 C/C++ 算法模型）之间的等价验证尤为困难。传统的基于仿真的方法覆盖率有限，而布尔等价工具无法处理不同抽象层次之间的差异。

VC Formal DPV（Data Path Verification）专为算术数据路径设计：

- 支持浮点和定点运算的形式化等价证明 - 可以在 RTL 和 C 参考模型之间建立等价关系 - 自动检测流水线级数差异和时序重排

控制路径模块中广泛使用自动时钟门控（Auto-Clock-Gating）以降低动态功耗。然而，时钟门控的插入改变了设计的周期级行为，使得传统的布尔等价检查不可行。

VC Formal SEQ（Sequential Equivalence Checking）能够：

- 处理插入时钟门控前后的时序差异 - 证明门控和非门控设计在所有可达状态下的功能等价 - 自动推断状态映射关系

本文介绍了 Synopsys 形式等价验证工具在数据路径和控制路径模块中的应用。VC Formal DPV 和 SEQ 分别针对算术数据路径和时序优化后的控制路径提供了超越传统布尔等价检查的验证能力。

概念	说明
形式等价验证 Formal Equivalence Checking	证明两个设计表示功能一致性的方法
VC Formal DPV	Synopsys 数据路径验证工具，支持 RTL 与参考模型的形式化等价证明
VC Formal SEQ	Synopsys 时序等价检查工具，处理时钟门控等时序优化后的等价验证
Formality	Synopsys 布尔等价检查工具（组合逻辑等价）