aldecでpslを試してみる。 - sawaragikunkun’s diary

アサーション技術の本丸はPSLでしょう。。
と言うことでaldecのRiviera-PROで試してみた。

簡単にPSLの解説。。
SVAやOVLより強力なアサーション用の記述言語で
verilogソースに入れる事も出来るし、別ファイルとすることも出来る。
物の本には数学的に正確であると書いてある。
「アサーションベース設計」p415.. 丸善
SVAやOVLは不正確なの？？この疑問はとりあえず放っておいて、
数学的に正確なPSLであればモデル検証も出来るぜ～～と言う事だそうです。
　　注）専用モデル検証toolを使いたくても下々の者では高価すぎで使えません。。汗）

由来はsynopsysがsugarというプロパティー言語をaccelleraに寄贈した事に始まり、これを元に
作ったプロパティー言語だとの事です。

とりあえず簡単なアサーションを書いてみた。。下記参照

// vunit psl_count4($root.top.counter_w.count4)
vunit psl_count4(count4) // count4 <- module name
{
	default clock = rose(clk) ;
	
	property count_up = always {(rst | !load) -> q} ;
	assert_count4_up : assert count_up ;
}

defualt clock ....でクロックのエッジを指定している、この場合立ち上がりエッジで状態を遷移する。

property..の所でリセットとカウント値のロード時以外は０でないを記述して
assert_cou....の所でfail時の検出を記述している。
　注）カウンターなんだからプロパティは”常に＋１”なのでこれを記述したかったが。。文法エラー頻発でやめました。。汗）

PSLのコンパイルはコマンドラインのオプションに-psl file_nameを付ける。

vlog ..... ounter_if.sv counter_tb.sv ..... -psl counter4.psl

コンパイルしてRiviera-PROを立ち上げたら
[View]->[Debug Windows]->[Assertions]->[Assertion window]を選択して
Assertion windowを出しておく。
PSL記述の中にあるcount_upはこのAssertion windowで見ることが出来ます。
もちろんwaveform windowでも見ることが出来る。

カウンターがfullになって更にカウントすると値が０になったところでfailが
出てるのが解るでしょう。
　→この場合、正しくないプロパティーなのでfailが出ている、failの出ている例として見てくれよ。

systemVerilog PSL aldec Riviera-PRO