system-verilog - 如何在系统 verilog 断言中编写属性？

Question

我想在 SVA 中编写一个属性来正式验证一个行为。

这是我想要的：

property prop1(sig1,sig2,sig3,sig4);
    @(posedge clk)
    $fell(sig1) ##[1:$] first_match($fell(sig2)) ##0 sig3 |-> sig4 == sig3;
endproperty

如何重写上述属性，以便在 sig1 下降后，它在剩余的评估周期内保持低电平？

注意：我不想将 sig1 设为禁用 iff (sig1)

Answer 1

property prop1(sig1,sig2,sig3,sig4);
    @(posedge clk)
    (!sig1) throughout (##[1:$] first_match($fell(sig2)) ##0 sig3) 
          |-> sig4 == sig3;
endproperty

请参阅第 16.9.9 节1800-2012 LRM中序列的条件