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

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

2025-06-30 20:46:44作者:蔡丛锟

问题背景

在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. 在关键验证场景中,考虑在不同后端下交叉验证结果

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

登录后查看全文
热门项目推荐
相关项目推荐