アサーション・ベース検証による
観測性の向上と潜在不具合の早期発見

アサーション・ベース検証とは

RTL設計において論理シミュレーションの結果確認はどのように実施していますか?
画像処理回路であれば実際の画像を流して結果を確認したり、独自の結果判定プログラムを用意しチェックしたり等、DUTを効率良く検証する手法を導入されていることでしょう。
しかし波形やログを目視確認する人手作業も残っているのではないでしょうか?
アサーション・ベース検証とは、そのような目視確認作業の自動化が可能となる検証手法です。
目視確認ではどうしても確認漏れや確認ミスを生じてしましますが、アサーション・ベース検証を用いることで確認漏れやミスも防止できます。
また回路内部にアサーションを埋め込むことにより、出力端子に反映されない不具合現象についても検出可能となり、 観測性の向上による潜在不具合の早期発見を期待できます。


アサーションを回路内部にチェッカーとして適用する概念図

アサーション・ベース検証を行うための具体的な準備は、アサーションのための専用言語である SVA(SystemVerilog Assertion)やPSL(Property Specification Language)を用いて、検証者がチェックしたい動作を定義することです。
そのアサーション記述と一緒に通常の論理シミュレーションを実行することで、定義した動作を満たさない状況が発生した場合には論理シミュレーション時にFAILとなります。
アサーションは専用言語であるために、動作仕様をシンプルに表現することができ、複雑な動作仕様であっても容易に定義することが可能です。


期待する動作(1) と これをチェックするためのSVA記述例 (2) の簡単な例

検証者がアサーション言語により動作仕様を0から記述する方法の他に、予め用意されているアサーションライブラリを使用する方法もあります。
標準的なアサーションライブラリである OVL(Open Verification Library)や 各EDAベンダーが用意しているアサーションライブラリ (Mentorの場合にはQVL(Questa Verification Library)) を利用することが可能です。
これらを用いることで検証者がアサーション記述を作成する手間を削減でき、また検証の信頼性を向上させることが可能です。

導入効果

アサーション・ベース検証を導入した場合の代表的な効果を3つ紹介します。

  1. 検証結果確認の自動化により、検証時間の短縮・検証結果確認の漏れを防止
  2. 外部調達IPや他の設計者とのインターフェース仕様を明確化し、仕様が曖昧であることに起因する不具合を未然に予防
  3. 再利用による検証の効率化

1. 検証結果確認の自動化
今まで目視で確認していた論理シミュレーションでの動作を、漏れなくミスなくチェック可能です。
検証では多くのテストパタンを流すことになりますが、その全てのパタンの全ての期間において、定義した動作仕様を違反しないかを自動で漏れなくチェックします。

2. 外部調達IPや他の設計者とのインターフェース仕様を明確化し、仕様が曖昧であることに起因する不具合を未然に予防
アサーションは動作仕様を明確に記述する必要があります。これによりHDL設計とは別の視点から仕様に曖昧な部分がないかを洗い出すことが可能です。曖昧な仕様は不具合を発生させる危険性を孕んでいます。その洗い出しに有効です。

3. 再利用による検証の効率化
一度用意したアサーション記述は、資産として流用することが可能です。設計したRTL回路やインターフェースを別の製品へ展開することは多々ありますが、その場合にはアサーション記述も流用利用することにより、検証の効率化が図れます。

運用方法の例

回路上のどの動作についてアサーションを用意するべきか、多くの方が最初は迷われます。回路の動作仕様を全てアサーション記述化することも可能ですが、大変非効率であり現実的ではありません。適切な箇所に絞って適用することが、効果をあげる秘訣です。
具体例を挙げます。

  • AXI など一般的なバスを搭載する場合に、そのインターフェースプロトコルをアサーション言語で用意する
    バスには複数の設計者のブロックが接続されることでしょう。
    各設計者がプロトコルを守って正しい転送を行えているか、一様に検証することが可能となります。
  • 外部調達IPを使用する場合に、そのインターフェース仕様についてアサーション記述を用意する
    外部調達IPに対して仕様どおりの出力であるか、またIPへ違反した入力をしていないかを検証することが可能です。
  • 不具合を修正した際に、不具合動作が発生しないことをアサーション記述で定義する
    不具合が正しく修正されたことを、第三者視点で自動チェックすることが可能です。同じ不具合を再発させないチェッカとなります。

Mentor製品を用いたアサーション検証 デバッグ手法

Mentor ModelSim/Questaには、アサーション検証に関するデバッグ・解析・マネジメント機能を搭載しています。 これらを用いてを効率よくデバッグすることが可能です。

(a) シミュレーション時の各種機能
 » アサーションのコントロール機能
 ・アサーションのPASS/FAIL 機能の ON/OFF
 ・アサーションFAIL時のシミュレーション動作(継続、中断、停止 等)
 ・アサーションFAIL時のメッセージ表示 ON/OFF
 など
 » 波形Viewer上にアサーションの評価開始、結果PASS/FAILを表示

(b) アサーション カバレッジの取得
シミュレーションを実行した結果のアサーションPASS/FAIL判定の回数を取得可能

(c) ATV (Assertion Thread Viewer) による アサーションの判定状況解析
複雑な動作仕様を記述したアサーションは、そのPASS/FAIL判定のために複数の状態事象が発生する可能性があります。
各状態事象で理論値がTRUE/FALSE がどうなって結果的にPASS/FAILを発生させたかを時系列的にタイミングチャートイメージで表示します。

まとめ

アサーションとは一種のチェッカのようなものであり、論理検証におけるシミュレーション結果の確認を自動化し、検証結果確認の効率化を図ることが可能です。
アサーションを利用するには、
  ・アサーション用言語である SVA、PSL を利用する
  ・アサーション用ライブラリである OLV、(Mentor提供の)QVL を利用する
という方法があります。

代表的な導入効果として以下があります。
1. 検証結果確認の自動化により、検証時間の短縮・検証結果確認の漏れを防止
2. 外部調達IPや他の設計者とのインターフェース仕様を明確化し、仕様が曖昧であることに起因する不具合を未然に予防
3. 再利用による検証の効率化

Mentor ModelSim/Questa を用いることでアサーション検証が実施でき、また効率よいデバッグが可能な様々な機能を搭載しています。

適切なアサーションを用意し、またMentor ModelSim/Questaを利用した効率よいデバッグ環境を利用することで、検証品質の向上を図れます。

ModelSim DE
QuestaSim

アサーションを用いた別の検証手法

アサーション記述は、シミュレーション時だけではなく、形式検証という手法でも利用可能です。 形式検証 ではテストベンチやテストパタンが不要であり、RTLとアサーションのみを用いて、定義した動作仕様を満たさない場合があるかどうかを検証することが可能です。

Questa Formal

関連ページ

SVA(SystemVerilog Assertion)の文法

 


お問い合わせ

資料請求・お問い合わせ