system-verilog - シーケンスが発生すると、System-Verilog アサーションでその中にサブシーケンスが発生します。

Question

私が言いたいのは、「シーケンスAが発生する場合、シーケンスはBそのシーケンス内で発生する」ということです。これどうやってするの？

私はアサーションを使用できると思っていたでしょう：

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

しかし、これは私の例ではうまくいかないようです。

私はそれを読んだ：

線形シーケンスは、最初のブール式が最初のクロックティックで true と評価され、2 番目のブール式が 2 番目のクロックティックで true と評価されるという条件で、連続するクロックティックの有限間隔に沿って一致すると言われます。最後のクロックティックで true と評価される最後のブール式。

|->しかし、最初にしたいときに、クロックティックが最後のクロックティックの反対側に渡されたと思われます。

私の特定の例は、十分な数の正の数を追加するとオーバーフローすることが予想されるアキュムレータA = (input == 1)[*MAX_SIZE]です。B = (output == 0)B

私はsystem-verilogに非常に慣れていないので、コードの他の部分が間違っている可能性がありますが、この例がどこでも行われたことはありません。

score 2 · Accepted Answer

すでに一致した後、|->演算子の結果が開始されることは正しいです。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_within_aシーケンスはの最後に正確に一致します。これは、プロパティがに評価されるときでもあります。ABtriggered1

b_within_aシーケンスには、明確に定義されたクロックがあることに注意してください。これは LRM の要件であり、それ以外の場合は呼び出すことができませんtriggered。

1 に答える 1