フォーマル検証は助けになるのか？

ASHISH DARBARI

なぜ、シリコンにバグを残すことなく、高品質なサインオフを確実に行うことがいまだに難しいのだろうか？DVConで会った同僚によれば、その答えは非常に微妙だという。業界は全体的には改善しているが、デザインの複雑さも進んでいる。

Wilson Research Group / Siemens EDAの最近のレポートでは、調査対象となったASIC設計の74%が1つ以上のプロセッサコアを持ち、52%が2つ以上のコア、15%が8つ以上のプロセッサコアを持っている。注目すべきは、ASICの32%がAIコアを搭載している一方で、30%がRISC-Vプロセッサを搭載していること、そして58%がセーフティ・クリティカルなチップを開発しており、なんと60%以上がISO 26262準拠を必要とするASICのチップを開発していることである。自動車はASICの急成長分野である。セキュリティ検証も大きく飛躍しており、FPGAプロジェクトの71％、ASICプロジェクトの75％がセキュリティとセーフティを同時に検討している。ASICの72％が積極的に消費電力を管理しているともあり、消費電力管理の検証は重要な課題となっている。

レポートによると、ASICプロジェクトの66％、FPGAベースのプロジェクトの70％がスケジュールに対して遅れている。驚くべきはASICの76％が2回以上のリスピンを必要としていることだ。同時に、検証エンジニアと設計エンジニアの比率は1：1になっている。一方、2020年に発表された前回のレポートでは、FPGAプロジェクトの68％が予定より遅れており、プロセッサのデザインハウスの場合、検証エンジニアの設計者に対するリソース比率は5:1となっている。2007年と比較すると、検証エンジニアは145％増加し、設計エンジニアは50％増加している。では、検証エンジニアが設計者の3倍も増加しているにもかかわらず、なぜASICプロジェクトの66％、FPGAプロジェクトの70％がスケジュール遅延を起こしているのだろうか？またASICの76％が2回以上のリスピンを要しているのはなぜだろうか？

ラップトップ、PC、サーバー、AIチップ、スマートウォッチと呼ばれるような、1,000万ゲートから10億ゲートのASIC設計のうち、初回に成功するのはわずか13%に過ぎない。最も驚くべき発見は、ASICのリスピンの最大の原因がロジック／機能の欠陥であるということだ。これらの欠陥の62％がリスピンを引き起こしている。もしフォーマルメソドロジが正しい方法論で計画通りに採用されていれば、このような事態は完全に回避できたはずである。

検証技術の導入傾向

検証のランドスケープで言うならば、UVMとディレクテッド・テストが支配的であることは周知の事実である。

ダイナミック・シミュレーションではアサーションの利用が増加しているが、アサーション・ベースのフォーマル検証もまだ主流になる必要がある。フォーマル検証の普及が進んでいないことは、我々が取り組むべき課題であり、この統計レポートは我々全員にとって目から鱗のはずである。

フォーマルメソッドを用いた疑いの余地がない検証

私たちは、コーナーケースのバグを早期に発見し、それが存在しないことを証明し、飛行機や自動車に搭載されるシリコンが安全でセキュアであることを保証する必要がある。私たちの生活で使用されるシリコンの数が増えている現在、Ariane 5の爆発、GoFetch、メルトダウン型のセキュリティシナリオ、FDIVなどを許容する余裕は私たちにはない。

フォーマル検証は、バグがないことの証明を築く唯一の方法である。私は、フォーマルは今やメインストリームになりつつあると信じているが、これを裏付けるためにWilson Researchの調査に目を向けることにする。Siemens EDAが、当初メンター・グラフィックスが始めたこの調査のスポンサーを続けてくれていること、そしてハリー・フォスターが再び、主要な調査結果をまとめた素晴らしい一連のブログ記事を投稿してくれたことを嬉しく思う。

私にとって最も興味深い発見は、現在ASICプロジェクトの3分の1以上が検証フローの一部にフォーマル・プロパティチェックを使用していることである（図1参照）。捉えたいデータは、このフォーマルの採用がバグハンティングやバグ回避に与える影響度である。興味深いのは、このデータをよりオープンな調査の中で、進んで開示するかどうかであろう。

この数値は低いパーセンテージに思えるかもしれないが、多くの比較的小規模なASIC設計では、依然として古いプロセステクノロジのノードが使われている。

この調査から明らかな傾向として、設計規模が大きくなるにつれて、あらゆる高度な検証技術の採用が増加していることが挙げられる。1,000万ゲートを超えるASICプロジェクトの約半数がプロパティチェックを使用している。フォーマル検証が、今やユビキタスとなっているシミュレーションの採用率の半分を達成したことは、大きな意味がある！

自動フォーマル技術の採用は、プロパティチェックよりも少し劣る。クロック/リセットのドメインクロッシング(CDC/RDC)や接続性チェックなど、ユーザがアサーションを書かなくてもフォーマルによる証明の価値が得られる重要なアプリケーションがいくつかある。一部のツールは、このようなチェックをアドバンスト・リンティングとして分類しているが、実際にはツール内部でフォーマルエンジンが使われており、ユーザがどのようにレポートしているかに依存する部分もある。

プロパティ・チェックにはプロパティを記述する必要があるため、ASICプロジェクトのほぼ70%（図2参照）がアサーションを採用しており、SystemVerilog Assertions（SVA）が最も広く使用されていることを確認できたのは喜ばしいことである。またこの調査は、Universal Verification Methodology（UVM）や他のあらゆる最新のテストベンチ・アプローチの中核をなす制約付きランダムスティミュラス生成よりも、アサーションを使用するプロジェクトが多いことを示している。

アサーションを使用するプロジェクトの半数しかフォーマル検証を使用していないため、多くのアサーションはまだシミュレーションでのみ実行されていることになる。アサーションの一部はフォーマル解析に適しているが、設計チームと検証チームは、設計意図をアサーションに変換するという困難な作業をすでに終えている。フォーマル・プロパティチェックを試してみるべきであろう。

FPGA開発者は、フォーマル技術を含むすべての高度な検証手法の採用において、ASIC開発者に追いつく必要がある。歴史的に、FPGA設計は一般的にASICよりも小さく複雑ではない。FPGAは、バグが発見された場合、立上げの実験室でも現場でも、再プログラムが可能である。このため、一般的にシリコン前の検証はあまり重視されず、実験室でのテストへの依存度が高くなっている。

しかしこれは劇的に変化している。最も大規模なFPGAは、複数のプロセッサや特殊なアクセラレータを備えたシステム・オン・チップ（SoC）設計である。実験室での立上げでバグの原因を特定するには数日から数週間を要し、毎回、可能な修正を試すために、長時間の再プログラミング・ループが必要になる。その結果、FPGAチームはASIC開発者と同じ検証ツールや手法を使用するように変わってきている。

Wilson Researchの調査によると、FPGAプロジェクトの40%以上がアサーションを採用しており（図3を参照）、ASICと同様、アサーションは制約付きランダムテストよりも多く使用されている。FPGAプロジェクトの15%以上が自動フォーマルツールを使用し（図4参照）、25%近くがフォーマル・プロパティチェックを使用している。興味深いことに、アサーションとフォーマルの比率は、ASICよりもFPGAの方が開きが小さく、シミュレーションのみのアサーションの使用割合は少ない。

フォーマル検証の利用が増加している背景は明確である。それは初回のシリコンでチップを正しく作ることが常に困難になっているからである。この調査によると、ASICの76%は、量産準備が整うまでに1回以上のリスピン（再ファブリケーション）を必要としている。

スピンごとにプロジェクトコストが数百万ドル増加し、スケジュールが数か月延長される。さらに、最終製品が競合他社に比べて市場投入が遅れた場合に発生する数千万ドルから数億ドルの収益損失分は考慮されていない。

また、この調査では、FPGA設計の84%で、最終製品によってバグが市場流出していることが判明している。これらのデバイスを現場で再プログラミングまたは交換することは、可能であるとしても非常に高価な作業となる。生産中のFPGA設計の半数以上にロジックまたは機能的なバグがあり、これらのバグはすべてフォーマル検証をより適切に適用すれば発見できるはずである。同様に、ASICのリスピンの半分以上はロジックまたは機能バグが原因である。

フォーマル検証： 高まる必要性

フォーマル検証の市場を長い期間に渡って注視してきたが、このテクノロジーへの注目度が高まっていることも一つの指標である。EDAの主要ベンダー3社すべてが、フォーマル検証の製品で成功を収め、活発な研究開発活動を展開し、ニーズと要求が高まるユーザをサポートしています。Axiomiseに対しては、ユーザの社内チームを補い、メソドロジとベストプラクティスを確立するために、フォーマルエキスパートに対する需要が着実に高まっている。

私は、フォーマル検証のメソドロジについて議論し、ユーザが商用ツールで成功を収めるのを支援するため、世界中を飛び回る機会に恵まれた。私は、フォーマル検証のメソドロジがいかに強力なものであるか、また、そうでなければ見つけることがほとんど不可能であったバグを見つけたときのユーザの喜びを目の当たりにしてきた。設計の正しさが証明されれば、機能的なバグによるリスピンを憂慮することなく、自信を持ってテープアウトすることができる。

このような理由から、フォーマル検証のキャパシティとユーザビリティがどれほど進歩し、採用がどれほど進んだかを目の当たりにするのは非常にエキサイティングなことである。まだフォーマル検証を試したことがないのであれば、ぜひ試してみてほしい。自動フォーマルツールは、最小限のセットアップですぐに使えるし、シミュレーション用のアサーションがすでにあれば、プロパティチェックのツールで簡単に試すことができる。私は、あなたがその結果に満足し、次のWilson Researchの調査の際に、あなた自身の経験を報告するだろうと予測している。全体として、フォーマル検証を設計検証フローの早い段階で一貫して採用すれば、検証のクライシスは多くのケースで確実に緩和されるはずである。

著者:
Axiomise, Ashish Darbari