Yosys等价性检查中的信号命名影响分析

概述

在数字电路设计中，等价性检查是验证两个设计功能是否相同的重要步骤。Yosys作为一款开源的硬件描述语言综合工具，内置了等价性检查功能。本文将深入分析Yosys等价性检查中一个有趣的现象：内部信号命名如何影响检查结果。

等价性检查的基本原理

Yosys的等价性检查基于形式验证技术，通过比较两个设计的逻辑功能来判断它们是否等价。检查过程主要包括以下步骤：

1. 将两个设计分别读入并预处理
2. 创建等价性检查模块
3. 应用多种等价性证明技术（如简单等价性检查、结构等价性检查、归纳法等）
4. 输出检查结果

案例分析

我们通过一个加法器设计的例子来说明信号命名的影响。考虑以下两种实现：

实现1（参考设计）

module adder_small(...);
  // 输入输出声明
  logic sum;
  assign c0 = a + b;
  always_ff @(posedge clk)
    if (spec__03_) sum <= c0;
  // 其他逻辑
endmodule

实现2（待验证设计）

module adder_small(...);
  // 输入输出声明
  logic sum;  // 或改为 impl_sum
  assign sum = _01_ + _00_;
  // 其他逻辑
endmodule

当两个设计中都使用sum作为内部信号名时，等价性检查通过；而当待验证设计中使用impl_sum时，检查失败。

技术原理分析

这一现象源于Yosys等价性检查的工作机制：

1. 信号匹配策略：Yosys会尝试匹配两个设计中名称相同的信号，并假设它们应该等价。这种假设增强了证明能力，为等价性检查提供了额外约束。

2. 证明能力影响：当内部信号名称相同时，检查器会额外验证这些信号的等价性。这种额外的验证约束可以帮助证明更复杂的设计等价性。

3. 归纳法限制：在信号名称不同的情况下，Yosys使用的k-induction方法存在局限性。当设计包含使能信号（如本例中的enable）时，检查器可能无法证明初始状态的等价性。

实际应用建议

1. 命名一致性：在进行等价性检查时，保持内部信号命名一致可以提高检查成功率。

2. 替代方案：对于正式的设计验证，建议使用专门的等价性检查工具，这些工具通常不依赖信号名称匹配。

3. 参数调整：可以尝试增加-seq参数的值，但如本例所示，在某些情况下这可能无效。

4. 设计约束：避免设计中出现可以无限期停滞的状态（如本例中enable长期为低的情况），这会影响等价性证明。

结论

Yosys的等价性检查功能虽然强大，但其内部实现针对的是工具自身的测试需求而非通用设计验证。理解其工作机制和限制对于正确使用该功能至关重要。在实际工程中，应根据具体需求选择合适的验证方法和工具。