貢献度が高まるフォーマル検証-これはシミュレーションでは無理でした
EDA Express読者の皆様こんにちは。
私はＣｙｂｅｒＴｅｃ（サイバーテック）株式会社の片山勝博と申します。
ＣｙｂｅｒＴｅｃは長年ハードウェア設計における機能検証という分野にフォーカスした製品・サービスを提供している会社で、現在はフォーマル検証ツールのリーダーである米Jasper Design Automation社の日本総代理店としてお客様の検証課題と取り組んでおります。
一昔前とは違い、ここ最近は日本でもフォーマル検証技術の利用が一般的になりつつあるかと思いますが、その中でも一歩先を行く米Jasper Design Automation社の製品につきまして、これから3回にわたり最新のフォーマル技術の利用動向についてご紹介したいと思います。
■■ますます高まるフォーマル検証の貢献
今、フォーマル検証はどのように貢献しているか。
以下はJasper社フォーマル検証ツールJasperGoldユーザーの声です。
・シミュレーションでは出来なかったった複雑なステートマシンの一発動作をさせることが出来た。
・シミュレーションで検証済みだったのに、フォーマル検証でコーナーケースのバグが発見された。
・実チップで発見された不具合に対してワークアラウンドでバグが回避できることをフォーマル検証で証明できたのでリスピンせずに済んだ。
・シミュレーションによるアサーション検証に比べて検証期間を1/2から1/3に減らすことができた。
このようにフォーマル検証の貢献が高まっている最大の理由は、従来からお使いのシミュレーション手法に限界が来ていることにあります。
その限界を克服するために求められているのがフォーマル検証です。
つまり時代がフォーマル検証を必要とするようになっている、と言えます。
フォーマル検証の利点の１つは、シミュレーションでは実質不可能な入力の全ての組み合わせを網羅検証出来ることです。シミュレーションのようにテストベンチの機能やテストベクタの質や数に依存することなく、確実な検証が可能になりますので新機能や重要な機能などに対し網羅検証を行い、動作の信頼性を高めることができます。
また別の利点としては、シミュレーションと違いテストベンチやテストベクターが一切不要で、RTLとアサーションがあれば、即座に網羅検証が可能なことです。
設計しながら検証することが可能になりますので、設計初期からアサーション検証を行いブロックレベルの設計品質が向上し、開発後半で見つかるバグによるリグレッションの回数を減らすことが出来ます。
フォーマル検証の利点を生かした検証で、JasperGoldでよく利用されている効果的な検証としては以下のようなものがあります。
・組み合わせの数が膨大な回路の検証
（対象例）テスト回路の接続検証、アービター、割り込み制御回路
シミュレーションとは違い入力の全ての組み合わせを網羅検証しますので、漏れのない検証を行うことができます。
（対象例）ブリッジ
シミュレーションでは動作の保証ができませんが、フォーマル検証は絶対に起きないことを証明することができます。
・バグ対策の正当性やワークアラウンドでバグを回避できるかどうかの検証
これも、デッドロックやハングアップの検証同様に、シミュレーションでは動作の保証ができませんが、フォーマルでは動作について100%証明できることにより可能となります。
・End-to-Endでデータ転送が正しく行われていることの検証
JasperGoldには、予め用意されたハイレベルなプロパティおよびモデリング群 Jasper Proof Accelerators™があり、その中の一つJasper Formal Scoreboardを利用すれば、 接続するだけでデータ転送の検証を行うことができます。
JasperGoldでは、こうした検証を可能にするため検証容量の拡張、パラレルエンジンの導入といった基本性能の向上が図られるとともに、複雑な検証を容易に実現し検証期間を短縮するためのハイレベルなプロパティおよびモデリング群Jasper Proof Accelerators™(スコアボード検証、キャッシュのデータ正当性検証、SDRAM、DDR、など）、フォーマル検証に最適化された標準インターフェースのプロトコル検証モジュールJasper Proof Kits(OCP、AXI、AHB、APB、USB、PCI、PCI-Eｘpress、など)などが提供され、効率的に取り組めるようになっています。
■■まとめ
設計初期からフォーマル検証を使うことでブロックレベルの品質が向上され、重要な機能の網羅検証を行うことで動作の信頼性を高めることができます。
また実チップでのバグ対策などにもフォーマル検証が非常に有効利用されています。
このようにフォーマル検証を使うことで従来のシミュレーションでは困難な検証を実行できるようになり品質向上や検証を前倒してゆくことなどが可能になります。
※本掲載記事は次回の「さらに広がるフォーマル検証の適用」に続きます。
<筆者プロフィール>
ＣｙｂｅｒＴｅｃ株式会社 片山 勝博
EDAの日本代理店を経てＣｙｂｅｒＴｅｃにおいて営業として社内の検証コンサルタントと共に顧客の検証課題に対するソリューションを提供中。