SVA（SystemVerilog Assertion）断言是什么？

更新时间：2026-09-21。问题驱动短答页。断言实战见 SVA 断言实践，形式验证见 形式验证基础，覆盖率见 代码与功能覆盖率。

一句话回答

SVA 断言是用一句声明性的话描述「这个属性必须始终成立」（比如「valid 一旦拉高，在若干拍内必须收到 ready/应答」「请求不允许无响应」），工具在仿真时每一拍自动盯着，条件一旦被违反立刻在发生点报错；同一段属性还能交给形式验证工具从数学上证明是否存在任何反例。它把「翻波形找问题」变成「违例即报错」。

立即断言 vs 并发断言

• 立即断言（immediate）：像过程语句，在 always/if 执行到的那一刻判断，用于检查某个即时条件。
• 并发断言（concurrent）：基于时钟沿、在 property 里描述跨周期时序关系，是协议/接口检查的主力，写在模块内或独立 bind 文件里。

sequence / property 长什么样

sequence req_gnt;
    @(posedge clk) req ##[1:5] gnt;   // req 后 1~5 拍内必须出现 gnt
endsequence

property req_must_get_gnt;
    @(posedge clk) disable iff (!rst_n)
        req |-> req_gnt;              // 一旦 req，就必须满足该时序
endproperty

assert property (req_must_get_gnt)
    else $error("req without grant!");
cover property (req_gnt);            // 同时统计该握手确实发生过（覆盖）

• sequence 描述时序片段，property 组合逻辑关系与蕴含 |->/|=>，assert 检查、cover 统计、assume 约束（供形式）。
• 最常见的是检查 valid/ready、请求-应答、AXI/AHB 协议、FIFO 不能满写空读等，见 valid/ready 握手。

为什么值得写

• 在根因处报错：协议被违反的那一拍就触发，不用从最终数据错误倒翻几千行波形。
• 仿真和形式两用：同一断言既是仿真 checker，又能被形式工具证明对所有输入成立，见 形式验证。
• 可综合子集可进硬件：部分断言在 FPGA 原型上保留做在线检查。
• assert（必须对）+ cover（要发生）一起，把正确性与覆盖率绑定。

常见坑

• 断言写得过严、把合法的多周期/背靠背场景误判成违例，产生假错。
• 忘记 disable iff (!rst_n)，复位期间狂报错。
• 时钟/采样沿写错（用了阻塞即时判断处理跨周期信号）。
• 只在 testbench 写、与 RTL 信号时序对不齐；更稳妥用 bind 把断言模块绑定到 DUT 接口。
• 断言报错但环境没有 fail 机制，错误被淹没在日志里。

总结

SVA 用 sequence/property 以声明方式规定跨周期必须成立的时序属性，并发断言按时钟在仿真中持续监控、违例即在现场报错，同一份属性还能被形式验证数学证明，cover 形式又兼做覆盖率；它最适合守护 valid/ready、请求应答、总线协议和 FIFO 边界等规则，能把事后翻波形的定位成本压缩到违规当场，写的时候注意复位禁用、采样沿和别把合法多周期行为约束得过死。