GHDL中PSL断言合成导致的常量反馈环路问题分析

问题背景

在数字电路形式验证过程中，使用GHDL工具对包含PSL(Property Specification Language)断言的VHDL代码进行综合时，发现了一个影响形式验证结果准确性的问题。当使用SymbiYosys进行k-归纳证明时，某些断言会被错误地报告为违反，而实际上这些断言在假设条件下本应成立。

问题现象

通过分析综合后的网表发现，GHDL在合成PSL的always断言时会生成一个特殊的"常量反馈环路"结构。这个结构表现为一个寄存器，其输出直接反馈到输入，形成一个看似没有实际功能的环路。在Quartus生成的原理图中，这些结构被标记为黄色圆圈。

这种结构导致SymbiYosys的k-归纳证明算法出现异常行为，错误地报告断言违反，即使相应的假设条件也被违反。在波形图中可以观察到，输出信号c_out会出现一个时钟周期的脉冲宽度（表明断言失败），而实际上假设a_3本应阻止这种情况发生。

技术分析

深入研究后发现，这种"常量反馈环路"是GHDL处理PSLalways断言时的特定实现方式。该结构由一个简单的D触发器构成，其输出直接反馈到输入，形成一个稳定的状态保持机制。

这种实现方式在功能上是正确的，但在形式验证过程中会带来两个问题：

1. 增加了不必要的状态空间，影响验证效率
2. 在某些情况下会干扰k-归纳证明算法的正确性

特别值得注意的是，这个问题不仅出现在PSL的always断言中，用户自行编写的类似结构（如assume never unstable_a）也可能产生相同的效果。

解决方案

GHDL开发团队已经针对此问题进行了修复。主要优化措施包括：

1. 识别并消除这种冗余的常量反馈环路结构
2. 在适当情况下用常量'1'直接替代环路结构

对于暂时无法升级的用户，建议在使用GHDL综合后，通过Yosys的优化流程来处理生成的网表，以消除这些冗余结构。

经验总结

这个案例揭示了硬件描述语言综合与形式验证工具交互时可能出现的一些微妙问题。开发人员在编写PSL断言时应当注意：

1. 理解不同断言语句的综合结果
2. 在复杂断言组合时特别注意时序关系
3. 验证假设条件的自洽性（如示例中a_2假设可能缺少always修饰）

同时，这也提醒我们形式验证工具链中各组件协同工作的重要性，以及中间表示优化对最终验证结果的关键影响。

后续建议

对于使用GHDL进行形式验证的开发人员，建议：

1. 更新到包含此修复的最新版本
2. 在验证流程中加入适当的网表优化步骤
3. 对关键断言进行交叉验证，确保验证结果的可靠性
4. 在编写复杂PSL断言时，考虑其综合后的实际电路结构

通过这些问题分析和解决方案，我们可以更有效地利用GHDL和SymbiYosys进行硬件设计的形式验证，提高验证结果的准确性和可靠性。