GHDL项目中的PSL验证测试失败问题分析

问题背景

在GHDL 4.0.0版本中，用户报告了两个与PSL(Property Specification Language)相关的测试用例(issue880和ticket24)在x86_64架构下使用mcode后端时出现失败。这两个测试用例在使用LLVM或GCC后端时能够正常通过，但在mcode后端下却出现了不一致的结果。

问题表现

测试失败的具体表现为PSL报告中"started-count"字段的预期值与实际值不匹配：

• 预期值：3
• 实际值：8

这种差异表明在mcode后端下，PSL属性的触发次数与预期不符，可能导致验证结果不可靠。

问题定位

经过开发团队调查，发现这个问题不仅限于x86_64架构下的mcode后端，在ppc64el架构下使用LLVM后端时也能复现相同的问题。这表明问题可能与特定架构或后端实现相关，而非仅限于mcode后端。

解决方案

开发团队在后续提交中修复了这个问题。修复后的版本经过验证，确认解决了PSL验证测试失败的问题。值得注意的是，这个问题在Windows平台的CI测试环境中无法复现，说明它可能与特定平台或工具链版本有关。

版本发布情况

虽然问题已在代码库中修复，但GHDL 4.1版本已经发布且未包含此修复。目前开发团队没有计划发布包含此修复的4.0.x维护版本。

技术建议

对于依赖PSL验证的用户，建议：

1. 如果遇到类似问题，可以尝试切换不同的后端(如LLVM或GCC)
2. 关注GHDL的后续版本更新，特别是当需要使用mcode后端时
3. 在关键验证场景中，考虑在不同后端下交叉验证结果

这个问题提醒我们，在不同架构和后端下，硬件描述语言的仿真行为可能存在细微差异，特别是在涉及断言和属性验证时，需要特别注意验证结果的一致性。