アサーション・ベース検証によりハイエンド・サーバー向けASIC設計のコーナーケースを活性化

　エンタープライズ向けコンピューティング・ソリューションで世界をリードする企業であるSun Microsystems（以下Sun）が製造するワークステーションおよびハイエンド・サーバーは、クラス最高レベルの通信帯域幅、最小レベルのレイテンシを特長としています。Sunの設計検証担当マネージャであるPaul Gingras氏は、いくつかの非常に大規模かつ複雑なコンポーネントを搭載した、ハイエンド・サーバー向けの大規模ASICの検証を担当していました。

　このASICは設計サイクルの最後にデバイス内のトランザクションの流れを制御するための複雑な遅延制限用モジュールが追加されました。この新しいロジックは設計に含まれる他の多くのモジュールと接続され、複雑な調停スキームを採用していました。この時点で、既に設計は3百万ゲート規模に達しており、 I/Oピンも800を超えていました。Sunは、全ての発生しうるコーナーケース動作を解析するためにダイレクテッド・テストで記述するのは非常に難しく、時間が掛かると判断しました。

　「我々が直面とした大きな問題の１つに、従来のシミュレーションが持つランダムな側面をどのように改善していったらよいか、ということがありました。」 Gingras氏はこのように語っています。「テープアウトする前にデザインに対するカバレッジを改善する必要があったのです。」Sunは新しい遅延制限モジュールを含む、設計のホットスポットの解析に0-InのAssertion-Based Verification （ABV）Suiteが使えないかと考えました。

0-Inを使ったチェックにより有効なアサーション手法を実現

　Sunの開発チームは、RTLシミュレータを市販のテストベンチおよびカバレッジ・ツールと組み合わせた、高度な設計・検証手法を適用していました。 0-InのABV Suiteはこれらのツールにはない、重要な機能を付け加えることになりました。ASIC設計の内部構造を解析することにより、ABV技術は機能検証の2 つの主要な問題、すなわち観測性の限界と不十分な制御性という問題に挑戦しました。

0-Inツールは、CheckerWareライブラリを使うことにより、ASIC設計内部の観測性を改善しました。チェッカとは、統計情報収集とコーナーケース解析用ロジックを加えたアサーションです。これらのチェッカを使うことにより開発者は設計インタフェースの検証と文書化、並びに業界でも最も厳しい指標を使用したテストスイートの評価が行えます。チェッカはRTLで記述されているため、使用されている特定のテストベンチ並びに検証言語に依存しません。

0-In付属の豊富なCheckerWareライブラリを使って設計に対する仮定条件を設定することにより、ASIC設計者は最小限の指定で最大限の設計チェックを実施することができました。

「0-Inが非常によくフィットした大きな理由は、設計にステートメントを挿入する、あるいは設計意図を表現したアサーションを設定する等の点において弊社の既存手法に合致していたためです。」Gingras氏はこのように述べています。「設計部門のマネージャーと私がチェッカを使用する工程スケジュールを作成し終えた頃には、エンジニアはそれらを既に設計で利用していました。エンジニアは説明書を少し見ただけで、これらのチェッカを使った設計を非常に短時間に作成してしまいました。」

「我々はまた、0-Inの提供する直接推定のfull_caseおよびparallel_caseチェッカもフルに活用しました。」Gingas氏はプロジェクトを振り返ってこのように語りました。0-In Checkにより自動的に挿入されたcaseチェッカによって、default caseがcase/endcaseブロック外にあることによる設計エラーを検出しました。設計者はまた、req_ack、one_hot、 maximum、value、arbiter等のチェッカを使って、設計に関する様々な重要アサーションを指定しました。

設計エラーが見つかった場合、その原因の追跡は従来難しい作業でした。しかし、0-In Checkではエラーをその原因箇所で検出することによるデバッグが可能です。「システム検証を行ったことのある担当者なら誰しもが認識していることですが、欠陥を切り分けるのは非常に難しい作業です。」Gingras氏はこのように説明しています。「欠陥を見つけてもそれは実際の問題の7000サイクル後である場合もあります。チェッカーが有効になっていて、設計内に配置されていれば、エラーが実際に起こった場所にかなり近いところでそれをとらえることができます。」

0-In Searchはコーナーケース・ロジックのエラーを検出

　0-In Searchを使ってコーナーケースの動作を直接実行することにより設計のコントロール性を高めることができます。.0-In Searchはダイナミック・フォーマル検証技術、すなわちシミュレーションとフォーマル・テクニックの組み合わせにより設計を解析し、コーナーケースにストレステストを行い、ダイレクテッド・テストや疑似ランダム・テストでは見逃されてしまうバグを検出します。フォーマル解析により既存のシミュレーション・テストを「増幅」させることにより、0-In Searchはテストを追加記述することなく、より徹底した設計検証を行うことができます。

遅延制限モジュールはその複雑性により検証ホットスポットであることが判明したため、検証チームはフォーマル検証の適用を決めました。遅延制限モジュールに含まれる特定の複雑なロジックを検証するためにダイレクテッド・テストを記述する代わりに、Sunの設計チームはロジック内にチェッカを配置し、0- In Searchを使って既存のシミュレーション・テストを「増幅」することができます。

この手法を使うことにより、 0-In Searchはdiscardカウンタのコントロール・ロジックに含まれるごくわずかなエラーによって、カウンタ・ロジックが突然リセットされる問題を引き起こすことをつきとめました。このエラーにより破棄されるべきであった一部のトランザクションがそのまま処理されていたのです。この問題は0-In Searchのオーバーフロー・チェッカにより、Sunの検証チームが記述したテストの1つを「増幅」することにより検出されました。このエラーはシミュレーションで観測することは根本的に不可能であったはずです。なぜならば唯一の影響は不適切な帯域幅調整によるシステム・スループットの悪化のみだからです。この問題が検出されなければ、すべてのトランザクションは成功するにも関わらず、最終的なパフォーマンスは低いという結果になっていたでしょう。

「0-In Search は設計のタイムアウト・ロジックに含まれるエラーも発見しました。」とGingras氏は語ります。「コントロール・ステータス・レジスタとして上限が定義してあり、しきい値に達すると減速を始めるようになっていました。しかしそのしきい値を超えてしまっていたのです。結果的にそのしきい値を超えてどんどん進んでしまっていました。この問題は従来のテスト手法では発見されませんでしたが、0-In Searchは問題があることを即座に検知しました。チェッカを関連づけておくことで 0-In Searchは設計のその側面を解析することができたのです。」

ABVによりテープアウトの信頼性を向上

　「ハードウェア検証グループのマネージャーである私は、常に上司から『テープアウトできるか?』と聞かれます。0-InのABV Suiteの素晴らしい点は、私の自信を本当に高めてくれたことです。ダイナミック・フォーマル検証は私のテストベンチに盛り込まれた知識を拡大し、これまでカバーされていなかった設計の様々な側面を徹底して追及してくれます。これは私にとって大きな自信となり、上司のオフィスに入り気分良く『準備できます！』と言えるのです。」 Gingras氏はこのように語ります。
 

• CheckerWareチェッカにより検証の難しいロジックの観測性を向上
• 0-In Searchはダイレクテッド／疑似ランダム・テストベンチで見逃されるコーナーケースの活性化を可能にし、テストベンチを「増幅」
• 0-In Searchは設計サイクル早期にバグを発見し、タイム・トゥ・マーケットを改善
• 0-Inツールは設計のテープアウトに向けた高い信頼性を提供