シーケンスが発生した場合、System-Verilogアサーション

Question

でサブシーケンスが発生します。 "シーケンスAが発生した場合、そのシーケンス内でシーケンスBが発生します"。これどうやってするの？

私が主張使うことができると思っているだろう：

assert property (@(posedge clk) (A |-> (B within A)); 

をが、これは私の例のために動作するようには思えません。

私がいることを読んだ：リニアシーケンスは、連続するクロックの有限区間に沿って一致すると言われている

が最初にブール式が最初のクロック・ティックでtrueと評価されてダニ、第二ブール式が評価され2番目のクロックティックで真になり、最後のブール式を含めて最後のクロックティックで真と評価されます。

しかし、私はそれが最初になるようにしたいときにクロックチックが|->最後のクロックティックの反対側に渡されたと思う。

私の特定の例は、私は私が十分に正の数を追加する場合はオーバーフローすることを期待アキュムレータであるので、私はA = (input == 1)[*MAX_SIZE]とB = (output == 0)をしたいので、ここBは、長さ1の配列であることが問題を起こした場合、私は知りません。

私はシステムVerilogの新機能ですので、私のコードの他の部分が間違っているかもしれませんが、この例はどこにも見られませんでした。

Answer 1

Aが既に一致した後に|->演算子の結果が開始されるのは正しいです。 "Aを見たら、B within Aを見たことがありますか？"

これを行うには、シーケンスのtriggeredプロパティを使用できます。

sequence b_within_a; 
    @(posedge clk) 
    B within A; 
endsequence 

assert property (@(posedge clk) A |-> b_within_a.triggered); 

Bも起こった場合b_within_aシーケンスがときtriggered財産である、もちろん、Aの終わりに完全に一致します評価は1になります。

b_within_aシーケンスのクロックは、特に定義されています。これはLRMの要件です。そうでなければ、triggeredを呼び出すことはできません。