verilog - 単純な波形の SVA プロパティ

Question

波形：-

私はプロパティを次のようにしました：

property p1;
   a |=> (b == 1)[=2] ##1 (c == 1)[=2]
endproperty

しかし、この特性はこの波形ではうまく機能しません。"c" の前に 3 つ以上の "b" があり、最初の "b" の後の "c" では機能しません。

「a」信号の後に2つの「b」だけを通過させ、「2つのc」を通過させて、その間に任意の量のギャップがあるプロパティが必要です。

手伝ってくれてありがとう。

Answer 1

You do not specify that b should not be 1 when during the pulses on c, nor do you specify that c should not be 1 during the pulses on b.

So, how about something like this:

property p1;
   a |=> ((c == 0) throughout (b == 1)[->2]) ##1 ((b == 0) throughout (c == 1)[->2]);
endproperty

The [->N] operator is the exact non-consecutive repetition operator or goto repetition operator. With goto repetition, the expression must hold in the final cycle of the match; in other words, the match is achieved as soon as the specified number of repetitions has occurred.