0

有没有办法在每个时钟周期断言已声明的属性是否为假？

例如，

status[idx]req[idx]只有当两者都为高时才应enable[idx]为高。

我想要的是针对上述情况的负面情景检查器。即当或或低status时，不应该变高。reqenable

我在下面尝试过，但是 vcs 给了我下面的编译错误

sequence seq_a (int idx);
  !(req[idx] & enable[idx])
endsequence

sequence seq_b (int idx)
  status[idx] == 1
endsequence

property ppty_ab (int idx)
  disable iff (f_req[idx] & f_enable[idx])
  seq_a(idx) |=> seq_b(idx)
endproperty

generate
  for (idx=0; idx<5; idx++) begin
    a_ab : assert property (@(posedge clk) (not ppty_ab(idx)))
           else $display("ppty_ab [%0d] failed at %t",idx,$time)
  end
endgenerate

错误-[PIWDOAACS] 不正确使用“禁用 iff”

带有 'disable iff' 的属性实例只允许在“assert”、“assume”和“cover”语句中使用。属性 p_RiseIntDischeck 可能不会在此上下文中实例化。

seq_a并且seq_b已经被声明并用于其他一些断言。重用这些序列并为上述情况创建负面场景检查器的最佳/推荐方法是什么？

4

2 回答 2

0

尝试将时钟和not属性放入属性本身。

那是：

property ppty_ab (int idx)
  @(posedge clk)
  disable iff (f_req[idx] && f_enable[idx])
  not seq_a(idx) ##1 seq_b(idx)
endproperty

generate
  for (idx=0; idx<5; idx++) begin
    a_ab : assert property (ppty_ab(idx))
           else $display("ppty_ab [%0d] failed at %t",idx,$time)
  end
endgenerate

wherenot seq_a(idx) ##1 seq_b(idx)与 不同!seq_a(idx) |=> seq_b(idx)，not但当语句为假时，将使属性评估为真。

我假设这disable iff需要对该属性进行计时，尽管我不确定为什么。

于 2016-10-17T07:05:22.080 回答
0

您的负面属性可能如下所示：

property ppty_ab (int idx);
  @ (posedge clk)
  disable iff (f_req[idx] & f_enable[idx])
  !req[idx] | !enable[idx] |=> !status[idx];
endproperty

genvar idx;
generate
  for (idx=0; idx<5; idx++) begin
    a_ab : assert property (ppty_ab(idx))
      else $display("ppty_ab [%0d] failed at %t",idx,$time);
  end
endgenerate
于 2016-10-18T02:57:14.047 回答