SV
req ##1 ack
req ##2 ack
req ##N ack
( a ##1 b ) ##0 ( c ##1 d ) // b,c in the same time
a ##1 b && c ##1 d // equivalent to above
req ##[4:32] ack // ack is true at some cycle in 4-32
req ##[4:$] ack
req ##2 ack ##3 1'b1 // expand the length of seq
a ##1 b ##1 b ##1 b ##1 c // b is true in 3 cycles
a ##1 b [*3] ##1 c // equiv to above
( a ##2 b ) [*3] // (a-->b)->(a-->b)->(a-->b)
a [*1:5] // a[*1] or a[*2] or ... or a[*5]
$sampled ( exp )
$rose ( exp [, [clk_event] ] )
$fell ( exp [, [clk_event] ] )
$stable ( exp [, [clk_event] ] )
$changed ( exp [, [clk_event] ] )
$past ( exp [, [num_of_ticks] [, [exp] [, [clk_evt] ]]] )
a_ok : assert property ( @clk a==b )
else $error ("a=%b,b=%b", $sampled(a), $sampled(b));
seqA and seqB
// seqA, seqB を同時刻に評価開始
// 両方が true のシーケンス
// 時刻は長い方の終了時刻
seqA intersect seqB
// 短い方の終了時刻になる点が and との違い
seqA or seqB
// どちらかが true のシーケンス
first_match ( a ##[2:5] b )
// a ##2 b から a ##5 の中で最初にマッチしたもの
exp throughout seqA
seqA within seqB
シーケンス宣言は省略
-> や => は property の演算子
seq_expr ::= // sequence_expr
cycle_delay_range seq_expr // これの繰り返し
| seq_expr cycle_delay_range seq_expr // 繰り返し
| experssion_or_dist [ boolean_abbrv ]
| seq_instance [ seq_abbrv ] // seq_id 呼び出し
| ( seq_expr {, seq_match_item } ) [ seq_abbrv ]
| // seq_expr の and, intersect, or
| first_match, througout, within, clocking_event
cycle_delay_range ::=
## constant_primary
| ## [ cycle_delay_const_range_exp ]
| ## [*]
| ## [+]
cycle_delay_const_range_exp ::=
const_exp : const_exp
| const_exp : $
boolean_abbrv ::=
consecutive_repetition
| non_consecutive_repetition
| goto_repetition
consecutive_repetition ::=
[* const_or_range_exp ]
| [*]
| [+]
const_or_range_exp ::= const_exp
| cycle_delay_const_range_exp
exp_or_dist ::= exp [ dist { dist_list } ]
non_consecutive_repetition ::=
[ = const_or_range_exp ]
goto_repetition ::= [-> const_or_range_exp ]