HOT TOPIX
ポストシリコンデバッグにおけるフォーマル技術の適用 Jasper Design Automation
ポストシリコンデバッグにおけるフォーマル技術の適用
by Jamil R. Mazzawi, Senior Applications Engineer, Jasper Design Automation, Pearl Lee, Senior Field Applications Engineer, Jasper Design Automation, and Lawrence Loh, Vice President of Worldwide Applications Engineering, Jasper Design Automation
今日の高性能チップの検証では、最良のメソドロジーとツールが求められており、アーキテクチャ解析からポストシリコンデバッグまで、高い能力のフォーマル検証技術がデザインフローの至るところで使われています。ここでは最後のエリア、ポストシリコンについて見ていきましょう。これはデザインの正しさを確認するプロセスでフォーマルを採用してこなかった設計検証チームにも価値の高い使い方です。
この記事の中で提示されたケーススタディが立証するように、バグの発見、修正、検証というフォーマルの使い方は、ポストシリコンラボに絶大なアドバンテージを与えます。
ポストシリコンバグに関連するコストを理解するには、広く知れ渡っている因果関係を考えてください。モデルチェックでバグを発見できるとさほどコストはかかりませんが、コンポーネントで見つかるとその10倍、システムレベルだと更に10倍、そして消費者の元で不具合が見つかった場合には、起こりうる最悪の結果として更に10倍のコストがかかってしまいます。
ポストシリコンのデバッグは大変ストレスがたまる作業です。チップが動作せず納期が迫ってきた時、あなたはどうしますか。納期に間に合わなければ、会社やプロジェクトメンバーに損害を与えてしまいます。マネージャはポストシリコンバグを迅速に取り除くことを期待しており、状況をアップデートするために設計・デバッグチームを頻繁にヒアリングするでしょう。
バグを再現するために、ランダムシミュレーションやエミュレーションに労力が割かれますが、これら従来のアプローチではしばしば労多くしてバグの根本的な原因になかなか辿り着かないことがあります。フォーマル検証はこのような状況で救世主になることが確認されています。他のアプローチでうまくいかなかった時でも、バグの原因を見つけ出し、正しく修復されていることを立証します。
この記事では、ポストシリコンにおいて機能バグを根絶するためにフォーマル適用の基本と、このテクニックをどう適用すればよいか、成功した3つのプロジェクトの例で紹介します。
バグの発生
ポストシリコンのデバッグチームがテストでチップの問題を発見するとき、最初は非常に抽象的であり、よく分かりません。ハングアップしているのか、応答しないのか、またはパケット欠落や、誤出力なのか、など。最初の第一歩は、何がチップ内で起こっているかを理解することです。
今日では多くのチップにオンチップトレースを抽出する機能が備わっています。例えば、あるイベントが識別された時にチップをフリーズする制御、選択した信号のグループをマルチプレクスして外部ピンに出力するオンチップロジックアナライザ、フリーズイベント前のNサイクル間のある信号の値を、チップの内部メモリーにセーブする機能、あるいは、フロップの状態をスキャンアウトするスキャンチェイン等です。問題が検出される前後の特定の数の信号のキャプチャを繰り返して、デバッグチームはフェイルした波形を抽出できます。
シミュレーションでバグの原因をつきとめる試み
次のステップはポストシリコンバグを特定し、根本的な原因をつきとめることです。この時点で、チップで起こった違反動作はトレースで確認できますが、トレースは最後のNサイクルを表しており、この状態がどのような経緯を辿ったかは分かりません。通常は限られた数の信号だけがトレースされ、問題を起こす信号を正しく選ぶことは困難です。
図１ バグハンティング
図1はラボにおける窮地を表現しています。フェイルしたシナリオの最後の数サイクルは観測できますが、問題の原因はどのように見つけることができるでしょうか。設計者は、バグがどのブロックに存在しているのかをどう知るのでしょうか。
元来、シミュレーションチームによってバグが特定されますが、彼等はシミュレーションでバグに至る経路を発見できるのでしょうか。バグがどこで起きているか明らかではありませんが、ブロックDが異常動作していることは分かります。ある種のトラフィックが注入されるとき（例えば、バスXにおけるリードトランザクション）、ラボで3-4時間実行した後にバグは起こります。
実のところ、シミュレーションでバグの原因を探し出すのは、ほとんどの場合「不可能な任務」と言えるでしょう。ランダムトラフィックを用いてバグにヒットするのにリアルタイムで4時間かかると、シミュレーションが1,000倍遅い場合、再現するのに何時間かかるでしょうか。4,000時間のシミュレーション、それを1週間で完了できますか。その間、マネージャは一日おきにバグの原因を聞いてくるでしょう。
フォーマルによる救済
・数百数千のブロックを持つ大きなデザインをフォーマル検証で実行でき、エンドツーエンドでフォーマル検証を行うこと
のできる高い能力
・Jasper Formal ScoreboardやProof Acceleratorsで実現しているようなデザインを横断するデータの転送を完全に検証
できる能力。Formal Scoreboardを使うと、複数の入出力ポートでバイトイネーブルに依存する転送やバス幅の変換、
シリパラ変換のように多くの異なったタイプのデータ転送の検証が可能になります。Proof Acceleratorsは、FIFOやメモ
リなど一般的なブロックの検証において、パフォーマンスを向上させ、検証の収束を加速させます。
・簡単なデバッグのための視覚化機能：ラボにマッチしたシナリオを簡単に生成する能力
・非同期クロックのハンドリング
ポストシリコンデバッグで、フォーマル検証技術を利用する重要な特徴のひとつは、迅速にバグを発見できることです。通常、フォーマルで反例を見つけることは、同じプロパティで完全証明するよりはるかに速く、このテクニックを使うとバグハンティングが非常にやり易くなります。フォーマル検証ツールであれば、ユーザは特定のサイクルで状態を止めておくことができ、そのポイントから解析を継続できますので、一度にすべてのデザインを解析する必要はありません。
フォーマルを使ったバグ探しは、プレシリコンのフォーマル検証フローとほとんど同じプロセスですが、いくつか大きな相違点があります。
・1つの特定バグとシナリオのための探索
・完全証明や100％のカバレッジを期待しない
・違反した動作につながるシナリオだけを探す
・プロセスを簡素化するために過剰な制約を容認できること（例えば、バグがリードトランザクションだけで起こるため、ラ
イトトランザクションを許可しないなど）
典型的な例では、チームはすでに何かを知っている状態からスタートします。違反のシナリオを表す波形がすでにあり、リードトランザクションが他のリードトランザクションに追随される時に問題が起こることが分かっている場合、やるべきことは、違反するシナリオではなく、プロパティの状態を定義することだけです。
そのプロセスにおいて、通常のフォーマル検証実行のように制約を加えることは必要ありません。それによってプロセスを簡素化して、ショートカットすることができます。 例えば、次のような過制約はOKです。バグがリードトランザクションで起き、ライトトランザクションでは起こらないことが分かっているなら「ライトトランザクションを許可しない」という制約を加えることです。
プロパティの証明はフォーマルエンジンを走らせるだけで、違反シナリオからフェイルしたバックトレース波形を生成します。もちろん、バグ発見後も設計者はRTLに戻って修正を行い、修正後のシナリオが違反しないことを確認するために同じプロパティで再びフォーマル検証を実行します。このプロセスを視覚化する能力はJASPERツールの特徴であり、テストベンチなしで自動的に波形を生成することで、"what-if"の問いに対する解を示し、視覚的に機能を確認できます。
ケーススタディ
ポストシリコンのデバッグにおけるフォーマルの力を説明するために、デバッグにフォーマル検証技術を使用して大きな課題を克服したチームの例を３つ紹介しましょう。
IPのバグによる潜在的な被害
最初にバスプロトコル（図2）に違反するメモリーコントローラのデバッグについて説明します。 プロセッサと複数の周辺回路から構成されるこの大規模SoCは、ある条件でハングアップするという粗悪な動作のため、メーカーによりリコールされました。
図２：バスプロトコルに違反したメモリーコントローラのシステムブロックダイアグラム
ポストシリコンのデバッグチームは、ラボからの僅かな情報でシミュレーションをスタートさせ、メモリーコントローラでリードトランザクションが実行されたときにチップがハングアップすることが分かりました。
バグの原因に辿り着くまで３ヶ月以上かかってしまいましたが、原因がメモリーコントローラにあることが特定できました。非常に特殊なパターンでラッパーにデータを送りバグを活性化させると、バスプロトコル（図3）の違反を引き起こしたのです。システム内の異なるイベントで大変稀なタイミングに照準を当てるのは難しく、シミュレーションで検出するのは極めて困難なため、シリコンバグとして見逃してしまいました。
図３：シミュレーションだけではバグの原因を探すのは困難です
バグの原因を追いかけ、シミュレーションに３ヶ月かかったことはチップメーカー、顧客、およびIPプロバイダにとって、明らかに大きな問題でした。 特にそのチップが入った製品がすでにエンドカスタマーに届いており、結果としてリコールすることになったからです。
シミュレーションよりも早くバグの原因を突き止められるかどうかを調べるために、フォーマルが利用されました。フォーマルエンジニアは、シミュレーションチームがスタートした時とまったく同じ情報が提供されました。バグはちょうど2.5週間で発見されましたが、その多くが検証環境の構築に費やされました。実際、セットアップが完了しプロパティを検証すると、反例は1分以内で見つかりました。シミュレーションがランダムパターンでバグにヒットするのに何週間もかかったのと比べてください。
フォーマルはフェイルの原因を迅速に生成するために、フェイルしたトレースから遡って数学的に解析しますので、現実的で期待通りの結果を得ることができます。シミュレーションでは、エンジニアはバグがいつおこるのかを検出するチェッカーを作ったり、もっとバグを引き出すためにランダムパターンを増やし、それがいつかバグにヒットすることを期待しています。
その後、修正されたRTLをフォーマルで確認したところ、シミュレーションが逃していたバグを２つ発見し、メーカーは再びリスピンするのを回避できました。
ポストシリコンパートナーシップ
2番目のケースでは、フォーマルチームとポストシリコンラボのエンジニアがどのように協力して動いたかについて説明します。かつてラボでバグが発見された際、フォーマルに救済が求められました。
チップに含まれる一連の4ブロックにバグが発生していました。各ブロックは、入力データを処理して次のブロックに送ります。チップには、チップ出力で観測するために、一群の信号を探し出せるビルドイン・ロジックアナライザが内蔵されていました。しかしながら、ラボチームにとっては、どの信号を調べたらよいかを選択するのがいつも課題でした。どの信号が問題を表すかを知ることが非常に難しいからです。フェイルした波形はチップの出力、またはブロックDの出力で検出されたので、ラボチームは焦点をブロックDに置き、ロジックアナライザでこのブロックを調べていました。
フォーマルチームは、Bの入力からDの出力までのエンドツーエンドのプロパティ（図4）を書きました。このケースにおいて、ブロックAは関連していませんでした。プロパティはポストシリコンラボで抽出された違反トレースに基づいて書かれました。そしてバグを引き起こした入力だけを許すように他の信号は制約で除外しました。
図４：エンドツーエンドのプロパティの記述
3ブロックの規模が原因でプロパティが収束しなかったため、より小さなプロパティに分ける必要があり、プロパティはブロックDの入力から出力まで記述されました。このプロパティには、D（図5）の入力に対する正しいふるまいを定義する制約が必要でしたが、このプロパティはあっという間に立証することができました。これは、Dの入力が制約に従い動作するなら、ブロックDは違反動作を決して起こさないことを意味します。
図５：制約を加えた入力でBlockDを検証
ブロックDにはバグはないことはが明らかになりましたので、 次にポストシリコンデバッグチームはブロックCに焦点を移し、ロジックアナライザがブロックCから信号を得るように設定しました。
同時にフォーマルチームもブロックCについて検証を行いました。Dの入力で制約だったものはCの出力のアサートに変換され、そしてブロックCの入力に対して正しい入力になるように新しい制約が記述されました。
これらのプロパティは数分以内に立証されました。ブロックCは完全に正しいというフォーマルチームからの回答に基づき、ラボはブロックBに焦点を移しました。ロジックアナライザは、ブロックBの信号に設定され、これによって、デバッグチームはブロックBから抽出されたトレースからバグを発見することができました。
本件は2つのチームがどう協力し合ったかを示す良い例であり、早期にバグを発見するために各々の強みを生かしつつ、もう一方のチームから得た情報を共有したケースです。
シミュレーション/エミュレーションで見つけられなかったバグをフォーマルが発見
最後に、検証戦略にフォーマルを活用していなかった会社にとって、フォーマルを利用したポストシリコンデバッグが高く評価されたケースを説明します。
元々、検証はシミュレーションとエミュレーションだけで、フォーマルを使っていなかったのですが、１つのバグがポストシリコンラボで見つかりました。シミュレーションやエミュレーションでは難しいコーナーケースやサイクルに依存する問題によってバグを見逃してしまったのです。修正の正しさを確認するために、シミュレーションとエミュレーションで数週間かけて確認した後、ECOが実施されました。万一に備えて、フォーマルで再チェックしたところ、わずか2?3時間で修正に欠陥があることが分かりました。フォーマルツールによって、バグを引き起こす別のシナリオが発見され、修正がすべてのケースをカバーしていないことが分かりました。2回目の修正をフォーマルで検査してみると、違った部分のロジックでも同じバグを引き起こすことが発見され、3回目の修正でフォーマルのテストをパスしました。
この経験から分かることは、フォーマルを使った検査が複数回のリスピンを回避し、その会社を救ったことです。なぜなら彼らのシミュレーション環境では、修正した後の検証でバグをカバーしていなかったのです。彼らは現在、ブロックレベルのテストベンチに頼らず、フォーマルを使いながら設計を行っています。
まとめ
ポストシリコンデバッグのために、高価なハードウェアだけ導入しても不完全なソリューションです。フォーマルは、遅延（すなわち今日の競争市場で一度でも欠陥を出すこと）を許されないユーザーに感銘深い成果をもたらしています。ポストシリコンデバッグのプロセスにおいて、曖昧さは壊滅的な影響をもたらします。検証には、不完全なテストベンチや不適切なプロパティ仕様、ソフトウェアのバグなどの不明確な要素があります。それら全てにバグの可能性がありますので、早期にバグのもとを取り除いておくことがバグの原因を特定するキーとなります。ポストシリコンデバッグにフォーマル検証を適用するメリットは、この不明確さを取り除くことです。高い能力を持つフォーマルの徹底的な動作解析によって、特定の検証コンポーネントが想定していない動作の元であるかどうか確実な解をもたらしてくれます。
本当のソリューションは、バグを早期に発見するためにデザインフローの一部としてフォーマルを採用することですが、従来のポストシリコンメソドロジで製造されたシリコンがバグなしであることを保障することにも使用できます。ポストシリコンラボの能力とフォーマル検証を組み合わせれば、期待通りの成果を生み出します。先に引用された3つのケーススタディで証明されたように、フォーマルの網羅性は特定ブロックのバグを根絶し、リスピンを回避できます。
ジャスパー社について
Jasper Design Automation, Inc.は、最新のフォーマル技術をベースに、半導体の設計、検証、デザインの再利用に向け、業界をリードするEDAソフトウェアのソリューションを提供しています。カスタマーは、ワイヤレス、コンシューマ、コンピューティング、ネットワークなどの分野で世界をリードするトップ企業で、200を超えるチップ開発で成功しています。ジャスパー社の本社は、米国カリフォルニア州マウンテ ンビューにあり、他に北米、南米、ヨーロッパ、日本 に支社や代理店があります。
開発のリスクを減らし、設計、検証、再利用などの生産性を引き上げ、Time to Marketを加速し、ターゲットとするROIを得るため、是非ジャスパー社のホームページ http://www.jasper-da.com/ をご覧下さい。
問合せ先
ＣｙｂｅｒＴｅｃ株式会社
神奈川県横浜市都筑区茅ヶ崎中央50番17号 CM Port5階
TEL: 045-945-3690 FAX: 045-945-3680
URL: http://www.cyber-tec.co.jp/
｜ページの先頭へ｜