非同期デザインへのフォーマル検証適用方法 Jasper Design Automation
非同期デザインへのフォーマル検証適用方法
Jasper Design Automation
1.イントロダクション
昨今デザインが著しく複雑になるにつれ、非同期デザインの検証が、現在のSoCにおける大きな課題の一つとなっています。機能シミュレーション、リントチェックや従来の検証手法では正確かつ徹底した非同期デザインの検証には不十分であることが分かっています。このような従来の手法は、アーキテクチャー仕様を正確に理解し、対象デザインで発生しうるすべての複雑なシナリオを検証することに関し、設計者や検証者の力に依存しているため、手動で手違いが発生しがちとなり、不完全です。
従来手法での検証が困難な非同期デザインの課題として以下のようなものが挙げられます。任意の値をとる非同期クロックドメインクロッシング（CDC）のモデリング、位相・周波数ジッタの正確なモデリング、データパス検証、複雑なクロック構成のローパワーデザインなどです。もしこれらの複雑で特定することが難しい非同期デザインの問題が、早期に検出・検証されなければ、リスピンを引き起こし莫大なコストが発生する可能性があります。
フォーマル検証は、テストベンチや入力ベクタを作成することなく、あらゆる複雑なシナリオを網羅的に検証できる力によって、SoCデザインにおける困難な問題を検証するための理想的なソリューションの一つであることが明らかになっています。フォーマルでは、フォーマルエンジンが全ての起こりうるシナリオを自動的に発生させ、信頼性を高めますので、設計者や検証者は起こりうるシナリオを考え出すことに時間を費やす必要がなくなります。複雑なデザインのため考慮することが困難だったり、見逃してしまい、検証していないシナリオがある、という不確定な状態をフォーマル検証によって、取り除きます。
2非同期デザイン例
2.1 PHY・デジアナ混在ブロック
PHYブロックはアナログラインや非同期入力から発生するノイズといった、予測不能な入力を扱います。このようなノイズは時にデッドロックの原因となることもあります。以下にPHY・デジアナ混在ブロックの検証に関連する課題を挙げます。
■ パケット転送に関する検証。例：
・CRCエラー発生時のパケット破棄
・複数の出力ポートへパケットを複製するマルチキャストパケットなどパケット複製
・優先度の高いパケットを低いパケットより先に出力順序を変えるパケットリオーダー
■ 非対称な入出力の検証。例：
・異なるデータ・アドレスバス幅
・入力パケットを出力時に複数パケットに分解
・複数の入力パケットを連結して１つもしくはより少ないパケット数で出力
・入出力間で異なるクロックドメインを使用
・標準プロトコル、等
■ 入出力間の遅延の検証。例：
・可変遅延と複数の固定遅延の設定が混在
2.2 複雑なクロック構成を含むローパワーデザイン
現在、デザイン内のパワードメイン数やパワーモードは着々と増え続けています。設計者はローパワーデザインの徹底した検証を求められ、その検証内容はパワーアップ・ダウンシーケンス、適切な状態保持・復帰、状態変化時のデータの信頼性などです。この徹底した検証によりリスピンの原因となる構造的な欠陥や電力仕様違反、時にはリスピンも必要とするような時間的な欠陥を防ぎます。
ローパワーアーキテクチャーでは、クロックツリーを利用してダイナミックにパワーを大きく変化させるため、クロックツリーの最適化やクロックゲーティングはよく用いられる技術であり、非同期のクロックドメインクロッシング（CDC）を伴うこともよくあります。周波数ジッタや位相ジッタのタイミングが複雑なため、一般的にシミュレーションは、機能違反を発見するのに頼りに出来ません。クロック周波数を変化させることでCDCに潜む問題が判明します。それに対してパワーゲーティングはドライブされない信号線や保持した状態が不正に消失する問題を起こします。
誤ったクロックゲーティングの実装例としては次のようなものがあります。消費電力を抑える仕組みを実装しようとした際、不正なデータが発生したために計算中のパイプラインへのクロック供給を止めてしまったとします。（下図1参照）計算結果をレジュームする前にデータがフラッシュされていなければ間違ったデータがパイプライン中に残り、機能欠陥を引き起こします。クロックジッタと位相ジッタを理解しモデリングすることにより、このような欠陥の検証が楽になります。
図1：複雑なクロック系を伴うローパワーデザイン
この例では、計算中のデータがステージ2にあるときにクロック供給を止め、ステージ2のホールドタイムを考慮せずにクロックを再供給したためにデータ破壊が発生します。
3.非同期デザイン検証における課題
通常の非同期クロックの検証に伴う大きな問題の一つとして、クロック間の位相関係が固定であることが挙げられます。しかし実世界ではその位相関係は不確定なものです。この不確定性を正しくモデリングする必要があります。例えば2つの非同期クロックをシミュレーションやフォーマル検証では同じ周波数、位相差0で扱うことがよくあります。しかしこれでは非同期デザインの検証になりません。実世界では２つのクロックドメインのエッジの関係は不確かなものです。そこで非同期検証の新たな課題としてドメイン間における不確かな関係を網羅的にモデリングすることが挙げられます。
3.1 位相ジッタ
位相ジッタや周期ジッタはあるクロック周期と理想周期の差になります。同期回路では、エラーの無い回路動作が可能な限り最短のクロック周期により制限され、回路の性能が平均クロック周期に制限されるので、この位相ジッタあるいは周期ジッタは重要になります。従って、最短のクロック周期が平均のクロック周期に近づくように同期回路は周期ジッタを最小にする必要があります。
図2：位相ジッタ
3.2 周波数ジッタ
非同期クロックはあるクロックに対して固定されたものではありません。そして周波数はクロック間で揺らぎます。周波数ジッタやサイクル間のジッタとは任意の連続した２つのクロック周期の差です。このジッタはマイクロプロセッサやRAMインタフェースで使われているクロック生成回路のタイプによっては重要な要素となります。
図3：周波数ジッタ
3.3データ消失・データ間の非干渉性
同期回路では、あるクロックドメインから別のクロックドメインへの転送時にデータが消失するのを防ぐためには、ディスティネーションドメインが確実に受け取れるように、ソースドメイン側が相手のセットアップ・ホールドを満たす十分な期間保持する必要があります。非同期クロック回路ではハンドシェークやFIFO技術がデータ消失を防ぐためによく使われます。
あるクロックドメインから別のクロックドメインへ信号が伝達される時に、信号の値が変化し、ソースとディスティネーションのクロックエッジが近くなると、メタステーブルが発生し、そのためにディスティネーション側では信号間で異なるサイクルでデータを受けとることがあります。この場合、間違った信号の組み合わせがディスティネーション側に発生する可能性があります。
非同期CDC検証における課題として非同期クロック間における位相差が全く予期できないものであること、そしてそれがメタステーブルの原因となることが挙げられます。
4現在のソリューションとその欠点
機能シミュレーションは複雑なCDC問題（例：FIFOやハンドシェークを使用した同期メカニズム）の徹底した検証には不十分であることが明らかになっています。すべての入力パターンを考慮したシナリオや、セットアップ・ホールド間のデータ変化時におけるレジスタの振る舞いの不確かさを発生させることは非常に困難だからです。
シミュレーションで網羅検証を行うのは困難です。例えばグリッチをモデリングしたとします。シミュレーションで検証対象回路に対し網羅的にグリッチを挿入してその干渉をチェックする入力パターンを作成するのは不可能です。
CDCチェッカーやリントツールでは部分的な解決に過ぎません。これらツールは何千ものワーニングを出すため、本来チェックすべきワーニングを見落とすことがよくあります。結果、CDCにおける問題は残ったままとなります。
既存のフォーマルプロパティチェックツールは通常、検証環境におけるすべてのイベントを同期としてモデリングします。つまりCDCのおけるグリッチやメタステーブルが原因となるようなバグは見逃してしまいます。
非同期CDCにおける不確かな影響をモデリングすることはとても困難です。さらにCDC上のバスの不正なエンコードによるエラー状態も見逃す可能性があります。例えば出力側のバス値がグレイエンコード（１サイクルで１ビットのみ変化するコード）でない場合、入力側ではバスの個々のビットのサンプリングタイミングにばらつきが生じることでデータの値が正しくないことが起こる可能性があります。
プッシュボタン式のCDCチェッカーでは複雑なCDC問題の検証には不十分であることが判明しています。フォーマル検証で非同期CDCの不確かな振る舞いに対する網羅検証を行う必要性が高まっています。
5. Jasperの洗練されたフォーマル検証アプローチ
5.1非同期デザインにおける動作をモデリング
洗練されたフォーマル検証ツールで非同期回路の機能の正確さを証明できます。
Proof Accelerator（PA）は実績のあるモデルで、FIFO、メモリ、データ転送コンポーネントといった様々な共通コンポーネントがあります。このモデル群により検証プロパティの記述工数がかなり減ります。
PAの一例として非同期CDC PAを紹介します。このPAでCDCの不確かな結果に対し網羅検証を行うことが可能となります。さらに検証対象デザインにおける周波数ジッタや位相ジッタをPAでモデリングすることが可能です。
5.2周波数ジッタをモデリング
周波数ジッタPAは複数のクロックドメインを持つDUTでアサーションを証明するときに周波数ジッタの影響をモデリングするために使用します。このPAを使用することで速いクロックと遅いクロックの比を固定することなく定義した範囲内の任意の比で検証することが可能となります。
5.3データの信頼性と消失に対する検証
データ転送の検証における問題は次のようなたくさんのデザインアプリケーションで存在します。
■用意された入力ベクタでのみ検証を行う
o データ破壊やパケット消失の可能性が残ったまま
■ 通常データ転送検証のシミュレーションはシステムレベルで行い、低いレベルでの入力信号の制御性が悪い
o ハイレベルなテストベンチであればあるほど、ブロックレベルの入力における特定のデータパターン生成は複雑になる。
データ転送検証の問題はCDCやメタステーブルを扱うとより大きなものとなります。スコアボードPAにはチェッカーが組み込まれており、データ転送の入出力を検証することが可能です。このPAでデータ転送検証に対応することができます。
図4：スコアボードPA
6.実際の非同期デザインの検証例
6.1ロックアップ条件を検出するリセット回路の検証
不適切なCDCによりデザインがロックアップすることがあります。ロックアップ条件を検出し、そのブロックをリセットするリセット回路がありました。リセットがスタック条件で起動するかということを検証することでリセット機構が正常に動作していること保証するためにフォーマル検証が適用されました。ある特定の状態において、リセット条件を活性化する信号が正しく動作しないというバグが見つかりました。フォーマルを使うことでこの致命的なバグはすぐに見つかりましたが、さもなければリスピンの必要があったかもしれません。
6.2リセットの復帰メカニズムを検証
リセットメカニズムの動作をチェックするためにプロパティを定義しました。この例のリセットメカニズムは前述した例とは違いました。CDCで発生したグリッチにより回路が期待されない状態になってもリセットシーケンスが正常に動作することを保証するのが検証の目的でした。
フォーマルのおかげでこの回路の問題点が見つかり、内容はある状態でクロック供給が止まり、リセットシーケンスが正常に機能しなくなるというものでした。バグが見つかり、デッドロックに陥る状況は回避されました。発見が遅れれば致命的な状況になった可能性もあります。シミュレーションではこの複雑なシナリオを見つけることはできませんでした。
フォーマル検証が、リセット状態により任意の状態にあるステートマシンがアイドル状態へ戻ることを保証するために使用されました。さらにチェックの追加として、CDCチェックを行ない、CDC の許容範囲を検証したところ、その中には不正なものがあることがわかりました。フォーマルでこのような検証が行われなければこのCDC問題は見落とされていたでしょう。
6.3 PHYにおけるクロック比とディレイモードのコンフィギュレーションの検証
2週間でPHYデザインの様々なモードを検証するため、エンジニアがシミュレーション環境の立ち上げを行っていました。環境の立ち上げはまだ終わっておらず、同ブロックにフォーマルを適用することを決定しました。フォーマル環境を2日で立ち上げ、3日目から検証をスタートしました。
図5：スコアボードと位相/周波数ジッタPA
スコアボードPAはエンドツーエンドのデータの信頼性を検証するために使用されました。アドレスとデータのビットがそのパスを通っても同じであればアドレス・データの伝搬にエラーがないことが保証されます。位相・周波数ジッタPAはあらゆる設定での往復遅延のレイテンシの検証のために使用され、それがPHYブロックにおける重要な検証事項となります。
PHYデザインには設定できるクロック比がたくさんあり、またデザインも複雑でした。リード時に出力ポートに戻ってきたデータの遅延はルート遅延に周波数ジッタが加わり一定ではありませんでした。結果として、シミュレーションで検証するには動作モードが多すぎました。ある特定の遅延モード・クロックモードで検証をしていなかったためにコーナーケースバグを見逃していました。
図6：あらゆるクロック・遅延モードの検証環境
PAによりあらゆる周波数ジッタだけでなく設定可能な複数のクロックモードも同時に網羅検証ができました。この結果、プロトコル違反はなくなり、クロックとデータパスの遅延に関する検証も迅速に進み、すべての検証タスクを2週間かからずに終えることができました。
6.4ローパワー検証：パワーマネージメントユニットとクロックゲーティングロジック
ローパワーデザインではパワーマネジメントの機能をパワーマネジメントユニット（PMU）と呼ばれる一つのブロックに集約します。PMUはパワードメイン制御関連のロジックやコントロールシグナルで構成されます。各々のパワードメインは通常異なるクロックで制御されます。
PMUでは適切なコントール信号の生成が行われているか、様々なパワーシーケンスが信頼性の高い動作モードであるか、を検証する必要があります。現在のほとんどの検証ソリューションでは検証対象の信号がアクティブになった時、信号をチェックします。この手法では、対象デザインの検証ポイントの数が多いために、長い検証サイクルを必要とします。より良いメソドロジは遅延を不確かなものとしてモデリングすることです。非同期CDC PAや周波数ジッタPAを使えば周波数・位相ジッタのモデリングが可能になります。
ローパワーデザインで一般的に使われる技術はクロックゲーティング、パワーシャットダウン（パワーゲーティング）、電圧制御です。データの信頼性を保つため適切にクロックゲーティングする必要があります。もしある対象ブロックに対しクロック供給を適切に止めることができなければ、不適切な状態の信号やグリッチが伝搬し、データ破壊を引き起こすこともあります。非同期CDC PAを使うことで各パワードメインのシャットダウン・パワーアップを制御するクロックゲーティングブロックの機能を保証することができました。
7.0結論
非同期デザインとその課題は今日の複雑なSoCでは現実のものとなっています。とくにローパワーデザインでは顕著です。機能シミュレーションやリントチェックなどの従来の検証手法では不十分であり、また非常に時間がかかってしまうことが分かっています。
非同期デザイン検証のソリューションとしてJasper社のフォーマル検証ソリューションは理想的な選択肢として挙げることができます。入力パターンやテストベンチは必要なく、あらゆる入力を考慮した網羅検証が可能です。非同期PAのようなアドバンスドフォーマルを使用すれば本稿で議論した以下の非同期問題も正確かつ広範囲に検証することが可能です。
■ 非同期デザインの不確かな振る舞いをモデリング
■ 位相・周波数ジッタをモデリング
■ データ消失・信頼性を検証
このような複雑な動作のフォーマル検証が早ければ早いほど、設計の終盤での致命的なバグの発見やリスピンの危険性が低くなります。
Jasperの洗練されたフォーマル検証は様々なデザインの検証で成果を上げています。
■ ロックアップ条件を検出するリセット回路
■ リセット復帰メカニズム
■ 様々なクロック比、ディレイモード設定可能なPHYブロック
■ パワーマネジメントユニットとクロックゲーティング回路をもつローパワーデザイン
フォーマル検証により機能シミュレーションへの依存度は減り、生産性が最大となり、また、網羅検証により信頼性が増し、プロジェクト全体のリスクを軽減します。
Jasper Design Automation社について
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/