形式化验证基础与PSL角色

本章导读：芯片验证最怕的不是发现问题，而是不知道还有多少问题没有被发现。传统动态仿真用有限激励采样设计行为，而形式化验证试图在数学意义上证明“设计满足预期”。PSL（Property Specification Language）正是把“预期”转化为机器可判定属性的桥梁。本章回答四个问题：动态验证与静态验证有何本质差异？属性与断言是什么关系？形式化引擎如何证明属性？哪些场景真正适合用 PSL？

问题背景：随着总线协议、流水线互锁、安全机制越来越复杂，单纯依赖仿真已经难以覆盖所有并发分支。验证工程师需要一种不依赖测试向量、能够穷尽遍历状态空间的验证手段。PSL 属性语言应运而生，它让工程师用简洁的时态逻辑描述“请求后最终有授权”“读写不允许同时拉高”等设计意图，并交给形式化引擎证明。下面这条链路是本章的核心地图：从设计意图出发，到 PSL 属性、形式化引擎、证明/反例，最终收敛。