製品の高機能化が急速に進み、搭載するLSIの回路規模増大によって複雑な実装を行う必要に迫られています。たとえば、省電力化が求められる一方で処理速度を追求するなど、相反する状態を達成するため、ただでさえ複雑な機能にさらに機能を上乗せした設計が必要になります。設計の複雑化に伴い、検証する作業量も膨大になります。これが喫緊の課題となっています。
　LSI開発の工程は、仕様検討、回路設計、機能検証、論理合成、そして量産という流れです。なかでも「機能検証」が最も時間を要する工程だと言って良いでしょう。検証工数が増えればコストに反映してしまいます。

　検証を十分に行わなかった結果、後工程での不具合発覚による作業の手戻りの発生や、量産後に不具合が見つかってクレームになってしまうなど、お客様の信頼を損ね次の製品開発に影響を及ぼしてしまうケースもあります。製品の要求仕様が決まっているため、設計段階で機能を勝手に削ってしまうことはできませんし、決まった期間内に開発を終えるためにはいつまでも検証作業を続けるわけにもいきません。しかし、開発期間を優先して検証範囲を狭めると、不具合の見逃しにつながりかねません。現場からも「より効率よく検証したい」、「より品質高く検証したい」という声が多く出ていました。
　限られた開発期間内に求められている機能すべてを確認するため、より検証しやすいように設計の変更を依頼することもあります。設計工数が増えたとしても、それ以上に検証工数が削減できれば製品開発全体としては工数の削減になるためです。より品質の高い製品を、いかに短い時間で開発できるかが重要なのです。
　検証には、「シミュレーション検証」、「ランダム検証」、「フォーマル検証」と大きく3つの方法があります。(図-1)
　シミュレーション検証は、一つひとつ入力信号のパターンをつくり、正しい出力かを確認する検証手法です。一つの入力パターンで確認できれば良いのですが、実際は、どのようなパターンで確認すべきか検証者が検証項目表を作成し、数百種類の入力パターンを作成して確認します。しかし、その項目に漏れがあると、入力パターンも作成されず、不具合に気づくことができません。
　ランダム検証は、シミュレーション検証をベースにしている検証方法です。入力する値の組み合わせ範囲にルールを決め、入力パターンの生成を機械に任せます。この時に重要なのは、検証者が確認したいパターンが発生したかどうかの確認をすることです。機械任せなので同じパターンばかり発生してしまい、確認が不十分になる可能性があるからです。これを必要な組み合わせが発生したかを確認する、カバレッジ工程で補完します。シミュレーション検証で必要となる検証項目表が、ランダム検証のカバレッジ項目になります。入力パターンを一つひとつ作成する必要はありませんが、確認したい項目に漏れがある場合は不具合を見逃してしまいます。シミュレーション検証の検証項目表と同じく、このカバレッジ項目の確認が重要です。
　フォーマル検証は数学がベースになっています。科学的に裏付けされた仕様記述言語を使用し、曖昧さがない機械処理を行うのが特徴です。検証者は回路の要求仕様から守るべきルールを定義します。フォーマル検証ツールは、回路がどのような構造になっているのかを解析し、要求仕様を記した守るべきルールとの間に差異がないかを計算で確認する新たな検証方法です。

　シミュレーション検証では、パターン入力と結果確認の両方を人が行うため、項目を作成する段階で気づけなかったパターンについては確認されません。ランダム検証では機械任せにランダムパターンを生成させますが、人が気づけなかったパターンが発生するかは運任せとなります。いずれも検証者のスキルによって検証品質に差が出てしまいます。一方、フォーマル検証では「同じ構造となっているか？常にルール(要求仕様)を守れるか？」を答えが明確に示される数式の形に変換して確認するため、検証者のスキルに依存せず、曖昧さを排除した状態で常に正しいかを確認することができます。

　当社ではフォーマル検証とシミュレーション検証を組み合わせることでトータルの開発コストを削減できるような検証方法を推奨しています。図-1で示したように、シミュレーション検証にもフォーマル検証にも、それぞれ得手不得手があります。例えば、機能を実装している各ブロックは網羅性を実現できるフォーマル検証で確認し、複数のブロックを接続した状態での確認は広範囲でも確認が可能なシミュレーション検証で実施するなど、それぞれの得意分野を組み合わせることで全体の検証を行います。このような連携を実現するには、どのような構成で設計されているかが重要になります。フォーマル検証を適用しやすい形でブロック分割していないと、もともと確認したかった内容とのズレが発生し、不具合を見逃してしまうこともあり得ます。また、同じ機能を実現する回路であっても、設計によってはフォーマル検証の計算時間が数十倍に伸びてしまうこともあります。そのような問題を防ぐ意味でも、フォーマル検証とシミュレーション検証の適用範囲の見極め、さらにはフォーマル検証を見据えた設計手法を取り入れることが重要となります。
　以下の事例は、製品Aと製品Bに対してシミュレーション検証とフォーマル検証を組み合わせて検証した結果です（図-2）。両製品とも破線の左側がシミュレーション検証で見つけた不具合のコストの累計値（人日）、右側がフォーマル検証で見つけた不具合のコストの累積値となります。ここで、フォーマル検証を適用せずにシミュレーション検証のみで同じ不具合を見つけようとした場合のコストについて試算してみました。

　この例では、製品Aはシミュレーション検証を単独で使うよりも166人日、製品Bでは210人日、短く検証を終わらせることができ、開発コストの大きな削減に寄与しました。フォーマル検証では、シミュレーション検証では見逃しやすい、複雑な条件の組合せでのみ発生する不具合(レアケース、コーナーケース)なども簡単に見つけることができるため、シミュレーション検証のみでは製品化するまで気づけない不具合の排除も可能です。フォーマル検証を活用することで、より高い品質をより少ないコストで実現することができます。

　当社では半導体回路の検証に「フォーマル検証」を推奨していますが、フォーマル検証を使いこなすには専門知識が必要なため導入のハードルの高さが課題になっています。そのため私たちは、長年にわたる開発で培った経験をもとに、お客様の課題を解決する「フォーマル検証ソリューション」を提供しています。(図-3)

　具体的には、フォーマル検証の教育サービス、使い勝手を大幅に改善する導入サービスという2つの視点でアプローチしています。
　これは、お客様自身が設計・検証を行う場合には、フォーマル検証のサポートメニューを提供するということです。
　技術的な課題には教育サービスで、フォーマル検証に適した設計手法や、フォーマル検証を行ううえで検証者が意識しなければならない点などをご理解いただきます。これにより基礎理論をベースにしたフォーマル検証向けの設計・検証手法を習得し、ターンアラウンドタイムの短縮と収束性向上につなげます。
　また、運用上の課題には導入サービスとして、フォーマル検証を行うための環境を提供します。フォーマル検証を深く理解できていなくても、またツールのマニュアルを読み解かなくても、お客様が手軽にツールを使える環境を整えられることを目的にサポートします。Cadence^®社のJasper™ Formal Verification Appsを、誰でも手軽に使える実行環境として提供し、フォーマル検証環境の立ち上げをサポートします。(図-4)

　当社はこれからもLSI開発を行うお客様に対して、フォーマル検証ソリューションの提供をはじめ、お客様の課題解決に向けて最適解となるサービスを提供していきます。

※記事内における内容、組織名、役職などは2022年7月公開時のものです。
※本文中の会社名および製品名は各社が商標または登録商標として使用している場合があります。