sva日常学习0

1. 反压期间保持 VALID 和数据稳定

property p_axi_payload_hold_when_stalled;
@(posedge clk) disable iff (!rst_n)
(valid && !ready) |=> valid && $stable({data, strb, last, id, user});
endproperty
assert property (p_axi_payload_hold_when_stalled);

2. ## 延迟 —— APB Setup → Access 时序检查

(psel && !penable)
|=>(psel && penable && $stable(paddr) && $stable(pwrite));

3. 重复运算符 [*N] —— AXI 连续反压检查

(WVALID && !WREADY)|=>WVALID[*1:3];
req |=> busy[*2:4] ##1 done;

当 req 信号在某个时钟周期有效，下一个时钟开始， busy 需要持续保持高电平2～4个时钟；
busy结束之后，再等待1个时钟周期， done 必须拉高。

4.请求时记住 X，响应时检查 X

可以想到这个模板：
property p_req_rsp_match;

logic [WIDTH-1:0] saved_value;

@(posedge clk)
disable iff (!rst_n)

(req_fire,
saved_value = req_value)

|->
##[MIN:MAX]

(rsp_fire &&
rsp_value == saved_value);

endproperty

5.动态延迟

当 dma_req 出现时，读取当时的 timeout_cfg。dma_ack 必须在 1 到 timeout_cfg 个周期内返回。局部变量 + 重复 sequence + 计数递减 + first_match(),一种典型思路：
property p_dma_dynamic_timeout;

int cnt;

@(posedge clk)
disable iff (!rst_n)

(dma_req, cnt = timeout_cfg)
|->
first_match(
(##1 !dma_ack, cnt = cnt - 1)[*0:$]
##1 (dma_ack && cnt >= 0)
);

endproperty