代码之家 › 专栏 › 技术社区 › kkdev

如何编写用于正式验证的属性?

system-verilog-assertions formal-verification system-verilog

0

kkdev · 技术社区 · 9 年前

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

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

打开从高到低的转换 sig1 是我的触发条件。如果我这样做了 disable iff(sig1) 将不满足触发条件。

还使用 throughout 在正式验证器中,启用和满足序列都不可能。

我该怎么做? 谢谢

2 回复 | 直到 5 年前

1

0

Matthew Taylor 9 年前

写点怎么样 卫星代码 派生的延迟版本 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

2

0

Tudor Timi 9 年前

如果看不到,可以重新编写断言以仅触发 sig1 第一次循环后为高:

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