アサーション活用の手引き：その基本から、記述ノウハウ、フォーマル解析への展開まで（1/5 ページ）

ICの高機能化が進むに従い、その機能を検証する作業が非常に大きな課題となってきている。この課題を解決するものとして期待され、現在、着実に普及しつつあるのが、アサーションベース検証（ABV）である。本稿では、まずこのABVの基本について説明する。続いて、アサーションを記述する上での注意点などを紹介する。さらに、アサーションを利用したもう1つの検証手法であるフォーマル解析についても解説を加える。

[矢ヶ部 常義（日本ケイデンス・デザイン・システムズ），EDN]

「検証」にかかる負荷

　ICの集積度は、ムーアの法則に基づき、現在でも18カ月で2倍になると言われている。集積度の増加に伴い、数年前は複数のチップで実現していたいくつかの機能が、現在では1チップで実現できるようになっている。

　しかし、1つのチップに複数の機能が混在すると、動作の複雑さが著しく増加する。そして、設計者は、各機能が正しく動作することはもちろん、それら複数の機能が互いに影響し合うことも考慮した上で正しく動作することなど、すべての検証（機能検証）を限られた開発期間内に行わなければならない。一般に、開発期間の約7〜8割が検証に費やされていると言われている。そのため、検証の遅れは製品の市場投入の遅れに直結する。複雑な機能を検証し、なおかつ検証時間を短縮するには、従来の手法から一歩進んだ新たなチャレンジが必要である。

リスト1　HDLで表現したアサーション　

リスト2　PSLで記述したアサーション　アサーション言語を使って、リスト1と同じ内容を記述している。

　 そうした新たな手法の1つに、「アサーションベース検証（以下、ABV）」がある。アサーションという考え方は決して新しいものではなく、シミュレーションにおいてアサーションモニターやウォッチドッグという名で古くから使われていた（リスト1）。現在では、PSL（Property Specification Language）とSystem Verilogアサーション（SVA）の2つが、それぞれIEEE 1364、IEEE P1800として標準化されたアサーション言語となった（リスト2）。それにより、多くのツールでアサーション言語のサポートが進んだ。また、波形ビューワにもアサーションの結果をデバッグするための機能が多数、搭載されてきている。

従来の検証の問題点

　従来の検証は、多くの場合、外部入力端子と外部出力端子の波形を目視確認することで行われていた。あるいは、テストベンチ内に、検証のために結果を比較するような構造を追加するという方法がとられることもある。こうした方法で、仕様どおりの振る舞いであるか否かを確認していたのである。

　こうした方法では、検証の対象となるものが外部端子に限定される。そのため、設計の内部で発生しているバグの影響が外部端子まで伝播する条件でテストが行われなければ、バグの存在を見逃す可能性が非常に高かった。また、バグの影響が外部端子まで伝播したとしても、内部のどの部分で、どの時刻にバグの影響が現われたのかを判断するのが非常に困難であった。バグの発生個所を特定するために、外部端子から設計の内部へとバックトレースを行いながらデバッグを進める必要があり、非常に多くの工数を費やす必要があったのだ。さらに、外部端子だけの確認では、設計全体のどの程度までテストベンチの影響が及んだのかを確認する方法がなく、十分に設計を検証できるテストシナリオが用意されていたのかどうかが判断できない。

　このように、従来の検証では、基本的に外部端子の振る舞いが適切でない場合にしか内部を確認しない。そのため、この手法は「ブラックボックス検証」と呼ばれている。規模が小さく、搭載している機能の数が少ない一昔前の設計であれば、この手法でも十分であった。しかし、現在の大規模/複雑化した設計では、この手法による対応は難しくなっているのである。

アサーションでできること

　従来の検証手法とは異なり、ABVでは、外部端子に加え、設計内部のどの部分でも容易に検証ポイントとすることができる。アービトレーション（調停）の公平性、FIFO（First In, First Out）のオーバーフロー/アンダーフローなど、検証におけるホットスポットと呼ばれている個所や、設計者がコメントで設計意図を記述していたような個所など、実装レベルで注意を要するポイントにアサーションを挿入することができる。もちろん、インターフェースの仕様、エンドツーエンドの振る舞いの仕様として定義されている禁止動作や起こるべき動作についても、アサーションを適用可能である。

　設計内部で用いられているFIFOを例にとって考えてみよう。FIFOは、設計のある機能を構成するための1つの部品である。この1つの部品が意図したとおりに動作しなければ、設計全体の動作に影響が及ぶケースは少なくない。そのため、この部品が正確に動作することは非常に重要であり、その動作を保証するためにアサーションを適用する。「FIFOがオーバーフロー/アンダーフローしない」ということは、設計全体の仕様には記載されない。しかし、これが満足できなければ、当然、FIFOとしての動作が保証できないし、設計全体としての機能も保証されない。それ故、各部品を十分に検証することは非常に重要である。また、機能全体を検証する中で各部品の検証も行える。

　設計者の中には、「アサーションの挿入個所がわからない」という方がいる。しかし、難しく構える必要などまったくない。アサーションを用いて検証ポイントを設計内部にも設定することで、外部端子に伝播しない内部のバグをピンポイントで発見することができる。言い換えれば、ブラックボックス検証では検出が困難だったバグを発見することが可能になる。加えて、バグを特定するのに要する時間を大幅に短縮することができる。実際、デバッグ時間を約50％削減できたとの事例報告もある。

図1　アサーションは各検証フェーズで利用できる　

　また、アサーションはバグの発見に加え、設計全体の検証カバレッジの測定にも利用できる。その場合、アサーションによるチェックが実際に行われるように条件を作ることが重要である。前述したFIFOの例で、オーバーフローをチェックするアサーションを挿入していたとしても、FIFOがフルになるようなシーケンスに到達する検証が行えていないと、オーバーフローが起きない正しい設計を行えたのか、それともたまたまオーバーフローするような状況をテストで作れなかったのかを区別することができず、検証としての意味が薄くなるからだ。カバレッジを測定することにより、テストが足りない個所を認識することができる。そのため、この測定は、検証の進捗を測る上で有用である。

　上述したような形でアサーションを利用することにより、設計の内部まで検証を行うことができる。そのため、この手法は従来のブラックボックス検証に対して、「ホワイトボックス検証」と呼ばれている。

　さらに、アサーションは、通常の論理シミュレーション時に行うダイナミック検証だけでなく、フォーマル（形式手法）解析や、ハードウエアアクセラレーション/エミュレーションのフェーズでも利用できる。すなわち、早期に行われるブロックレベルの検証の段階からチップ全体の検証の段階まで、一貫して環境の再利用を図ることが可能である（図1）。