verilog : SVA の property 記述概要

目的:

SVA の property 記述について 理解した内容を 記す

property 記述 :

検証の動作を定義する。
property 記述のみでは アサーションを生成できず、 assertion 記述が必用。

記述方法:

プロパティ表現:

プロパティ表現で 検証の動作内容を定義する。

インプリケーション演算子を使用する場合。

前提条件が 成立した後、 1 クロック後に 帰結部 を 評価する。
上の例では、 X が 立ち上がった後、1クロック後に Y が 立ち下がる事 を確認する。
シーケンスについては、下記参照。
インプリケーション演算子 には次の 2種類がある。

• オーバーラップ・インプリケーション演算子  ( |-> )
  　　前提部終了と帰結部開始が同じクロック

• ノン・オーバーラップ・インプリケーション演算子 ( |=> )
  　　前提部終了の 1クロック後に帰結部開始。 |-> ##1  と同じになる。

プロパティ否定演算子を使用する場合。

クロック毎に x と y が 等しくない事を確認する。

演算子を使用しない場合。

クロック毎に x と y が 同じであることを確認する。

その他、プロパティ演算子 として and, or, if else を使用して複数のプロパティ表現を組み合わせる事が可能。

シーケンス:

シーケンスは、信号の一連の動作を表す。
例えは、 信号 A, B, C が 1クロック毎に 立ち上がる場合は、
　 a ##1 b ##1 c
の様に記述する。
1つの信号が立ち上がるだけでも シーケンス である。
　 a
シーケンスは、シーケンス記述で 名前を付けて プロパティ記述の中で使用することができる。

シーケンス演算子 の 詳細は こちら を参照。

システム関数:

システム関数として、以下の関数があり、シーケンス記述等で使用できる。
$rose( 信号 )
　信号の最下位ビットが '1' に変化した時に 真
$fell( 信号 )
　信号の最下位ビットが '0' に変化した時に 真
$stable( 信号 )
　信号が 1サイクル前から変化しなければ 真
$past( 信号 , n )
　信号のnサイクル前の値,  nが省略された場合は n=1
$onehot( 信号 )
　信号の'H' のビット数が 1 の時に 真
$onehot0( 信号 )
　信号の'H' のビット数が 1 又は 0 の時に 真
$isunknown(信号)
　信号に 'x' や 'z' が含まれる場合に 真
$countones(信号)
　信号の'H' のビット数