GHDL项目中PSL断言处理长布尔AND表达式时崩溃问题分析

问题现象

在使用GHDL进行VHDL代码综合时，当PSL(Property Specification Language)断言中包含较长的布尔AND表达式时，GHDL会意外崩溃。具体表现为：当开发者将多个条件检查合并为一个长AND表达式时，GHDL抛出内部错误并终止运行；而将这些条件拆分为多个独立断言时，则能正常工作。

技术背景

PSL是VHDL中用于形式验证的一种属性规范语言，允许开发者编写时序和组合逻辑断言。GHDL作为开源的VHDL仿真和综合工具，支持PSL特性的处理。在硬件设计中，这类断言常用于验证复位状态下信号的行为。

问题复现

开发者提供了一个典型的使用场景：

-- 正常工作方式（多个独立断言）
assert always rst = '1' -> s1_crs_dv = '0';
assert always rst = '1' -> s1_er     = '0';
assert always rst = '1' -> s1_d      = "00";

-- 导致崩溃的方式（合并为长AND表达式）
assert always rst = '1' ->
    s1_crs_dv = '0'   and
    s1_er     = '0'   and
    s1_d      = "00"  and ...

当使用第二种方式时，GHDL会抛出"synth_psl_expr: cannot handle N_IMP_BOOL"错误并崩溃。

根本原因

根据错误信息和代码分析，问题出在GHDL的PSL表达式处理模块中。当遇到复杂的布尔AND表达式时，代码未能正确处理隐含的布尔逻辑转换(N_IMP_BOOL节点类型)，导致内部断言失败。

解决方案

目前有两种可行的解决方案：

1. 拆分断言：将长AND表达式拆分为多个独立断言，如示例中的第一种方式。这种方法简单可靠，是推荐的临时解决方案。

2. 使用VHDL原生断言：如评论中提到的，可以考虑使用VHDL自带的assert语句替代PSL断言，虽然表达能力稍弱，但在这种情况下更加稳定。

技术建议

对于硬件验证工程师，在处理复位状态验证时，建议：

1. 对于关键信号，优先使用独立断言，提高可读性和调试便利性
2. 在必须使用复杂布尔表达式时，考虑分阶段验证
3. 关注GHDL的更新，该问题已被标记为修复状态

未来展望

该问题已被GHDL开发团队确认并修复，预计会在后续版本中发布。对于依赖复杂PSL断言的用户，建议在升级后重新评估代码结构，平衡表达简洁性和工具兼容性。

在硬件验证实践中，断言是强大的验证工具，但需要考虑工具链的支持程度。合理设计断言结构既能保证验证效果，又能避免工具链限制带来的问题。