属性形式化验证怎么写？

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

属性形式化验证怎么写？

How to write property for formal verification?

formal-verification

system-verilog

system-verilog-assertions