EDA工具
System
IP
SolvNetPlus
培训中心
定义
等效检查 是“形式验证”这一更广泛学科的一个分支。该技术利用数学建模技术，证明设计的两种表示形式具有相同的行为。这种方法不应与功能验证相混淆，后者通过穷举仿真来验证设计的正确性 。
等效检查 是如何运作的？
等效检查 包含三个基本步骤：
- 设置
- 映射
- 比较
设置阶段的输入包括经过验证的参考设计、库元素以及修订后的设计。在此步骤中，系统将读取这些输入并创建数据结构，以便后续步骤的进行。
在映射过程中，会将设计的关键点进行映射和比较。通常使用逻辑锥来组织比较点。逻辑锥是一个驱动比较点的组合逻辑模块。逻辑锥的输入包括寄存器输出引脚、主输入端口和黑盒输出引脚。比较点包括寄存器、主输出端口和黑盒输入引脚。
在“比较”过程中，系统会检查映射的关键点，以确定它们是等效、非等效还是反向等效。对于返回结果不明确的设计部分，可以投入更多精力重新运行以解决问题。
下图说明了该过程：
Why Equivalence Checking is Important?
在任何典型的复杂SoC设计中，设计流程中都有许多工具会对设计进行处理。除了逻辑综合外，还有功耗优化 步骤、可测试性插入以及功能性ECO，用于解决设计问题或处理设计变更。
所有这些步骤都可能导致设计行为发生细微变化，而这些变化可能在仿真中被忽略，因为仿真的完整性取决于驱动它的测试平台。由于等效检查 基于无向量形式化证明方法，该技术能够捕获在此过程中引入的各种错误。这大大提高了对最终结果的信心。
等效检查 有哪些优势？
等效检查 为任何设计流程提供了强有力的补充。通过应用形式化方法来验证设计的一致性，能够深入了解设计结果的质量，且这种了解并不依赖于测试平台的完整性。具体优势包括：
- 效率更高。对速度较慢的门级仿真的依赖程度更低。
- 信心更足。不必担心工具链或工程变更订单（ECOs）会引入细微的错误。
- 更高质量。该技术可重点 设计中质量较差的RTL编码。
- 可预测性更高。漏检缺陷的可能性更小。
逻辑等效检查 与Sequence的对比等效检查
逻辑等价性检查（等效检查 ，简称LEC）通过分析设计的组合结构，来判断两种替代实现方案的结构是否会表现出相同的行为。如果对设计应用了重新定时等操作，则设计结构将不再map between the two representations。
序列等效性检查（SEC）会考虑时序因素，并在多个时钟周期内检查两个设计表示之间的等效性。
等效检查 和 新思科技
新思科技 提供 Formality 等效检查 该方法利用形式化和静态分析技术，用于判断同一设计的两个版本在功能上是否等价。
新思科技 还提供 VC Formal，该解决方案包含一套全面的形式化应用程序（Apps），包括属性验证（属性验证(FPV) ）、自动提取属性（AEP）、覆盖率分析器（形式覆盖率分析器 ）、连接性检查(CC) ， 顺序等效检查 （时序电路等价验证(SEQ) ）、寄存器验证（FRV）、X传播验证（FXP）、测试平台 分析器（FTA）、回归测试 模式加速器（RMA）、数据路径 、验证 （DPV）、功能安全 (FuSa) ，以及用于验证标准 和总线 协议的一系列断言IP（AIP）。
最后， 新思科技 提供了ESP，这是一款基于符号仿真的定制设计形式验证工具（等效检查 ）。ESP是一种形式验证工具（等效检查 ），通常用于对嵌入式存储器、定制宏、标准 单元以及I/O单元库等定制设计进行全面的功能验证。它用于确保两个设计表示在功能上等价。这些设计可以表示为Verilog 行为模型、RTL、门级、开关，或SPICE 或.db格式的网表 视图。
继续阅读
