4. 断言与属性的编写规范：核心概念、原理机制、实战要点
本章学习任务
掌握断言（Assertion）与属性（Property）的本质区别，理解 SVA 属性在形式化验证中的运行机制，并能够按规范编写具备可读性、可维护性与高定位效率的断言集合。
4.1 问题背景
形式化验证的核心工作不是“运行仿真”，而是用数学手段证明设计满足规格。调试时，定位问题依赖的关键证据就是违反属性的反例轨迹（counterexample trace）。所以，断言的编写质量直接决定了 debug 定位的精度与效率。
- 断言过少：关键协议违反未被捕获，bug 漏出。
- 断言过泛：误报海量，反例与真实 bad behavior 脱节。
- 断言过脆（太紧）：设计合理变化被误判为违反。
4.2 核心概念
以下 5 个概念构成断言与属性的知识底座：
| 概念 | 含义 | 验证角色 |
|---|---|---|
| 断言（Assertion） | 对信号或状态组合的即时或时序检查 | 验证裁判：捕获 bad behavior |
| 属性（Property） | 跨时钟/跨状态的时序行为规范描述 | 验证目标：比断言的规约层级更高 |
| 覆盖点（Coverpoint） | 关键场景是否被激活的统计机制 | 度量验证完整性 |
| 约束（Constraint） | 对输入激励空间的合法范围限制 | 缩小验证空间、避免非法反例 |
| 反例（Counterexample） | 违反属性的完整时间波形序列 | Debug 定位的核心输入 |
提示：属性是“要证明的东西”，断言是“把属性挂到验证环境中的钩子”。一个属性可以被复用为 assert、cover 或 assume。
4.3 原理机制
SVA 属性基于线性时态逻辑（LTL）的可合成子集。验证工具会将属性编译成自动机/监视器，在状态空间搜索中持续跟踪。一旦属性被违反，工具会输出最小化反例轨迹。
- 时序算子：
##（周期延迟）、|->（前置蕴含后续）、|=>（后续蕴含重叠）。 - 时钟与复位：
@(posedge clk)定义采样时钟，disable iff处理异步复位与初始化毛刺。 - 局部变量：在序列中保存中间数据，用于跨时序条件比较。
- 多时钟属性：
@(posedge clk1)与@(posedge clk2)的跨时钟域定序。
下图展示属性编写到验证闭环的完整路径：