SV
property p1;
@ ( posedge clk ) a |-> b ##1 c ;
endproperty
property p1;
@ ( posedge clk ) disable iff (e) a |-> b ##1 d ;
endproperty
// 以下は等価
seq_exp |=> property_exp
seq_exp ##1 1'b1 |-> property_exp
$rose (data) |-> ##[1:5] ready
// -> のネストも可能
// disable iff は default disable iff として property の外でも定義できる
プロパティ宣言だけではプロパティは評価されない。並列アサーション文の記述が必要。
モジュール本体
インターフェイス本体
パッケージ本体
A compilation-unit scope ( トップ階層のこと？)
genearete block
program, clocking block, checker
// property_declaration は assertion_item_decl の一つ
property_declaration ::=
property property_id
[ ( [ property_port_list ] ) ] ;
{ assertion_variable_declaration }
property_spec [ ; ]
endproperty [ : property_id ]
property_port_list ::=
property_port_item { , property_port_item }
property_port_item ::=
{ attr } [ local [ input ] ]
property_formal_type formal_port_id
{ variable_dimension } [ = property_actual_arg ]
property_formal_type ::= sequential_form | property
property_spec ::=
[ clocking_event ]
[ disable_iff ( expression_or_dist ) ]
property_expr
property_expr ::=
sequence_expr
| strong ( sequence_expr ) | weak ( seqence_expr ) // ここまでシーケンス・プロパティという
| ( property_expr )
| << property_exp の not, or, and >>
| sequence_expr |-> property_expr
| sequence_expr |=> property_expr
| if ( expression_or_dist ) property_expr [ else property_expr
| case ( expression_or_dist ) property_case_item { property_case_item } endcase
| その他いろいろあるが省略
property_case_item ::=
expression_or_dist { , experssion_or_dist } :
property_expr;
| default [ : ] property_expr ;
module_or_generate_item_declaration ::=
...
| default disable iff expression_or_dist ;