SVAで過去のイベントのチェック

SVAでは信号の過去の状態を表すのに$past()が用いられる。例えばとある地点の「１～３クロック前に信号が立ち上がる」を表現するには$past()を用いて以下のように書ける。

１～３クロック前に立ち上がる

//    4 3 2 1|0
//      _____.__
// ____|  ___.__
// ______|  _.__
// ________|
(!$past(a,4) && $past(a,3)) || (!$past(a,3) && $past(2)) (!$past(a,2) && $past(a,1))

しかし、$past()だけではあまり複雑なシーケンスは表現できない。例えば「10クロック前まで」とかになっただけでも$(past)を大量に繋げなくてはならない。又、あまり前の過去の状態を参照するのもシミュレーターの性能上良くなかったりする。
この様な過去のシーケンスを表現するのには<Sequence>.triggeredを利用する事ができる。.triggered自体はシーケンスの終了を示すbooleanで、seq_a ##0 seq_b.triggeredの様にすれば２つのシーケンスが同時に終了する事を意味する。プロパティの右辺で使用されればその事をチェックするプロパティとなる。

シーケンスの同時終了

//                       ______|
// seq_a                |______|
//                  ___________|
// seq_b           |___________|
//                            _|
// seq_b.triggered __________| |

property prop_a_b;
  seq_a |-> seq_b.triggered;
endproperty

なのでそのシーケンスの最後を[*n:m]や##[n:m]ような繰り返しや遅延にする事により、とある地点（＝sdq_aの終了時点）で過去にイベントが起きたかどうかをチェックする事ができる。
冒頭の「１～３クロック前に信号が立ち上がる」の例として「信号aの立ち上がりの時点の１～３クロック前に信号bが立ち上がる」とすれば.triggeredを使って以下の様に書く事ができる。

１～３クロック前に立ち上がる

//        4 3 2 1|0
//               |_
// a : __________|*
// b :      _._._._.
//     ____|^ 1 2 3
//            _._._.
//     ______|^ 1 2
//              _._.
//     ________|^ 1 

sequence seq_b(clk);
  @(posedge clk) $rose(b) ##1 b[*1:3];
endsequence

property prop_a_b;
  $rose(a) |-> seq_b(clk).triggered;
endproperty

ここで注意しなければいけないのは、sequence内で@(posedge clk)と動作点を明示的に指定する必要がある事だ。シミュレータによっては無くても動くものもあるようだが、正式には必要のようだ。
あと、必ずsequneceを使う必要があり、($rose(b) ##1 b[*1:3]).triggeredの様な記述はできない。

以下、EDA Playground上で各社のシミュレータで実行できる例。
SVA Past Event Check