1

私は正式に動作を確認するために、SVAでプロパティを書きたいです。ここでSystem Verilogアサーションでプロパティを書き込む方法は?

は、私が欲しいものです:

property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    $fell(sig1) ##[1:$] first_match($fell(sig2)) ##0 sig3 |-> sig4 == sig3; 
endproperty 

SIG1が落ちた後、それが残りの評価サイクルの間LOW留まるようにどのように私は、上記のプロパティを書き換えることができますか?

注:私は無効IFF(SIG1)

感謝としてSIG1を入れたくありません!

+0

でシーケンス以上16.9.9条件は_precondition_または_condition_の一部「SIG1が落ちた後、それが残りの評価サイクルの間LOWのまま」となっていますか?言い換えれば、あなたはそのSIG4を確認したいん== SIG3 _if_ SIG1低いままか、そのSIG1を_check_したいですが、低とどまっただけでなく、SIG4 = SIG3をチェックしていますか? –

答えて

2
property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    (!sig1) throughout (##[1:$] first_match($fell(sig2)) ##0 sig3) 
      |-> sig4 == sig3; 
endproperty 

参照セクション1800から2012 LRM

+0

ありがとう!もう1つのクエリ:16の連続したサイクル(sig4 == sig3)[* 16]で結果/満足のいくシーケンスを検証するために、このプロパティをどのように拡張できますか? また、sig1 == 1'b0; – kkdev

+0

あなたは結果として**を通して**を使うこともできますが、簡単な場合は '(!sig1 && sig3 == sig3)[* 16]' –

+0

とすることができます。最初の入力では、ツールはsig1が1'b1の反例を見つけようとします。私は結果として「全体」を使用しようとしましたが、成功しませんでした。 私は以下のようなものを試すことはできますか? (!SIG1)全体(## [1:$] first_match($(SIG2)に落ちた)## 0 SIG3 | - > SIG4 == SIG3) – kkdev

関連する問題