GHDL中PSL断言abort与async_abort关键差异解析

在硬件描述语言验证过程中，PSL(Property Specification Language)断言是验证设计正确性的重要工具。本文将深入分析GHDL工具中PSL断言abort与async_abort关键字的差异及其正确使用方法。

问题背景

在VHDL设计中，PSL断言常用于形式验证。其中abort和async_abort关键字理论上应该具有相同功能，都是用于在特定条件下异步终止断言检查。然而在GHDL 4.1.0版本中，使用async_abort会导致工具抛出内部错误，而abort则可以正常工作。

技术分析

语法差异

PSL断言的基本语法结构为：

assert <属性表达式> abort <终止条件> @<时钟事件>

在GHDL 4.1.0版本中，async_abort关键字未被正确处理，导致工具在解析时抛出"cannot handle N_ASYNC_ABORT"错误。这是工具实现上的一个缺陷，因为根据PSL标准，abort实际上是async_abort的别名，两者功能应该完全一致。

修复后的行为变化

GHDL团队在后续版本中修复了这一问题，但同时也修正了async_abort的语义处理方式：

1. 修复前错误处理：

assert always (false) async_abort (reset = '1') @rising_edge(clk);

被错误地解析为：

assert (always false async_abort (reset = '1')) @rising_edge(clk);

这种解析方式会导致断言在第一个复位信号出现时就被完全终止。

2. 修复后正确处理：

assert always (false async_abort (reset = '1')) @rising_edge(clk);

这种解析方式只会终止always属性内部的检查，而不是整个断言。

正确使用建议

1. 对于需要在整个断言周期内异步终止的情况，应使用：

assert always (表达式) sync_abort (条件) @时钟事件

2. 对于只需要在属性内部异步终止的情况，应使用：

assert always (表达式 async_abort 条件) @时钟事件

3. 考虑到代码可读性和工具兼容性，建议优先使用abort而非async_abort，除非明确需要强调异步特性。

版本兼容性说明

• GHDL 4.1.0及之前版本：async_abort会导致解析错误
• GHDL 4.1.0之后版本：async_abort被正确处理，但语义发生变化

设计人员在升级GHDL版本时，需要特别注意这一行为变化，必要时修改断言代码以适应新的解析方式。

总结

PSL断言中的abort机制是验证复杂硬件行为的有力工具。理解abort与async_abort的细微差别，以及不同GHDL版本中的处理方式，对于编写可靠的验证代码至关重要。建议设计人员根据实际验证需求选择合适的终止方式，并在版本升级时进行充分的回归测试。