第1章 PSL语言概览与形式化验证入门

随着芯片规模与设计复杂度的持续攀升，功能验证已占据项目周期的大半成本。传统仿真验证依赖手工构造测试向量，无法穷尽状态空间；而形式化验证能以数学方式对设计行为进行证明。PSL（Property Specification Language）作为一种标准化属性语言，恰好为两类验证手段提供了统一表达框架。本章将建立PSL的宏观认知，并带你在最小环境中运行第一条断言。

1.1 问题背景：为什么需要 PSL

验证工作的核心矛盾在于：缺陷发现越晚，修复成本越高。RTL阶段一次漏检，到系统集成阶段可能要付出数十倍的返工代价。PSL的作用，是让设计者和验证者用简洁、精确的语言描述“设计应当遵守的行为”，并由工具自动检查。

• 验证效率低：波形查看与人工比对难以覆盖复杂时序路径，断言可24小时自动巡检。
• 属性复用难：PSL是IEEE 1850标准，支持跨仿真与形式化平台复用同一套属性。
• 沟通成本高：设计意图用PSL表达后，设计师、验证工程师与EDA工具均能一致理解。

1.2 核心概念：PSL 的四大描述层

PSL采用分层架构设计，从底层到顶层依次为：Boolean（布尔层）、Temporal（时序层）、Property（属性层）、Model（建模层）。上层属性可以直接引用下层结构进行组合，形成从“信号表达式”到“完整验证场景”的递进关系。

四大层各司其职。最低层的 Boolean 层负责信号的基本运算，相当于“组合逻辑的语言”；Temporal 层将运算放入时钟周期维度，使属性具备“之前/之后/持续”等时间语义；Property 层是用户编写断言的主战场，定义“哪些行为必须成立”；Model 层则为验证提供环境模型与时钟定义，是整个形式的根基。

1.3 原理机制：断言在仿真与形式化验证中的执行

同样一个 PSL 属性，可以被两类验证引擎以不同方式执行：

• 动态仿真执行——仿真器在时钟事件驱动下逐拍推进时间，在每个有效时钟边沿对断言中的布尔表达式与时序运算符求值。若断言失败，仿真器记录时间戳、失败位置和信号值，生成报告。
• 形式化验证执行——形式化引擎将设计状态空间抽象为数学形式（如有穷状态机），以穷举或符号推理判断属性在全部可达状态下是否成立。若属性被违反，工具返回一条反例路径。

1.4 实战要点：搭建最小验证环境

搭建一个可运行 PSL 断言的最小环境，只需四步。

1. 编写RTL设计——准备一个简单模块（如握手状态机）。
2. 编写PSL属性——使用 default clock 声明时钟，并用 assert 声明属性。
3. 配置验证工具——在仿真器或形式化工具中启用 PSL 读取与编译。
4. 运行并分析——查看断言通过/失败报告，对失败问题追溯根源。

1.5 案例说明：第一条 PSL 断言

下面是一个经典的握手协议属性：当 req 拉高后，ack 必须在 1 至 4 个时钟周期内被拉高。该属性可嵌入 Verilog 文件，也可独立书写。

// dut.v
module dut(input clk, input req, output reg ack);
  always @(posedge clk)
    if (req) ack <= 1;
    else ack <= 0;
endmodule

// psl_property.psl
default clock = (posedge clk);

property P_REQ_ACK =
  always (req -> eventually [1:4] ack);

assert P_REQ_ACK;