IEE1800-2017では16.12 Declareing propertiesという節にproperty宣言について書かれています。
書かれていることを抜粋すると
- propertyはデザインのbehaviorを定義するもの。
- 名前付きのpropertyはassumption, obligation, coverageの仕様として使われる。
- obligationといっているのが検証対象がこういう動きをしなければならいという仕様のことで、あとでassert宣言されるものを指していると思います。
- 検証するためのbehaviorとして使うにはassert, assume, cover宣言が必要。
名前付きのpropertyは次のような箇所で宣言する
- module
- interface
- program
- clocking block
- package
- compilation-unit scope
- generate block
- checker
とあります。
この中でchecker blockは1800-2012で追加されたblockだと思います。ツールが対応しているかどうか確かめるためサンプルコードを書いたことはありますが実務では使ったことがありません。checker blockを活用している人いますか？
class内には書けないので、UVMのdriver classとかmonitor class内に書いて使うことはできません。interface blockにinterfaceのチェックをするproertyを書くという使い方になります。
property宣言の形式は下記のようになります。
property propertyの名前 [([propertyのポートリスト)];
{アサーション変数}
[clockingイベント][disable iff (disableの条件式)]
property本体 [;]
endproperty
property本体と書いてあるのはIEEE1800のドキュメントのBNFで書かれた仕様ではproperty_specと書かれているものですが、適当に意味が分かるような言葉に置き換えています。
property本体 [;]
となっていてproperty_specの後にセミコロンをつけてもつけなくてもよくなったんですね。以前の規格ではセミコロンが必ず必要だったような気がしますが手元に仕様書がないので確認できない。
property p_sample;
@(posedge clk) disable iff(!rst_n)
start |-> ##1 ack
endproperty
上のpropertの意味は次のようになります
propertyの名前はp_sample。
clkの立ち上がりでproperty本体の式を評価する。
rst_nがLならチェックをキャンセル。
startがHなら次のサイクルでackがH。