[SVA] 2. シーケンス (sequence)

SVAの並列アサーションで使用する シーケンス(sequence) の構文について、簡単にですがまとめます。sequence で使用する構文は property でも使えますので、property のみでアサーションを記述することもできます。

　sequence <シーケンス名> (<引数1>, <引数2>, ...);
    ....;
  endsequence

<注釈>
本記事中の S, B の意味は以下になります。

　S : サブシーケンス もしくは ブーリアン
  B : ブーリアン (条件式)

遅延

## を使用して遅延を表現することができます。

S1 ##n S2	S1 の n サイクル後に S2
S1 ##[n:m] S2	S1 の n～m サイクル後に S2
S1 ##[n:$] S2	S1 の n～無制限 サイクル以上後に S2
S1 ##[*] S2	S1 ##[0:$] S2 と同じ
S1 ##[+] S2	S1 ##[1:$] S2 と同じ

■ サンプル

  /* a = 1 の 2～3サイクル後に b = 1 を検出 */
  sequence s1;
    a ##[2:3] b;
  endsequence

繰り返し

[] を使って繰り返しを表現することができます。

S [*n]	S を n 回連続
S [*n:m]	S を n～m 回連続
S [*n:$]	S を n～無制限 回連続
S [*]	S [*0:$] と同じ
S [+]	S [*1:$] と同じ
B [->n]	B を n 回検出
B [->n:m]	B を n～m 回検出
B [=n]	B を n 回検出
B [=n:m]	B を n～m 回検出

■ サンプル

[* ] は条件が連続することを示します。

  /* a = 1 が 2回連続した次のサイクルで b = 1 */
  sequence s1;
    a [*2] ##1 b;
  endsequence

[-> ] と [= ] については条件が連続する必要はなく、条件を満たした回数を監視します。以下の例のように [-> ] と [= ] に後続する処理が無い場合は同じ意味になります。

  /* a を検出後 b を 2回検出 */
  property p1;
    @(posedge clock)  a |=> b [->2];
  endproperty

  /* a を検出後 b を 2回検出 */
  property p2;
    @(posedge clock)  a |=> b [=2];
  endproperty


  SVA_P1 : assert property(p1);
  SVA_P2 : assert property(p2);

但し、以下の例のように [-> ] と [= ] に後続する処理がある場合は意味が違ってきます。ややこしい。

  /* a を検出後 2回目の b の次のサイクルで c を検出 */
  property p1;
    @(posedge clock)  a |=> b [->2] ##1 c;
  endproperty

  /* a を検出後 2回目の b の次のサイクルから 3回目の b までに c を検出 */
  property p2;
    @(posedge clock)  a |=> b [=2] ##1 c;
  endproperty


  SVA_P1 : assert property(p1);
  SVA_P2 : assert property(p2);

下の3枚の波形は信号 c の位置がそれぞれ違います。1枚目の波形は SVA_P1, SVA_P2 共に OK ですが、2,3枚目の波形では SVA_P2 のみ OK であることが分かると思います。

※ちなみにですが、もう1サイクル c をシフトさせると SVA_P2 も発火します。

組み合わせ

複数のシーケンスを組み合わせることができます。(私は and と or しか使った記憶がないですが...)

S1 and S2	S1, S2 を共に満たすこと
S1 intersect S2	S1, S2 を共に満たすこと (同時終了の制約あり)
S1 or S2	S1, S2 のどちらかを満たすこと
first_match S	S にて複数のシーケンスを含む場合に最初に満たしたシーケンスのみ使用
B1 throuthout S2	S2 を満たしているときは B1 の条件を満たすこと
S1 within S2	S2 を満たしているときの S1 を満たすこと