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

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

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

こんなアサーションは意味がない

　アサーションは、1つ記述するだけでも効果が期待できる。しかし、アサーションの適用個所や記述方法によっては、検証に貢献しないケースもある。ここでは、適用すべきでない個所、意味のないアサーションの例を紹介する。

アサーションを適切な個所に挿入することは、費用対効果を考える上で非常に重要である。次のような目的で記述したアサーションについて考えてみよう。

（1）常に動作しているクロックをモニターするためのアサーション

（2）RTLコードをコピー＆ペーストして作るようなアサーション。例えば、インクリメントするカウンタ値の変化をモニターするためのものなど

（3）基本機能として動作が自明なコンポーネントをモニターするためのアサーション。例えば、マルチプレクサや、標準的なレジスタ（D入力をQ出力するだけのレジスタ）をチェックするためのもの

リスト4　RTLコードの内容をそのまま記述したアサーション（その1）　

（4）非同期のタイミングで発生するグリッチを検出するためのアサーション

　（1）〜（3）のような個所は、RTLのコードを見ただけで動作を理解できるので、アサーションを適用する効果は少ない。一方、（4）のような動作は、同期化されたアサーションで検出することはできない。無理に検出しようとすれば、極めて高いコストが発生する。このような個所には、アサーションを適用すべきではない。実際、アサーションを利用したダイナミック検証で、オーバーヘッドの最も大きな元凶になっているのは、目的が不明で費用対効果の低いアサーションを乱用することだ。アサーションは、RTLコードを見ただけでは、その振る舞いが判断できない個所に適用すべきである。本当に意味のある検証であるなら、シミュレーションにおいて多少の負荷が発生することは問題ではない。

リスト5　RTLコードの内容をそのまま記述したアサーション（その2）　

　アサーションを記述する際に、基となるのは原則として仕様であり、RTLのコードではない。RTLのコードをそのままコピー＆ペーストしたようなアサーションでは、RTLのコードに潜むバグまでコピーしてしまう恐れがある（リスト4、5）。RTLコードを基にしたアサーションは、RTLコードの振る舞いをそのまま検証するだけとなるため、ほとんどのケースでフェイルになることはない。バグの発見は期待できず、ただ単にシミュレーションを遅くするだけの無意味なものだ。この点には、注意が必要である。

リスト6　過剰に限定された条件をチェックするアサーション　

　また、過剰に限定された条件のみをチェックするためのアサーションもあまり意味がない。例えば、リスト6のアサーションは、極めて限定された条件のシーケンスを通ったときのみに発生するdone信号しかチェックできない。この条件に当てはまらない状況はチェックできないので、このやり方であらゆる条件を検証しようとすると、アサーションの数が膨れ上がってしまう。そうすると、シミュレーション上の負荷が大幅に増大してしまう。

　加えて、過剰に限定された条件のみをチェックするためのアサーションは、往々にして記述が複雑である。そのため、その記述自体のデバッグが困難な作業になってしまうことがある。結果として、アサーション自体のバグによる擬似エラーが発生したり、バグを見落としてしまったりといったことが引き起こされる可能性がある。

リスト7　包括的なアサーションへの変更　

　一方、条件の面で包括的なアサーションを記述することにより、幅広いシナリオをチェックすることができ、予想もしないバグを発見できる可能性が高くなる。包括的なアサーションを記述するには、何を検証するのかという理解が必要であり、そのためには仕様を十分に理解しておかなければならない。done信号はどのコマンドでも必ず発生する、サイクル数は必ず1サイクル以上であるといった仕様を正確に理解しておくことが、包括的なアサーションを記述するためのコツである（リスト7）。余計な信号やサイクル数の限定を条件とすることは、検証のチャンスを逃すだけでなく、時としてシミュレーションに余計なオーバーヘッドを生じさせる可能性がある。

　ただし、ダイナミック検証はテストベンチに依存するため、実際には包括的なアサーションを記述しただけでは、予期できないバグを発見できる可能性は低い。それに対し、スタティック検証であるフォーマル解析であれば、テストベンチを必要とせず、包括的なアサーションの効果が非常に高くなる。ダイナミック検証で予期しないバグを発見しなければならない場合には、予期せぬバグを引き起こすテストシナリオを発生させるランダム検証が最適である。ランダム検証の環境では期待値チェックは困難だが、その際に行う制御系の期待値チェックにはアサーションの利用が適している。