高位設計手法にアサーションを適用：アスペクト指向プログラミングの活用で（1/4 ページ）

昨今の回路設計では、アサーションを利用した機能検証手法が使われ出している。しかし、従来のアサーション記述言語はVHDLやVerilog HDLをターゲットとしていたため、SystemCなどを用いた高位設計には不向きであった。本稿では、ソフトウエア開発の分野で使われ始めているアスペクト指向プログラミング（AOP）を用いて、高位設計においてもアサーションを利用した検証を可能にする技術を紹介する。

[遠藤 侑介 （東芝 研究開発センター），EDN]

高位設計手法の課題

　デジタル回路の高位設計手法が脚光を浴びている。これはSystemCやSpecCなどのように、VHDLやVerilog HDLよりも高位のプログラミング言語を用いて回路を記述するというものである。高位設計手法では、VHDLやVerilog HDLよりも簡潔に回路を記述することができる。また、シミュレーションも高速に行えるようになる。その結果として、開発期間の短縮を図ることが可能になる。

　しかし、現状の高位設計手法には1つの課題がある。それは、既存の技術を用いたのでは、アサーションベース検証を適用するのが難しいということだ。

　アサーションベース検証は、VHDLやVerilog HDLによってハードウエアの機能を記述したプログラム（以下、設計記述）が、アサーション（表明）として記述した制約を満たしているか否かを検証する手法である。アサーションとは、回路の設計記述の性質や設計記述が満たすべき制約をアサーション記述言語によって条件式として記述したものだ。アサーションベース検証を担う処理系はアサーションと設計記述を読み込み、設計記述の動的解析または静的解析によってアサーションに書かれた条件が満たされているかどうかを検証する。アサーションは設計記述に対して、設計記述とは異なる側面から抽象的/部分的に記述することが可能なので、設計記述を複数の観点から検証することができる。

　ここで問題になるのが、高位設計手法に既存のアサーション記述言語を直接適用するのが困難であるということだ。従来のアサーション記述言語は、RTL（Register Transfer Level）による記述に適用することを前提としている。そのため、RTLによる記述で発生する低位のイベントしか扱うことができない。ところが、高位設計手法では、関数呼び出しのように、RTLの記述には存在しない高位のイベントが発生し得る。その対策として、高位のイベントを低位のイベントとして観測できるようにするためのコードを各プログラムモジュールに記述する方法が考えられるが、後述する理由からこのような手法は決して望ましいものだとは言えない。

　このような課題に注目し、筆者らは高位設計手法にアサーションを適用する方法を検討している。以下では、まず従来のアサーション記述言語がどのようなものであるのかを簡単に説明する。続いて、回路の設計記述の例を用い、従来のアサーションベース検証技術をそのまま高位設計に適用するのがなぜ難しいのかを具体的に説明する。その上で、この課題を解決するために筆者らが取り入れようとしている新たな技術や、その活用方法などを詳細に説明していくことにする。

既存のアサーション記述言語

表1　線形時相論理のオペレータとPSLの構文の対応　

　アサーション記述言語は、設計記述に対するアサーションを記述するための言語である。多くのアサーション記述言語は時相論理や拡張正規表現などをベースとしており、これらを用いて設計記述内のイベントが発生すべき順序について記述する。

　代表的な時相論理に、線形時相論理（LTL：Linear Temporal Logic）がある。これは既存の論理体系に離散的な時系列の概念を導入したものであり、表1に示す4つのオペレータが追加されている。以下に示すのは、時相論理式の一例である。

G （p→F q）

　この論理式は「ある時点でpが成立したら、その後いつか必ずqが成立する」という性質を表している。

　回路設計で実際に用いられる、LTLをベースとしたアサーション記述言語としては、プロパティ記述言語（PSL：Property Specification Language）やSystemVerilog Assertions（SVA）がある^＊1）。本稿では、アサーション記述言語としてPSLを例にとって解説を進めることにする。

　PSLを用いれば、回路記述の性質や制約を記述することができる。PSLは標準化団体のAccelleraとIEEEによって標準化されており、VHDL、Verilog HDL、SystemVerilog、SystemCという複数のハードウエア記述言語に対して使用可能である。なお、それぞれにおいて自然な記述が行えるように、PSLの派生バージョン（フレーバ）が用意されている^＊2）。

　LTLの各オペレータとPSLの構文は、表1のように対応している。

リスト1　PSLのVerilogフレーバによる記述例　

　リスト1に示すのは、PSLのVerilogフレーバによる記述例である。このコードでは、あるクロックのタイミングで信号線reqが論理レベルの1（真）になっていたら、必ず（always）、いつか（eventually!）、信号線ackが1になるという性質を記述している。このように、従来のPSLでは、信号線の値がある条件を満たしているかどうかによってイベントを表現し、そのイベント間の時系列上の依存関係を示すことでアサーションを記述する。

　PSLの言語設計は、以下の4層から成る。

・ブーリアン層：ハードウエア記述言語の式によってイベントや条件を表現する。リスト1の例ではreq==1とack==1がこれに当たる

・テンポラル層：ブーリアン層の記述がどのような時間関係で成立するのかを表現する。リスト1の例ではalwaysやeventually!がこれに当たる

・検証層：テンポラル層の記述をどのように使うかを指定する（成立するかどうかを検証する、成立する頻度を計る、など）。リスト1の例ではassertがこれに当たる

・モデリング層：検証用の補助回路を記述したり、テストベンチを記述したりする。リスト1の例には存在しない

脚注

※1…PSLは、LTLだけでなく、オプションとして計算木論理（CTL：Computational Tree Logic）をベースとしたアサーションも提供している。これについては、本稿では触れないこととする。

※2…ただし、SystemCのフレーバはほかのフレーバをそのまま移植した設計となっており、後述する高位のイベントに対するサポートは特に用意されていない。