0

既に宣言されているプロパティがすべてのクロック サイクルで false かどうかをアサートする方法はありますか?

例えば、

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] 'disable 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は、ステートメントが false の場合にプロパティを true に評価します。

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 に答える