Yosys项目中3位加法器验证失败问题分析

问题背景

在Yosys 0.43版本中，用户在使用OpenROAD流程处理ASAP7工艺下的3位加法器设计时，发现等价性验证(eqy)未能通过。该问题出现在逻辑综合后的形式验证阶段，导致设计无法被证明功能等效。

问题表现

当运行包含3位加法器的设计流程时，Yosys能够正常完成综合过程，但在后续的等价性验证阶段，EQY工具报告无法证明"adder.io_dst"分区的等价性。验证失败的具体表现为：

1. 综合过程正常完成，无报错
2. 等价性验证工具EQY启动后，尝试多种策略仍无法证明设计等价
3. 最终验证结果为FAIL，返回码为2

技术分析

从问题描述来看，这很可能与Yosys内部对多比特信号的处理方式有关。3位加法器虽然结构简单，但在某些工艺库映射或优化过程中，可能会产生与原始RTL描述不完全匹配的网表结构。

类似问题在Yosys的issue #3879中也有报告，表明这可能是Yosys在处理特定位宽算术运算时的一个已知问题。问题根源可能在于：

1. 综合优化过程中对加法器结构的转换不够保守
2. 工艺库单元映射后产生的网表结构与RTL描述存在形式差异
3. 等价性验证引擎对多比特算术运算的处理存在局限性

解决方案

根据开发团队的反馈，该问题已在后续版本中通过PR #4691得到修复。修复内容可能涉及：

1. 改进综合引擎对算术运算的处理方式
2. 增强等价性验证引擎识别算术运算等价性的能力
3. 优化工艺库单元映射策略，确保功能一致性

建议措施

对于遇到类似问题的用户，建议：

1. 升级到包含PR #4691的Yosys最新版本
2. 对于关键算术模块，可考虑添加验证断言辅助形式验证
3. 在综合约束中明确指定算术运算的优化策略
4. 必要时可手动实例化工艺库中的算术单元，避免依赖综合优化

总结

Yosys在处理3位加法器这类简单但关键的算术运算时，综合与验证流程可能存在某些边界情况。开发团队已意识到这类问题并持续改进相关算法。用户在实际应用中，特别是针对算术密集型设计，应当关注工具版本更新并建立完善的验证流程。