1. 反压期间保持 VALID 和数据稳定property p_axi_payload_hold_when_stalled;(posedge clk) disable iff (!rst_n)(valid !ready) | valid $stable({data, strb, last, id, user});endpropertyassert 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 需要持续保持高电平24个时钟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);endproperty5.动态延迟当 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 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});endpropertyassert 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 需要持续保持高电平24个时钟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);endproperty5.动态延迟当 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