アサーション・ベース検証（assertion-based verification）は機能検証手法の一つである。アサーションとは，検証対象の設計が満たすべき性質を指す。アサーション・ベース検証は，RTL（register transfer level）設計を対象にした論理シミュレーションで使われることが多い。
具体的には，論理シミュレーション中に，検証対象とアサーションの関係を調べて，アサーションが満たされているかどうかチェックする。こうすることで，設計記述の観測性が上がり，設計のバグを発見しやすくなる。また，バグの原因を解析しやすくするという効果もある（図1）。
【図１ アサーションを使った検証の効果】出典は富士通研究所。 （画像のクリックで拡大）
IEEE標準のアサーション記述言語
アサーション1)は，設計した回路で期待されている動作や禁止されている動作などを書いた文である。通常，その内容は，曖昧性がないようにハードウェア記述言語（Verilog HDLやVHDL，SystemCなど）やアサーション記述言語で記述する。
アサーションとして記述する動作は，「安全性タイプ」と「生存性タイプ」の二つに分類できる。安全性タイプの動作とは，「規定された値以外を絶対に出さないこと」である。一方，生存性タイプの動作とは，「規定された値をいつかは出力すること」である。
アサーション言語は，両タイプの動作を効率的に記述するための仕組みを備えている。アサーション言語としては，「e言語」，「PSL（Property Specification Language），「SVA（SystemVerilog Assertion）」などがあり，いずれも2005年から2006年にかけてIEEEで標準化された。
これらの言語は，通常の命題論理に時間の概念を加えた「時相論理」を基盤としており，ほぼ同様の記述能力がある。なお記述したアサーションは設計記述の中に入れ込んだり，まとめて別のファイルにしたりする（使う言語やツールで異なる）。
「どう書くか」は重要でない
アサーション・ベース検証で重要なことは，言語を用いてアサーションを「どう」書くかではない。適切な検証のために，「どんな」アサーションを「どこに」，「どれだけ」入れれば良いかを考えることである。これらは，曖昧性の高い設計「意図」に深く関係しているため，現時点で明確な指針や尺度は提唱されていないが，いくつかの有効な事例が報告されている。
例えば，「どこに」入れるかに関して，「検証ホット・スポット」という考え方がある2)。検証ホット・スポットとは，設計誤りを最も犯しやすく，最も検証時間を費やす部分を言う。文献2)では，複数の設計例から抽出された5種類のホット・スポットが挙げられている（図2）。全体の検証時間の80%がホット・スポットの検証に充てられているという。
【図2 検証のホット・スポット】2) （画像のクリックで拡大）
五つのうち，非同期クロックを除く4種類のホット・スポットは，アサーションの効果が高い。ほぼあらゆる設計に共通に現れる4種のホット・スポットに対して集中的にアサーションを投入することで，検証効率の大幅な向上が期待できる。
このほかに，アサーションを入れるべき場所としては，設計者がコメントを入れたい/入れたくなる場所，あるいはアサーション密度（後述）の低いところを挙げられる。
逆に，アサーションを入れるべきでないところには，すでに十分検証されたブロックの内部，グリッチ検出などの論理以外の動作，などがある。アサーションを挿入することで，シミュレーション速度は多少なりとも低下するため，無駄なアサーションや，必要以上にイベントをとらえるアサーションを極力排除することが重要である。これらはガイドラインとして文献3)に多くの事例が紹介されている。
アサーションの「見本」を活用する
アサーション言語は，理解が難しい時相論理を基盤としているため，記述誤りが発生しやすく，デバグも難しい。このため，再利用可能なアサーション群が，「パターン」や「ソリューション」と呼ばれる形で整備されている。実際の設計に合わせてこれらを適用することで，比較的簡単に必要なアサーションを用意できる。
ワンホット・コードのチェックや信号の依存関係チェックのように設計に広く使われるアサーションをパターン化したものは「アサーション・パターン」と呼ばれる。
一方，設計でよく使われる回路ブロックに対して入れるべきアサーションをセットにしたもの（ソリューション）が「クックブック」である。クックブックの対象となるブロックはホット・スポットと直接対応している場合が多く，導入効果が高い。文献1)ではFIFOやアービタなど15種類のブロックに対するソリューションが示されている。
適切な量を投入
ホット・スポットに対して，パターンやクックブックを適用すれば，ほぼ十分なアサーションが設計記述に挿入されていると考えてよい。アサーションの充足度を定量的に表す「アサーション密度」と呼ぶ指標がある。
これはRTLの設計コード1行あたりに挿入されたアサーションの数だが，RTLコード全体に対するアサーション密度はあまり意味がない。コードの中のホット・スポットで十分なアサーション密度があるか，同密度が極端に低い部分がないかを判別するために用いると，効果的である。
アサーションの入れ時
アサーションをいつ，誰が入れるかは，アサーションの性質で変わる。LSI全体に関わるアサーションは機能仕様作成後，設計者とは別の検証専任者が記述する場合が多い。
一方，RTL設計に組み込まれるアサーションは，RTL記述中ないし直後に設計者自身が作成する場合が多い。どちらのアサーションも，挿入後に「どこに，何を，どれだけ」の観点でレビューを受ける必要がある。
フォーマル検証との親和性が高い
アサーションの記述方式は，元々フォーマル検証の一つの「プロパティ（モデル）・チェッキング」のプロパティに倣っている。このため，アサーション・ベース検証はフォーマル検証と親和性が高い。多くの場合，アサーションは，そのままフォーマル検証でもチェックできる。
特にホット・スポット内のアサーションについては，影響範囲がそのモジュール内部にとどまることが多く，フォーマル検証が成功する可能性が高い。アサーションは論理シミュレーションによる検証でも，フォーマル検証でも記述を変えることなく適用できる点に大きなメリットがある。
参考文献
1) Foster, H., Krolnik, A., Lacey, D., 『アサーションベース設計 原書2版』，丸善，2004年.
2) Yeung, P., Gupta, V., “Five Hot Spots for Assertion-Based Verification”, DVCon, 2005.
3) Burgeron, J., Cerny, E., Hunter, A., and, Nightingale, A., 『ベリフィケーション・メソドロジ・マニュアル』, CQ出版社, 2006.
4) Glasser, M., Rose, A., Fitzpatrick, T., Rich, D., Foster, H., The Verification Cookbook: Advanced Verification Methodology（AVM）, Mentor Graphics Corp, 2007.
5) Foster, H., Krolnik, A., Creating Assertion-Based IP, Springer, 2008.
