system-verilog - 如何写属性进行形式验证？

Question

property prop1;
@(posedge clk)
$fell(sig1) ##1 sequence1 |-> sequence2;
endproperty

我想iff sig1=1'b1在第一个时钟周期后禁用该属性。

从高到低的转变sig1是我的触发条件。如果我这样做disable iff(sig1)触发条件将不会被满足。

throughout在正式验证器中的启用和满足序列上也无法使用。

我该怎么做？谢谢！

Answer 1

如何编写一些卫星代码来导出延迟版本sig：

  always @(posedge clk) sig1d <= sig1;

  property prop1;
    @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 sequence1 |-> sequence2;
  endproperty

http://www.edaplayground.com/x/2tbX

Answer 2

sig1您可以重新编写断言，仅在第一个周期后看不到高电平时触发：

property prop1;
  @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 !sig1 ##0 sequence1 |-> sequence2;
endproperty