2

triggeredシーケンスのプロパティを使用するアサーションがいくつかあります。これは、「X が発生した場合、Y は過去に発生したに違いない」という形式のプロパティをチェックするのに役立ちます。

簡単な例を見てみましょう：

3 つの信号 、および が与えられaたb場合、3 サイクル前に High であり、2 サイクル前に High であった場合にのみc、cHigh になることが許可されます。これは、このプロパティを満たすトレースです。ab

ここに画像の説明を入力

cこれを確認できるようにするには、 aが有効なポイントで一致するヘルパー (クロック付き) シーケンスが必要です。

  sequence two_cycles_after_a_and_b;
    @(posedge clk)
      a ##1 b ##2 1;
  endsequence

次に、このシーケンスをアサーションで使用できます。

  c_two_cycles_after_a_then_b : assert property (
      c |-> two_cycles_after_a_and_b.triggered )
    $info("Passed");

このアサーションはほとんどの場合問題なく機能しますが、リセットを処理するときはうまくいかなくなります。

と の間のクロック サイクルで正確にアクティブになるリセット信号もあるとしbますc。

ここに画像の説明を入力

この場合の素朴なアプローチは、アサーションの外側、default disable iff節の内側にリセット認識を実装することです。

  default disable iff !rst_n;

cリセットは の前にアクティブだったので、前にa ##1 b発生した はカウントされず、アサーションが失敗することが予想されます。ただし、シーケンスの評価はリセットとは無関係であるため、これは起こりません。

この動作を実現するには、シーケンスをリセット対応にする必要があります。

  sequence two_cycles_after_a_and_b__reset_aware;
    @(posedge clk)
      rst_n throughout two_cycles_after_a_and_b;
  endsequence

アサーションはリセット対応バージョンを使用する必要があります。

  c_two_cycles_after_a_then_b__reset_aware : assert property (
      c |-> two_cycles_after_a_and_b__reset_aware.triggered )
    $info("Passed");

two_cycles...リセットの発生によりシーケンスが一致しないため、2 番目のアサーションは実際に失敗します。

これは明らかに機能しますが、より多くの労力が必要であり、スコープごとに制御するのではなく、リセットをシーケンス/プロパティの不可欠な部分にする必要があります。この場合、を使用することに近いリセット認識を実現する他の方法はありますdisable iffか?

4

1 に答える 1

0

私が思いつく最善の解決策は、サンプリングするための小さな補助コードを追加rst_nし、クロックによってサンプリングされるのに十分な時間、それを低く保つことです。

always @(posedge clk, negedge rst_n) begin
  if(!rst_n) smpl_rst_n <= 1'b0;
  else       smpl_rst_n <= 1'b1;
end

smpl_rst_n次に、ターゲット シーケンスへのリファレンスを使用するリセット対応のジェネリック シーケンスを使用します。

sequence reset_aware(sequence seq);
  @(posedge clk)
  smpl_rst_n throughout seq;
endsequence

最終的なアサーションは次のように機能します。

a_two_cycles_after_a_then_b__reset_aware : assert property (
  c |-> reset_aware(two_cycles_after_a_and_b).triggered )
$info("Passed");

概念実証: https://www.edaplayground.com/x/6Luf

于 2016-10-18T00:58:34.633 に答える