数字IC验证中，使用‘SystemVerilog Assertions (SVA)’进行断言检查，在实际项目中常用的复杂序列（sequence）和属性（property）有哪些例子？

我们项目里用SVA最多的地方就是AXI总线了。比如检查AXI4的写地址通道，要求awvalid一旦拉高，必须等到awready也拉高才能拉低。这个用SVA写起来就很简单：property p_aw_valid_until_ready; @(posedge clk) disable iff (!rst_n) $rose(awvalid) |-> awvalid throughout awready[->1]; endproperty。 这个能有效抓到那些awvalid提前撤掉的问题。

还有状态机非法跳转，我们一般会为每个状态写一个property，比如从IDLE状态只能跳到CONFIG或IDLE自己，不能跳到其他状态。用case语句把每个状态的合法next_state列出来，然后用assert property检查。

平衡性能和覆盖率的话，我们的经验是：对于非常高频的信号（比如每个周期都可能变化的），慎用assert，尤其避免在property里用复杂的序列嵌套和大量$past，仿真会慢。可以把这类检查放到scoreboard里用SV写。SVA更适合检查那些协议明确、周期精确的时序关系。

实际项目中，除了协议检查，SVA在数据一致性检查上也很好用。举两个我们常用的复杂例子：

一个是FIFO的指针关系。我们不光检查空满标志，还检查读写指针的数学关系。比如定义一个property，确保写指针追上读指针时（特定差值），full信号必须为1。这个用sequence组合起来：sequence s_ptr_wrap; (wr_ptr – rd_ptr) == DEPTH; endsequence property p_fifo_full; @(posedge clk) disable iff (rst) s_ptr_wrap and wr_en and !rd_en |=> full; endproperty。 这种检查能发现指针计算逻辑的深层次bug。

另一个是跨时钟域（CDC）的简单一致性检查，注意，这里不是替代CDC验证工具，而是辅助。比如对同步打两拍后的信号，检查它不应该在目标时钟域出现毛刺或多次跳变。可以用$stable结合时钟来检查。

关于性能，我们会在回归的不同阶段开关断言。初期和debug阶段全开，大规模回归时，会把一些已经稳定、或者计算复杂的断言用`ifdef包起来，只开核心的。另外，避免在property里使用全局变量和复杂的函数调用，尽量用信号直接组合。

从验证工程师的角度，SVA最实用的就是抓那些“不该发生”的事情。书上例子太理想，我说几个接地气的。

比如检查中断行为：当中断信号intr被置起后，必须等到软件写特定清零寄存器才能拉低，中间不能自己掉下去。property p_intr_hold; @(posedge clk) $rose(intr) |-> intr until (reg_clear == 1‘b1); endproperty。 这种检查用传统写testbench的方式很啰嗦，用SVA一行断言，仿真自动报错，效率高。

再比如检查配置锁存：当配置使能信号cfg_en高时，配置数据cfg_data必须稳定，不能变。用$stable(cfg_data)配合cfg_en很容易写。

平衡覆盖率和性能，我的原则是：对关键协议路径（比如握手、仲裁、错误响应）必须用SVA断言，这是第一道防线。对于数据路径的复杂关系（比如一个数据包进来，经过处理，出来的结果要符合某种算法），更适合在scoreboard或参考模型里检查，因为SVA描述这种多周期、多变量的数据变换会很吃力，仿真开销大。

另外，多利用SVA的cover property来覆盖时序场景，比如“awvalid拉高后，在awready拉高之前，awaddr是否稳定”可以作为一个cover point，这样断言不仅是检查器，也是覆盖率收集器。