3. 安全属性建模基础
在Jasper这类形式验证工具中，安全属性建模的核心任务是把“设计必须满足什么”从自然语言翻译成工具能够判定真假的数学对象。这个翻译过程依赖三层要素：属性描述语言提供书写载体，时序逻辑提供时间维度的语义，安全属性分类决定我们该用哪种模板去表达。三者缺一不可，理解它们的配合关系，才能写出既正确又能被证明引擎高效处理的属性。
属性描述语言：SVA与PSL的定位
Jasper支持SystemVerilog Assertion（SVA）和Property Specification Language（PSL）两种主流属性描述语言。SVA与Verilog/SystemVerilog语法同源，在RTL设计中最为常见；PSL则更偏规范层，适合在验证计划早期描述高层协议。两者在表达能力上高度重叠，本节以SVA为主线讲解，因为它在Jasper的property检查中最为直接。
SVA属性由序列（sequence）和属性（property）两级构成。序列描述信号在时间轴上的布尔模式，属性则在序列之上加入蕴含、时钟、复位等约束。一个典型的属性写法如下：
property p_req_ack;
@(posedge clk) disable iff (!rst_n)
req |-> ##[1:3] ack;
endproperty
a_req_ack: assert property (p_req_ack);这段代码表达的是：在时钟上升沿采样，若复位无效且req为高，则在随后1到3个周期内ack必须为高。|->是重叠蕴含，##[1:3]是延迟窗口。Jasper在证明该属性时，会把它展开为状态机可达性判定，而不是逐周期仿真。
时序逻辑：把“什么时候”说清楚
安全属性之所以需要时序逻辑，是因为硬件行为本质上是状态序列。SVA提供的时序算子可以分成四类：
- 延迟算子：
##n表示固定延迟n个周期，##[m:n]表示窗口延迟。 - 重复算子：
[*n]表示连续重复n次，[*m:n]表示重复次数范围，[->n]表示非连续重复。 - 蕴含算子：
|->重叠蕴含（当前周期即开始匹配后续），|=>非重叠蕴含（下一周期开始匹配）。 - 时钟与复位：
@(posedge clk)定义采样时钟，disable iff定义异步复位屏蔽条件。
这些算子的组合决定了属性的“时间形状”。例如req |=> ##2 ack与req |-> ##[1:3] ack在语义上完全不同：前者要求固定在第3个周期，后者允许1到3周期的弹性窗口。在Jasper中，窗口越宽，证明难度通常越高，因为需要搜索的状态空间更大。
安全属性的分类与表达模板
从验证意图出发，安全属性通常分为四类，每类都有对应的表达模板：
| 类别 | 含义 | SVA表达要点 |
|---|---|---|
| 不变式（Invariant） | 任何时刻都必须成立的条件 | 直接写布尔表达式，或always属性 |
| 响应式（Response） | 一个事件触发后，另一个事件必须发生 | trigger |-> ##[m:n] response |
| 互斥式（Mutual Exclusion） | 两个信号不能同时有效 | !(a && b)作为不变式 |
| 序列式（Sequence） | 多个事件按特定顺序出现 | 用##和重复算子串联 |
以FIFO控制器为例，一个典型的不变式是“读写指针不能同时指向同一位置且同时有效”：!(wr_en && rd_en && (wr_ptr == rd_ptr))。一个响应式属性是“写请求后，若FIFO未满，则满标志在2周期内更新”：wr_en && !full |-> ##[1:2] $changed(full)。这些属性直接对应Jasper中的assert property语句。
从自然语言到可证明属性的转换路径
实际建模时，最容易出错的是把“设计意图”直接写成“实现细节”。例如“FIFO不应溢出”是意图，而“当count == DEPTH时wr_en必须为低”是实现约束。Jasper证明的是属性在RTL所有可达状态上是否成立，因此属性应当描述可观察行为，而不是内部信号的具体取值。下面这张图展示了从需求到可证明属性的转换关系，以及四类安全属性在时序轴上的典型形态。
图中左侧的转换路径强调一个关键原则：先确定属性类别，再选择时序算子。如果把响应式属性误写成不变式，Jasper可能因为无法捕捉跨周期行为而给出“Proven”的假象；反之，把不变式写成带窗口的响应式，会引入不必要的状态搜索，导致证明时间膨胀。
建模时的常见陷阱与检查要点
在Jasper中提交属性前，建议做三项检查。第一，复位语义检查：确认disable iff覆盖了所有异步复位源，否则属性可能在复位释放瞬间产生虚假反例。第二，采样沿一致性检查：同一组属性应使用相同的时钟域，跨时钟域属性需要显式声明@(posedge clk_a)和@(posedge clk_b)，并配合同步器建模。第三，窗口边界检查：##[m:n]中的n不宜过大，通常建议不超过协议规定的最大响应延迟，否则会显著增加证明复杂度。
assign full = (count == DEPTH)直接写成属性full == (count == DEPTH)，这种属性在Jasper中会被证明为真，但它没有增加任何验证价值，因为它只是重复了实现。一个实用的建模顺序是：从需求文档中提取“必须永远成立”的条件作为不变式，提取“触发—响应”对作为响应式属性，提取“不能同时发生”的信号对作为互斥式属性，最后把多步协议流程写成序列式属性。每类属性在Jasper中都可以独立提交、独立查看证明结果，便于定位是设计缺陷还是属性本身写错。
当属性被Jasper证明为“Proven”时，说明在RTL所有可达状态下该属性均成立；当返回“CEX”（反例）时，工具会给出从初始状态到违反属性的具体波形路径。此时应优先检查属性是否过强或过弱，再判断RTL是否存在真实缺陷。属性建模的质量，直接决定了后续逻辑等价验证的可信度。