IEC 62531：属性规范语言（PSL）用于数字电路形式验证

IEC 62531源自IEEE Std 1850，定义了属性规范语言PSL，这是一种用于描述数字硬件设计属性的形式化语言。PSL使工程师能够以精确、无歧义的方式表达复杂的时序行为和约束，这些属性和约束可以通过动态仿真和形式验证工具进行验证。随着集成电路设计复杂度的指数级增长，传统的纯仿真验证方法已不足以确保功能正确性。PSL与SystemVerilog断言一起，为基于断言的验证方法学提供了基础，这种方法已成为半导体行业不可或缺的技术。

PSL语言架构与时序逻辑基础

PSL语言构建在四层架构之上。布尔层由设计信号上的标准布尔表达式组成。时序层提供基于线性时序逻辑扩展了顺序扩展正则表达式的算子，用于指定随时间变化的行为。验证层提供assert、assume和cover等指令，告诉验证工具如何处理属性。建模层允许辅助代码支持属性规范。

时序算子是PSL的核心。基本的LTL算子包括always（全局）、never（全局否定）、eventually!（将来必然）、until!（强直到）、before和next。这些算子通过@算子补充了时钟变体，允许属性相对于特定时钟沿进行指定。SERE层支持类似正则表达式的方式指定顺序行为，算子包括连接、融合、Kleene星号和布尔交集。

基于断言的验证方法与工程实践

PSL支持三种验证指令。assert指令指定必须始终成立的属性。assume指令指定对设计环境的约束。cover指令指定覆盖点，跟踪仿真过程中是否执行了某些行为。从工程方法学的角度来看，有效的PSL使用遵循几种既定模式：接口协议属性的规范、使用PSL assume指令约束形式验证工具、以及使用cover指令定义功能覆盖点。行业经验表明，具有全面PSL断言的设计在验证过程中缺陷发现率提高30-50%，硅后缺陷减少40-60%。

基于PSL形式验证的工程设计要点

在实际验证流程中有效部署PSL需要关注几个工程考量。首先，属性集必须作为设计规范的一个组成部分来开发，而不是在验证阶段才事后添加。最佳实践是在架构阶段捕获PSL断言，在RTL编码开始之前将属性转化为可执行的规范来指导实现。其次，PSL属性的复杂度显著影响形式验证工具的性能。高度复杂的属性可能导致模型检验中的状态空间爆炸。工程师应将复杂属性分解为更小、更简单的断言。第三，PSL assume指令与复位序列之间的交互需要仔细设计。PSL提供了default clock和复位处理结构来管理这些场景。