Loading article…
プロパティ仕様言語（PSL）は、線形時相論理を拡張した時相論理であり、表現の容易性と表現力の向上を両立させるために、さまざまな演算子を備えています。PSLは正規表現と構文糖衣を多用します。ハードウェア設計および検証業界で広く使用されており、モデル検査などの形式検証ツールや 論理シミュレーションツールを用いて、特定のPSL式が特定の設計において成り立つかどうかを証明または反証します。
PSLは当初、ハードウェア設計に関する特性や主張を記述するためにAccellera社によって開発されました。2004年9月以降、 IEEE 1850ワーキンググループにおいて言語の標準化が進められ、2005年9月には、特性記述言語（PSL）に関するIEEE 1850規格が発表されました。
PSLは、あるシナリオが現在発生した場合、別のシナリオが後日発生するべきであることを表現できます。例えば、「 要求は必ず最終的に承認されるべきである」という特性は、PSL式で表現できます。
常に（要求→最終的には許可） 「 ACK信号が直後に続くすべての要求は、完全なデータ転送に続くべきである 。ここで、完全なデータ転送とは、信号startで始まり、信号endで終わるシーケンスであり、その間、ビジー状態が保持される」という特性は、PSL式で表現できる。
(true[*]; req; ack) |=> (start; busy[*]; end) この式を満たす軌跡が右の図に示されている。
(true[*]; req; ack) |=> (start; busy[*]; end) PSL の時間演算子は、大まかにLTL スタイルの演算子と正規表現スタイルの演算子に分類できます。多くの PSL 演算子には、感嘆符の接尾辞 ( ! ) で示される強いバージョンと弱いバージョンの 2 つのバージョンがあります。強いバージョンは、将来何かが成立することを要求しますが、弱いバージョンはそうではありません。アンダースコアの接尾辞( _ ) は、包括的要件と非包括的要件を区別するために使用されます。_a と_eの接尾辞は、普遍的(すべて) 要件と存在的(存在する) 要件を示すために使用されます。正確な時間ウィンドウは[n]で、柔軟な時間ウィンドウは[m..n]で示されます。
最も一般的に使用される PSL 演算子は、「接尾辞含意」演算子 (「トリガー」演算子とも呼ばれる) で、|=>で表されます。その左オペランドは PSL 正規表現であり、右オペランドは任意の PSL 式 (LTL スタイルでも正規表現スタイルでも可) です。r |=> pの意味は、i までの時間点のシーケンスが正規表現 r に一致するようなすべての時間点 i において、i+1 からのパスがプロパティ p を満たす必要があるということです。これは右の図に例示されています。
PSL の正規表現には、連結 ( ; )、クリーネ閉包 ( * )、和集合 ( | ) の共通演算子に加え、融合 ( : )、交差 ( && )、およびより弱いバージョン ( & ) の演算子、連続カウント[*n]および非連続カウント[=n]や[->n]などの多くのバリエーションがあります。
トリガー演算子にはいくつかの種類があり、以下の表に示されています。
ここで、sとtはPSL正規表現であり、pはPSL式である。
連結、融合、和集合、積集合、およびそれらの派生演算子を以下の表に示します。
ここで、sとtはPSLの正規表現です。
連続繰り返し演算に使用する演算子を以下の表に示します。
ここでsはPSL正規表現です。
連続しない繰り返し処理のための演算子は、以下の表に示されています。
ここで、bは任意のPSLブール式です。
以下は、LTL スタイルの PSL オペレーターの例です。
ここで、pとqは任意のPSL式である。
マルチクロック設計の場合や、より高いレベルの抽象化が必要な場合など、次の時点の定義を変更することが望ましい場合があります。この目的のために、サンプリング演算子（クロック演算子 とも呼ばれる）@が使用されます。右の図に示すように、p が PSL 式、c が PSL ブール式である場合、式p @ c は、そのパス上のp がcが成り立つ サイクルに投影されたときに、その パス上で成り立ちます 。
最初の特性は、「 ACK信号が直後に続く すべての要求は、完全なデータ転送 に続くべきであり 、完全なデータ転送とは、信号開始から信号終了まで続くシーケンスであり、そのシーケンスには 少なくとも8回分のデータが含まれるべきである」と規定している。
(true[*]; req; ack) |=> (start; data[=8]; end) しかし、場合によっては、上記の信号がclkがハイのサイクルで発生する場合のみを考慮したい場合があります。これは、式が
((true[*]; req; ack) |=> (start; data[*3]; end)) @ clk データ[*3]を使用し 、[*n]は連続した繰り返しです。一致するトレースには、データが保持される非連続な時間点が3つありますが、 clkが保持される時間点のみを考慮すると、データが保持される時間点が連続します。
ネストされた @ を含む数式の意味はやや複雑です。興味のある読者は [2] を参照してください。
PSLには、切り詰められたパス（計算のプレフィックスに対応する可能性のある有限パス）を処理するための演算子がいくつかあります。切り詰められたパスは、境界モデル検査、リセット、その他多くのシナリオで発生します。中止演算子は、パスが切り詰められた場合に、どのような事態が発生するかを指定します。これらの演算子は、[1]で提案されている切り詰められたパスの意味論に基づいています。
ここで、pは任意のPSL式であり、bは任意のPSLブール式である。
PSLは時相論理LTLを包含し、その表現力をオメガ正規言語の表現力まで拡張します。アスタリスクを含まないω正規表現の表現力を持つLTLと比較して、表現力が向上したのは、トリガー演算子とも呼ばれる接尾辞含意（「|->」と表記）によるものです。正規表現rと時相論理式fを持つ式r |-> fは、計算wにおいて、 rに一致するwの接頭辞がfを満たす継続を持つ場合に成立します。PSLのその他の非LTL演算子には、マルチクロック設計を指定するための@演算子、ハードウェアリセットを処理するためのアボート演算子、簡潔さのためのローカル変数などがあります。
PSLは、ブール層、時間層、モデリング層、検証層の4つの層で定義されます。
プロパティ仕様言語は、以下のような複数の電子システム設計言語（HDL）で使用できます。
PSLを上記のいずれかのHDLと組み合わせて使用する場合、そのブール層はそれぞれのHDLの演算子を使用します。