THE SOUND OF CADENCE Vol.71 (January 2010)

ここでもエコ、次世代のハイブリッド・エンジン“Incisive Enterprise Verifier”

検証ソリューション＝検証メソドロジ＋検証テクノロジ

検証の効率を向上するためには、メトリクス・ドリブン検証（MDV：Metrics Driven Verification）などの検証メソドロジを上手に活用し、機能検証のフローを見直すことが王道であり、また早道であることは、論を待ちません。この検証メソドロジ、また、メソドロジを実際に適用する上での基本部品としての検証I Pについては、これまでも小誌の中でご紹介してきました。

図1：ケイデンスの提供する検証テクノロジ

一方、検証メソドロジに沿った形で作られる検証フローの各プロセスの多くは、EDAツール、すなわち、検証テクノロジにより実現されます。検証プラン作成など、従来機械化できなかったプロセスについても、Incisive Enterprise Manager（およびそれに含まれる機能であるIncisive Enterprise Planner）などの新しいテクノロジがあり、これについても今までにご紹介しました。検証テクノロジを、検証環境を構築するツール群（例：Incisive Enterprise Manager）と、与えられた検証環境を実行するツール群（検証エンジンと呼びます。例：Incisive Enterprise Si mul ator）に分けたとき、今回はシミュレーションやフォーマル解析のような検証エンジンについてご紹介します。

アサーションベース検証の活用：再び

近年、広く使用され始めているアサーションは、波形図での目視チェックや、スコアボードなどの期待値比較型チェッカでは見つけにくかった、もしくは見つけるのに時間がかかっていたような、不正な動作の検出に大きな効果があります。アサーションを用いた検証のためのエンジンは、大きく分けて次の2種類になります。

1．	シミュレーション（ダイナミック ABV）
2．	フォーマル解析（スタティック ABV）

それぞれのエンジンには、それぞれに異なる特徴と、適したユースケースがあります。 シミュレーションでは、検証のためにはなんらかのテストベンチが必要となります。また、検証の品質はテストベンチの質と量に依存します。計算時間は、検証中に発生するイベント数に律速されますが、一般に大規模な検証課題を扱うことが可能です。

一方、フォーマル解析は、テストベンチは不必要です。検証の品質はアサーション／アサンプションの質と量に依存しますが、数学的証明手法をベースにしているので網羅性が高く、コーナーケース・バグですら検出が可能です。計算時間は検証するデザイン（DUV：Design Under Verification）およびアサーションの複雑さと量に依存しますが、SoC全体の検証を行うのは現状の技術では難しいものがあります。 これらの特徴の差を考慮し、長所を生かし、短所を補うための検証フローとして、CABV：Complete Assertion Based Verificationを従来から（例えば、2005年6月発行のTHE SOUND OF CADENCE,Vol.62をご覧ください）提唱してきました。

図2：Complete Assertion Based Verificationフロー

CABVでは、単体検査はフォーマル解析を使用して行います。テストベンチの完成を待たずに開始できることで、検証開始を前倒しにできます。フォーマル解析の網羅性を活用し、単体レベルでの機能的な作り込みを確実にします。 結合検査では、シミュレータが中心となります。単体ブロックの内部は単体検査で十分に調べられていますので、結合検査ではブロック間の結合の整合性を中心に調べることになります。単体検査でのインタフェース部分のアサンプションは、結合検査でのアサーションとして再利用可能ですし、単体検査でのアサーションは、設計者の気になる問題ポイントを示していることが多いので、これらを結合検査でのカバレッジとして再利用すると、問題のありそうな状況を調べることができたかの判断材料として活用できます。また、統合検査では、回路規模が大きくなり、検証実行時間も長くなるため、アクセラレータ/エミュレータによる高速化も重要です。

このような検証フローを実現するためには、SVAやPSLで書かれたアサーション（より厳密にはプロパティ）の検証フェーズ間での再利用が必須です。エンジンごとに書き換えが発生してしまっては、書き換えの工数や書き換えることによる品質問題を考えると、現実的な解とはいえないからです。フォーマル解析/シミュレーション/アクセラレーションが同一のプロパティ記述を使用でき、かつ同様のセマンティクスとして解釈できる必要があります。CABVを上手に活用することで、生産性と品質の向上と、検証の工期と負荷の削減の両方が可能となります。

ハイブリッド・エンジン：Incisive Enterprise Verifier

このように、設計・検証における回路規模のスケーラビリティに対応したCABVですが、近年の回路の一層の複雑さの増大や比較的大きな単位での設計IPの再利用が増えてきたことにより、下記のような状況が増えてきています。

1．	結合検査のためのテストベンチが複雑化し、テストベンチ完成が遅れがちになる
2．	単体検証でも、回路規模が大きくなっている

そのため、より大きなブロックの単体検証、そして可能であれば初期の結合検査についても、フォーマル解析テクノロジで実施したいという要求が増えています。 この要求に対応したテクノロジが、Incisive Enterprise Verifier（以下、IEV）です。

図3：ケイデンスが提供するハイブリッド・フォーマル・テクノロジ

ケイデンスが提供するハイブリッド・フォーマル・テクノロジであるIEVは、シミュレーションとフォーマル解析を組み合わせる ことで、両者の良いところ取りをしています。第一世代のハイブリッド・エンジンでは、シミュレーションのパタンやダンプデータが必要であり、テストベンチ開発を待つ必要が発生し、検証開始の前倒しが困難でした。IEVでは、ケイデンスのフォーマル解析テクノロジIFV（Incisive Formal Verifier）の環境をそのまま再利用できます。これは、言い換えると、テストベンチ環境は必要なく検証を開始できるということです。

IEVでは、IFVであれば‘Explored’となって検証できないアサーションを検証対象として、自動的にシミュレーションを併用しながらハイブリッドのエンジンを実行します。これにより、単独のフォーマル解析やシミュレーションでは見逃すバグを発見可能となります。 IFVおよびIEVは、BDDやATPG、SATなど複数のエンジンを持っています。これらのエンジンの中から、検証対象にあわせた最適なエンジンを選択しながらアサーションのチェックを行います。近年、マルチコア/マルチプロセッサ・マシンが増えていますが、IFVではそれぞれのエンジンをプロセッサに割り付け、高速に並列実行できる機能が用意されていますが、IEVでもこの機能を十二分に使用できるようになっています。さらに、アサーション毎にプロセッサを割り付けることで、数多くのアサーションが埋め込まれたデザインの高速化も可能となっています。このような高速化技術により、従来では対応できなかった統合試験レベルの回路であっても、フォーマル解析テクノロジの適用が可能になってきています。

IESシミュレータにおけるマルチコア対応による高速化

ここまで、IEVを中心に述べ、マルチコア対応による高速化についてもご紹介しました。マルチコア対応による高速化は、IES （Incisive Enterprise Simulator）でも「パフォーマンス・オプション」として提供しています。例えば、波形ダンプをシミュレーション実行とは別のCPUで実行させることで、全体の実行時間やメモリ消費を大幅に抑えることができるようになっています。

まとめ

機能検証の効率化には、検証メソドロジの上手な活用とともに、検証テクノロジの正しい選択が必要です。 検証エンジンの選択は使用する検証フローにより定義されますが、効率的な検証フローの確立のためには、検証フローをシームレスに構成できなら、かつ単体としての性能も両立している検証エンジンを使用することが必要です。 検証エンジンの効率向上について、ケイデンスは常に大きな努力を払い、改善し続けています

カスタマ・プラットフォーム・マーケティング部 後藤　謙治