PSL属性语言与形式化验证应用教程 - 第3节

## 第3章 PSL语法结构：四个描述层与属性构建 ### 3.1 问题背景 PSL（Property Specification Language）是用于描述设计行为约束与验证意图的核心语言。学习 PSL 时，最常见的困惑不是“怎么写关键字”，而是“如何从零开始组织一条完整的属性”。这背后隐藏着 PSL 最基本的语法设计思想：**分层描述**。 PSL 将复杂属性拆解为四个描述层——**Boolean、Temporal、Property、Model**。每一层解决一类问题，下层为上层提供基础，上层为下层赋予语义。理解这四个层，就等于掌握了 PSL 语法的“骨架”。 ### 3.2 核心概念：四个描述层 PSL 的属性表达能力由四个层次支撑，每一层都有明确的职责边界： - **Boolean 层**：描述信号、常量、逻辑运算与比较表达式，是最基础的数据单元。 - **Temporal 层**：在布尔表达式上叠加时序算子（如 `always`、`next`、`until`），表达事件在时间轴上的先后关系。 - **Property 层**：将时序逻辑封装为可被验证工具识别和执行的属性声明（如 `assert`、`assume`、`cover`）。 - **Model 层**：将若干属性与假设、环境约束组织在一起，形成可复用、可配置的验证模型。 ### 3.3 原理机制：四层之间的组合关系与语法层次 下图展示了 PSL 四层结构的核心关系：自底向上，逐层组合。底层提供“零件”，上层负责“装配”，最终形成可供形式化验证工具执行的完整模型。 关键组合规则： - Boolean 层是唯一直接接触设计信号的层，其他层都通过 Boolean 表达式获取数据。 - Temporal 层只能叠加在 Boolean 表达式之上，不能脱离布尔层独立使用。 - Property 层将一个或多个时序属性封装为带语义的断言（`assert`）、假设（`assume`）或覆盖点（`cover`）。 - Model 层是最高层，它可以包含多个 Property，并负责约束验证环境（时钟、复位、输入假设等）。 ### 3.4 流程步骤：从简单布尔表达式构建完整属性 按照“从下往上、逐层组装”的思路，构造 PSL 属性可分五步： 1. **识别设计信号** 确定参与属性的接口信号、时钟、复位等基础元素。 2. **写 Boolean 表达式** 用 `&&`、`||`、`!`、`==`、`!=` 等运算符描述信号之间的组合关系。 3. **加时序算子** 在布尔表达式外层叠加 `always`、`next`、`until`、`eventually` 等时序关键词，表达事件的时间先后顺序。 4. **封装为 Property** 使用 `assert`、`assume` 或 `cover` 将时序逻辑转换为可验证的属性声明。 5. **放入 Model 并验证** 在 `model` 结构中组织属性与假设，交给仿真器或形式化工具执行验证。 ### 3.5 案例说明：请求-授权握手协议 以经典请求-授权协议为例，假设信号有：`req`、`grant`、`clk`、`reset`。需要验证的核心属性是：**当请求有效且下一周期没有复位时，授权信号应在下一周期到来**。 **第 1 步：Boolean 表达式** ```psl req == 1'b1 grant == 1'b1 reset == 1'b0 ``` **第 2 步：加时序算子** ```psl always (req == 1'b1 -> next (grant == 1'b1)) ``` 含义：任何时钟周期，若 `req` 为高，则下一周期 `grant` 必须为高。 **第 3 步：封装为 Property** ```psl assert always (req == 1'b1 && reset == 1'b0 -> next (grant == 1'b1)); ``` **第 4 步：放入 Model** ```psl model handshake_protocol { assume always (clk); assume never (reset == 1'b1 && req == 1'b1); assert handshake_property; }; ``` 由此完成了一条从底层信号到顶层验证模型的完整属性构造链路。 ### 3.6 表格总结：四层描述层一览 | 描述层 | 核心元素 | 常用关键字 | 典型示例 | 主要职责 | |--------|----------|------------|----------|----------| | Boolean | 信号、常量、逻辑运算 | `&&` `\|\|` `!` `==` | `req && grant` | 构造底层布尔条件 | | Temporal | 时序算子、序列 | `always` `next` `until` | `always (a -> next b)` | 表达时间先后关系 | | Property | 属性声明、蕴含 | `assert` `assume` `cover` | `assert always (a -> next b);` | 声明可执行验证目标 | | Model | 模型、约束、环境 | `model` `assume` | `model m { ... }` | 组织属性与验证环境 | ### 3.7 误区提醒 - **误区一：把 Boolean 层和 Temporal 层混为一谈** 布尔表达式是纯组合逻辑，不含时间概念；时序算子才描述事件发生的时间关系。两者混用时，属性语义会变得模糊，甚至无法通过语法检查。 - **误区二：跳过 Property 层直接建模** 有些初学者喜欢把所有逻辑直接写在 `model` 中，导致模型庞大且难以维护。正确做法是先用 `assert`/`assume` 封装独立属性，再在 `model` 中引用。 - **误区三：忽略时钟与复位约束** 在 Boolean 层能写出正确表达式，但缺少时钟和复位约束，验证结果往往不可靠。Model 层中的 `assume` 必须明确指定时钟和复位行为。 ### 3.8 实践清单 - [ ] 从信号列表出发，先写下 2~3 个核心布尔表达式 - [ ] 检查布尔表达式中是否混入了时序关键字（`always`/`next` 等） - [ ] 使用 `always`/`next`/`until` 将布尔表达式扩展为时序逻辑 - [ ] 用 `assert` 声明验证目标，用 `assume` 约束环境 - [ ] 将属性放入 `model`，并明确时钟、复位、输入假设 - [ ] 用仿真器或形式化工具跑一次，确认属性不是 “空真”（vacuously true） - [ ] 为每条属性添加注释，说明验证意图，便于后期维护