アサーションで 'sequence.triggered'を使用するときのリセット認識

Question

シーケンスのtriggeredプロパティを使用するアサーションがいくつかあります。これは、「Xが起きたとき、Yがいつか過去に起こったことがある」というフォームのプロパティをチェックするのに便利です。

簡単な例を見てみましょう：aは3サイクル前に高く、bは2サイクル前に高いものであった場合は三つの信号、a、bとc、cを考えると

が高いだけ行くことを許されています。これは満たし、このプロパティをトレースです：

：

はこれをチェックすることができるようにするには、我々はヘルパー（クロックさ）cが合法である点で一致している必要がありシーケンスを必要とするだろう

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; 

期待がリセット以降前にアクティブであった、ということであろう10の場合、以前に起きた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...シーケンスは、リセットの発生のために一致しません。

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

Answer 1

私が思いつくことができる最善の解決策は、サンプル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"); 

証明： `two_cycles_afterを持って、より合理的ではなかったならば、私も思ったんだけどhttps://www.edaplayground.com/x/6Luf