株式会社PALTEK > 半導体事業 > 取扱メーカー > Siemens EDA/シーメンス EDA > アサーションベース検証とは

Siemens EDA/シーメンス EDA

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

【3/15開催＊10万ページビュー 記念特別無償開催＊】ModelSimウェビナー ～ 一連の操作を学ぶ入門編 ～

アサーションベース検証とは、
検証対象となるRTL設計の内部や⼊出⼒インタフェースに対し、仕様で定められている振舞いや、発⽣してはいけない振舞いを、複数信号の時相的な関係によって簡潔に表現したプロパティと検証ツールへのコマンドを組み合わせて記述し、RTLの振舞いとの⽐較によって検証する⼿法を指します。HDLシミュレーションやフォーマル検証がアサーションベース検証のツールの代表例です。VerilogやVHDLなど設計⾔語がIEEEで標準化されているように、アサーション⾔語もIEEE企画として標準化されています。
SVA ‒ SystemVerilog Assertions、PSL ‒ Property Specification Languageがその代表的な⾔語です。
2016年にワールドワイドで⾏われたWilson Research Groupの市場調査によれば、FPGAプロジェクトの47%においてアサーションが採⽤されており、その⼤部分はSVAを採⽤しています。

検証対象（Design Under Verification）にバグが混⼊している場合、テストパターンの役割は⼤きく2つに分けられます。1つめはバグを活性化させること、そして2つめはバグに起因する不正な振舞いを外部まで伝搬させることです。設計規模や複雑度が増すと、テストの制御性と観測性の維持が困難になります。

検証対象（Design Under Verification）にバグが混⼊している場合、テストパターンの役割は⼤きく2つに分けられます。1つめはバグを活性化させること、そして2つめはバグに起因する不正な振舞いを外部まで伝搬させることです。設計規模や複雑度が増すと、テストの制御性と観測性の維持が困難になります。

アサーション記述例

SystemVerilog Assertionsによるアサーション記述例を⾒てみます。対象はblock_Aとblock_Bのハンドシェーク部分です。アサーション記述はあくまでも仕様から起こすことが重要で、RTL実装の記述をベースにすると、同じ内容の異なる表現となってしまい、検証の意味がなくなってしまいます。

仕様：ハンドシェーク
reqが⽴ち上がったら1〜3サイクル以内にackが返されなくてはならない

仕様は⽇本語や英語のような⾃然⾔語で表現されますが、⾃然⾔語には曖昧さが含まれます。この例でも1〜3サイクルが、どのサイクルを起点とするかが明確ではありません。
アサーション記述にはこの曖昧さがありません。以下のSVA記述はreqの⽴ち上がりが検出されたサイクルを0サイクル⽬とし、1~3サイクル以内にackが1となることを仕様として求める記述です。1サイクル⽬、2サイクル⽬、3サイクル⽬にack信号が1になれば仕様を満たし、a_req_ackと名付けたアサーションはパスし、それ以外の振舞いをした場合、a_req_ackはフェイルします。

property req_ack;
  @(posedge clk) $rose(req) |-> ##[1:3] ack;
endproperty
a_req_ack: assert property(req_ack);

シミュレーションでの扱い

シミュレーションではアサーションのパス／フェイルの情報を、波形やリスト、スレッドビューなど様々な表現で解析することができます。波形ウィンドウではAssertionsペイン内にアサーションを▲で表⽰します。波形上ではアサーションがパスすれば▲が、フェイルすれば▼が表⽰されます。

assert_pkt_lengthは70425nsでパスし、assert_ram_write_check_IOは70435nsでフェイルしていることが確認できます。各アサーション名の[+]をクリックすることで、そのアサーションを構成する信号レベルへと展開できるため、どの信号が原因でフェイルしているかを知ることができます。アサーションによるチェック／監視は、ちょうど波形の⽬視確認を⾃動化していると考えることもできます。

アサーションの価値

アサーションをRTL設計に追加することで、バグがあった場合にはその特定もデバッグも容易になります。あるバグをテストパターンが活性化し、その不正な振舞いを出⼒段まで伝搬するのに最短で10万サイクルかかるとすると、アサーションがこのバグを検出すれば、その10万サイクル分のシミュレーションは不要になります。機能検証のおよそ50%もの時間が費やされるデバッグ⼯数を削減できるだけでなく、シミュレーションのライセンス数も適正量に抑えられる可能性があります。

またバグがなかった場合であっても、波形を⽬視確認する労⼒を削減することができます。この検証労⼒削減の効果はそのプロジェクトでの省⼒化に限定されません。アサーションは検証資産として異なるプロジェクトや異なる部⾨で再利⽤することができます。さらに再利⽤性の⾼いブロックやIPの開発時に、その⼊出⼒インタフェース部分にアサーションを追加しておけば、IPとそれに接続する他のブロックとのプロトコルに関する問題が発⽣した際に、問題の切り分けが容易になります。

フォーマル検証の活用

アサーションはフォーマル検証でも使⽤できます。
シミュレーションではテストパターンにより設計空間内の探索が⽅向付けられますが、フォーマル検証では初期値から開始して、設計空間が取り得る値を網羅的に探索します。そしてアサーションをターゲットにあらゆるステートの組み合わせを照らし合わせ、違反ないことを証明するか、違反があった場合にはその状態を再現するパターンを最⼩サイクルで提⽰します。FPGAプロジェクトでもフォーマル検証の採⽤が進んでいます。

 

 

「アサーションベース設計 立ち上げ支援サービス」をご利用ください

Wilson Research Groupが実施した機能検証の市場調査によれば、アサーションを使用する大多数はSystemVerilog Assertions（SVA）を使用しています。SVAは2005年にIEEE標準となっています。新たな手法が登場したときに、それを開発フローに導入するには、言語の習得に始まり、その効果を評価しては改善するなど、多くの労力を要します。
PALTEKではこの労力を低減し、誰もがアサーションを使い始められるようにするための支援策として、「アサーションベース設計 立ち上げ支援サービス」を提供しています。

「アサーションベース設計 立ち上げ支援サービス」についてはこちらをご覧ください

関連情報

関連ウェビナー

関連TECHブログ

アサーション関連のセミナー情報/ブログへ

シーメンス EDAのことなら
PALTEKにご相談ください！

シーメンス EDAのことならPALTEKにご相談ください！

シーメンス EDA製品の
お問い合わせ

03-5479-7025

株式会社PALTEK デザインサービス事業部
シーメンス EDA製品サポート窓口