はじめに

今日の設計の多くには複数の非同期クロックが含まれており、非同期クロックドメイン間で信号を載せ替える際に機能的なエラーとなる可能性があることを忘れてはならない。1つの非同期クロックドメインからの信号は、非同期であるので、どのようなタイミングで信号が変化するかが特定できない。異なる非同期クロックドメインの送信先レジスタによるサンプリング時にセットアップ／ホールドタイミング要件に違反することが原因である。このタイミング要件の違反により送信先レジスタがメタステーブルとなり、予測不能な値に落着くことで機能エラーを引き起こす可能性がある。クロックドメインクロッシング（ CDC ）検証は設計検証プロジェクトの重要なタスクであるにも関わらず、多くの設計チームはCDC同期化の構造解析にとどまっている。

設計者はシンクロナイザを追加しメタステーブルイベントの伝播を防ごうとするが、同時に正しいCDCプロトコルを順守していることも検証しなくてはならない。プロトコルが順守されていないとCDCの構造的な同期化は正しく機能せず、データ損失やデータ破損、メタスタビリティ伝搬などの原因となる。
CDCツールにアサーションを生成させ正しいプロトコル順守をチェックすることは一般的には行われているが、アサーション生成はCDCプロトコルを検証するには十分ではない。

本稿では従来のCDCプロトコル検証方法で遭遇する困難な状態について解説し、現在の課題を克服するための完全な方法を提示する。主な課題を次に示す。

• フォーマル検証やシミュレーションを行うためのデザインとアサーションのセットアップには、多大な労力と時間を要すること
• 構造解析、フォーマル検証、シミュレーションのそれぞれの工程間の統合が欠如していること
• フォーマル検証やシミュレーションでファイヤしたアサーション違反の確認とデバッグに、かなりの労力を要すること

本稿で提示するメソドロジは、セットアップ、制約設定、静的CDC解析の結果確認をフォーマル検証やシミュレーションへと自動化することにより、工程を容易化するものである。この自動化により、手作業によるスクリプト作成を回避し、セットアップに誤った情報が混入しがちな作業を削減できる。またこのメソドロジにより構造解析結果、フォーマル検証結果、シミュレーション結果を関連付けるという重要な課題に対応することができるため、デバッグの生産性向上を図ることができる。

CDCプロトコルとは何か、なぜ必要なのか

CDCパスにおけるメタスタビリティ伝搬を防ぐには同期化の構造が必要だが、CDCエラーを回避するには構造的な対応だけでは不十分である。設計者はこの事実を見落とす可能性がある。CDCの同期化回路が正しく使用されていない場合、CDCパスでデータ損失やデータ破損が発生する可能性があり、最悪の場合はメタスタビリティが伝搬する可能性がある。CDC同期化の適切な扱いを定義するルールは、CDCプロトコルと呼ばれる。

最も単純なプロトコル例として2段DFFのシンクロナイザを考えると、RXレジスタがTXデータを確実に取得するためには、少なくともRXクロックの２サイクル間、TXデータは安定していなくてはならない。この安定プロトコルが守られない場合にはデータ損失やデータ破損を防ぐことができない。
より複雑なプロトコル例として、データマルチプレクサ（DMUX）のシンクロナイザを考えると、マルチプレクサイネーブルがアクティブで、RXレジスタがTXデータをサンプリングできる状態においてTXデータが安定していなくてはならない。このDMUXシンクロナイザのプロトコルに違反すると、正しいDMUXが構造的には実装されていてもRXレジスタがメタステーブル状態になる。

CDCプロトコルエラーは、設計サイクルの早い段階での特定と対策は重要であり、後の段階で機能障害が発生すると、やり直しの反復回数が増え、最悪の場合シリコンのリスピンとなる可能性がある。このような問題を見逃すことのないように、設計者と検証エンジニアの双方がシンクロナイザのプロトコル用アサーションを生成し、フォーマル検証のモデルチェッキングやシミュレーション技術を使ってシンクロナイザのプロトコル順守を検証する必要がある。

CDCプロトコル検証の課題

プロトコル検証はCDCエラーを回避するためには重要であるにも関わらず、多くのプロジェクトチームでは展開するには課題が多岐に及ぶためプロトコル検証を採用していない。その一般的な課題には、プロトコル検証のセットアップ、制約のセットアップ、それにプロトコル違反／順守の確認、デバッグの難しさなどがある。

プロトコルのアサーション生成と検証のセットアップ

CDC構造解析ではCDCの同期化構造を識別し、CDCユーティリティがCDCシンクロナイザ用のプロトコルアサーションを自動生成する。CDCユーティリティは自動生成したプロトコルアサーションをインスタンス化し、それをTXレジスタ、RXレジスタ、TXクロック、RXクロック、TXリセット、RXリセットに接続する。

CDCプロトコルのアサーションが生成された後、設計者がこのアサーションをフォーマル検証やシミュレーション環境に組込むことは困難かも知れない。シミュレーションやフォーマル解析を実行するには、コンパイルにおける指示指定や検証ツール内で実行するコマンドスクリプトが必要となる。クロック周波数の情報はSDCやCDC制約から得られるが、この情報はCDCシンクロナイザ構造に対するデータ安定性プロトコル要件を指定する上で欠かせない。

SystemVerilog Assertionsとそれをバインドするbindファイルはフォーマル検証やシミュレーション環境に取込まなくてはならない。フォーマル解析に不慣れな設計者にとって、フォーマル検証のコンパイルや解析実行のスクリプトを生成することは困難である。複雑なシミュレーション環境では、プロトコルのアサーションをシミュレーシ ョンのリグレッション環境に組込むことも容易ではないだろう。

フォーマル検証用制約の生成

フォーマル環境では、設計者が設計のコンフィギュレーション情報、クロック情報、入力ポート情報などを含む制約をセットアップする必要がある。コンフィギュレーション情報は、コンフィギュレーション用のポートやレジスタへの定数指定である。クロック情報は、設計クロックの仕様とクロック周波数を指定する。入力ポート情報では、プ ライマリ入力ポートの仕様と関連するクロックドメイン情報を指定する。

CDCプロトコルアサーションのデバッグ

従来のCDCプロトコル検証手法では、プロトコル検証のレビューとデバッグはCDCの構造解析から分離されている。設計者はシミュレーションやフォーマル解析環境でプロトコルアサーション違反を、CDC同期化構造に対して関連付けることは容易ではない。構造解析とプロトコル検証の間に相関関係がないため、設計者によるプロトコル検証結果のレビューとデバッグには多くの時間／労力が費やされることになる。

CDCプロトコル検証メソドロジの提唱

本稿では従来のプロトコル検証方法に見られる一般的な課題を解決するだけでなく、プロトコル検証の結果改善をもたらすフォーマル検証のモデルチェッキングとシミュレーション技術を活用したメソドロジを提示する。そのフローを図1に示す。

図1 プロトコル検証フロー

このメソドロジには以下のワークフローがある。

1静的CDC構造解析
デザインに対して静的なCDC構造解析を実行し、関連するすべてのCDCパスが適切なシンクロナイザにより同期化されていることを確認する。さらに、プロトコルアサーションを自動的に生成し、フォーマル検証の制約を生成し、正式な検証制約を生成し、フォーマル検証とシミュレーションのセットアップ用ファイルを生成する。

• プロトコルアサーション自動生成：デザイン内の各シンクロナイザのプロトコルに対するアサーションを生成する。静的なCDC構造解析に基づき、CDCプロトコルの自動生成ユーティリティが各CDCシンクロナイザのプロトコルアサーションを生成する。プロトコルアサーションは、シンクロナイザとその接続タイプに応じて生成される。（図2）
  

  図 2. CDC プロトコルアサーションのインスタンス化

• フォーマル検証用制約の自動生成：CDC構造解析からフォーマル検証モデルチェッキング用の制約を生成する。CDCプロトコルの自動生成ユーティリティは、定数、安定状態、グレイコード信号などのCDC情報をSVAのassumeへと変換し、これはフォーマル検証に適用される。さらに入力ポート、出力ポートのクロックドメイン情報もフォーマル検証の制約へと変換され、フォーマル検証における反証例の提示における精度を向上させる。
• フォーマル検証とシミュレーションの自動セットアップ：フォーマル検証とシミュレーションを実行するためのセットアップとスクリプトを生成する。CDCプロトコルの自動生成ユーティリティは、フォーマル検証モデルチェッキング実行スクリプトを生成する。このユーティリティは、既存のシミュレーション環境に追加するシミュレーション引数ファイルも生成するため、設計者であってもプロトコルアサーションを容易に追加できるため、複数のアサーションを手動で追加しモジュールファイルをバインドする必要がない。

2フォーマル解析
フォーマルモデルチェックを実行し、自動生成されたフォーマル検証セットアップとスクリプトを用いて、自動生成されたシンクロナイザのプロトコルアサーションを検証する。CDCプロトコル自動生成ユーティリティは、フォーマル検証用のコンパイル、実行スクリプトを生成する。自動化されたフォーマル検証のセットアップにより、フォーマル解析に向けたセットアップを行う労力が大幅に削減される。また手作業 によるセットアップとは異なり、不完全、不正確なセットアップに起因する問題、それに伴うデバッグ作業労力を回避することもできる。フォーマル解析の実行に関して設計者が行うことは、単にmakefileを実行する（”make all”）だけである。

3シミュレーション
自動生成されたセットアップを既存のシミュレーション環境に追加してシミュレーションを実行し、フォーマル検証でプルーフされなかったプロトコルアサーションを検証する。CDCプロトコルの自動生成ユーティリティは、コンパイルとシミュレーション用引数ファイルを生成する。

フォーマル解析中に、フォーマル解析用スクリプトはシミュレーションセットアップ情報を自動的に更新し、シミュレーションで検証対象となるアサーションのリストから証明済のアサーションを削除する。フォーマル検証が設計制約なしで実行された場合、フォーマル検証で証明されたプロトコルアサーションは、対象となるCDC同期化構造について絶対にプロトコル違反が発生しないことを示す。この証明は、同期化構造がデータ損失、データ破損、メタステーブル伝播に対して安全であることを意味する。シミュレーションの対象アサーションからフォーマル証明されたアサーションを削除することは、シミュレーション実行時間の短縮につながり、同時にシミュレーションで違反することのないアサーションのシミュレーション結果を確認するという設計者の労力が削減される。

4CDCプロトコル検証結果の確認とデバッグ
集約されたCDC構造解析結果、フォーマル検証結果、シミュレーション結果を確認する。複数の異なる検証技術の相互関係により、設計者はプロトコルエラーをより速く、容易にデバッグし改修することができる。またこの相互関係により、設計者はプロトコルエラーに関するCDCの構造を特定し、プロトコルエラーの原因を素早く把握し診断することができる。この手法によりバグを正しく解析することができるため、CDCシンクロナイザのプロトコルエラーの見落しや誤った解析の危険 性がなくなる。

実設計への適用事例

このCDCプロトコル検証メソドロジをいくつかの実設計に適用した。現実の設計にメソドロジ展開をすることで、このメソドロジが設計者、検証エンジニアの労力を大幅に削減し、速いクロージャを実現したことを示すエビデンスが得られた。

従来のプロトコル検証方法では、プロトコルアサーションは最初にフォーマル検証で確認される。クロック、リセット、定数、入力ポート制約などの設計設定と制約は、静的CDC解析環境の情報を参考にフォーマル制約へと手作業で書換える。この作業には労力とフォーマル検証の専門知識を要する。フォーマル検証のツール環境のセットアップが完了すると、検証が実行され、違反するアサーションに対して反証例が生成される。

本稿で提示しているメソドロジでも、同様に最初のステップは、フォーマル検証環境でのプロトコルアサーション検証である。フォーマル解析から設計コンフィギュレーションと設計制約が、本メソドロジを使用して自動生成される。この自動生成されたセットアップは確認後、設計とアサーションのフォーマル解析を実行するために使用さ れる。セットアップの自動化により、CDCからフォーマル検証にセットアップを移植するために、従来のアプローチで必要とされていた手動によるセットアップ作業とフォーマル検証の専門知識は必要とされない。

今回の事例におけるフォーマル検証結果には、CDCプロトコルアサーションのプルーフ、ファイヤ、インコンクルーシブ（結論付けられないこと）などの結果が含まれていた。自動生成されたフォーマル検証のセットアップには設計制約が含まれていなかったため、ファイヤは非制約状態で発生したフォーマルのアサーション違反となる。 これは多くの場合、イリーガルなスティミュラスセットによる反証例である。フォーマル検証のモデルチェッキングに関する経験を持たない設計者にとって、ファイヤしたアサーションやインコンクルーシブとなったアサーションのデバッグは困難である。そこでこのような困難なケースをデバッグする代わりに、これらアサーションをシミュレーションへとプロモートする。参考までに従来の方法では、プルーフ済みのプロトコルアサーションはシミュレーション環境で再検証されてしまうか、もしくはシミュレーションセットアップから手動で削除する必要がある。

本稿で提示するメソドロジでは、フォーマル解析でプルーフされていないアサーションのみがシミュレーションで検証される。プルーフ済みアサーションは、シミュレーションセットアップから自動削除される。また自動生成されたシミュレーション引数のファイルは、既存シミュレーション環境に追加される。シミュレーションにおけるアサーシ ョンのファイヤは、CDCシンクロナイザのプロトコル違反であることを示しており、対象となるCDCパスでのデータ損失、データ破損、メタスタビリティ伝播をもたらす。設計者は、シミュレーションでファイヤをデバッグし、CDCロジックを修正してシンクロナイザのプロトコルに準拠させる必要がある。フォーマル検証でプルーフされなかっ たアサーションに対してのみシミュレーションを実行したため、デバッグの労力と時間は大幅に削減された。

以下の表1、表2、表3、表4は、100万ゲートから3000万ゲートまでの実設計における従来の方法と本稿で提示しているメソドロジを比較するためにフォーマル検証、シミュレーションごとにまとめたものである。

従来手法 － フォーマル検証によるCDCプロトコル検証
デザイン	セットアップに 要した時間	アサーション			実行時間	フォーマル カバレッジ*
		合計	フェイル	プルーフ
A	1週間と3日	170	79	91	24秒	100%
B	2週間と2日	800	304	437	5時間	92.6%
C	5週間と4日	8552	5673	877	7時間	76.6%

表1. 従来のプロトコル検証方法を使用した結果 （フォーマル検証）

 

従来手法 － シミュレーションによるCDCプロトコル検証
デザイン	セットアップに 要した時間	アサーション		実行時間	シミュレーション カバレッジ**
		合計	フェイル
A	10分	170	14	20分	91.7%
B	17分	800	83	35分	88.3%
C	30分	8552	127	1時間	79.4%

表2 従来のプロトコル検証方法を使用した結果 （シミュレーション）

* フォーマルカバレッジ＝（（フェイル数＋プルーフ数 )／合計アサーション数 ) ＊100
** シミュレーションカバレッジ＝（（フェイル数＋カバー数）／合計アサーション数 ) ＊100

 

本稿提示メソドロジ － フォーマル検証によるCDCプロトコル検証
デザイン	セットアップに 要した時間	アサーション			実行時間	フォーマル カバレッジ*
		合計	フェイル	プルーフ
A	2日	170	32	138	55秒	100%
B	5日	800	119	654	6時間	92.6%
C	1週間	8552	1825	4907	10時間	78.7%

表3. 本稿提示メソドロジをプロトコル検証に適用した結果 （フォーマル検証)

 

本稿提示メソドロジ － シミュレーションによるCDCプロトコル検証
デザイン	セットアップに 要した時間	アサーション		実行時間	シミュレーション カバレッジ**
		合計	フェイル
A	1分	32	6	20分	97.31%
B	1分	146	34	35分	97.06%
C	5分	3645	76	1時間	87.47%

表4 稿提示メソドロジをプロトコル検証に適用した結果 （シミュレーション)

* フォーマルカバレッジ＝（（フェイル数＋プルーフ数 )／合計アサーション数 ) ＊100
** シミュレーションカバレッジ＝（（フェイル数＋カバー数+プルーフ数 ）／合計アサーション数 ) ＊100

この結果から以下の改善がなされたことがわかる。

• フォーマル検証のセットアップ時間の大幅な短縮
  セットアップの自動生成により、セットアップ時間が短縮された。セットアップ時間の短縮だけでなく、セットアップの不完全さや誤りが含まれる場合に発生するデバッグの反復を回避することができ、その時間と労力も削減されている。セットアップ時間は3倍〜5倍短縮された。
• シミュレーションのセットアップ時間の短縮
  セットアップの自動生成により、セットアップ時間が短縮された。セットアップ時間の短縮だけでなく、セットアップの不完全さや誤りが含まれる場合に発生するデバッグの反復を回避することができ、その時間と労力も削減されている。設計例Cの場合、セットアップ時間は6倍〜17倍も短縮された。
• フォーマル解析における擬似ファイヤの削減
  セットアップの自動生成とCDC設計制約のフォーマル解析へのインポートにより、フォーマル解析のセットアップにおける誤りが減少し、擬似ファイヤの減少につながった。フォーマルでのアサーションファイヤ率は59％〜68％削減された。
• フォーマルカバレッジの向上
  フォーマルセットアップと制約が改善されたことで、インコンクルーシブとなるアサーションが減少したほか、プルーフとファイアリングといった結論づけることが可能な状態へと改善された。
• シミュレーションカバレッジの向上
  プルーフ済みのアサーションをシミュレーション対象から削除することで、ファイヤしカバーされたアサーションの割合が高くなった。本稿で提示されているメソドロジでは、フォーマル検証でプルーフされたアサーションはシミュレーションされず、プルーフ済みのアサーションはカバーされたものと見なしている。これは従来手法と本稿提示のメソドロジとの比較で一貫性を持たせる上で必要である。
• シミュレーション検証の時間と労力の削減
  フォーマル検証でプルーフ済みアサーションが除外されたことにより、シミュレーション環境に渡されるアサーションの数が減り、シミュレーションでのアサーション確認作業が削減された。CDC構造解析、フォーマル 検証、シミュレーション結果に相互関係を持たせることで、デバッグ生産性が向上し、プロトコルエラーと関連するCDCパスの関連付けが容易になった。なお、この実設計を用いたケーススタディでは、シミュレーション結果そのものの確認とデバッグの時間や労力は測定していない。
• シミュレーションにおける擬似ファイヤのデバッグ労力の削減
  本稿提示のメソドロジではシミュレーションにおけるアサーションファイヤの数が削減された。このメソドロジではCDC制約をフォーマル解析で使用することにより、データ安定性やグレイコード化の制約が適用され、より多くのアサーションがプルーフされた。このようなプルーフ済みの制約はシミュレーション実行時には適用されないため、アサーションの擬似ファイヤを回避することができた。従って設計におけるこのようなケースでは、アサーションの擬似ファイヤに費やされる時間と労力は測定されていない。

今回の実設計において、以下は影響を受けなかった。

• シミュレーション実行時間の改善は最小限
  フォーマル検証によりプルーフされたアサーションをシミュレーション対象から除外したことにより、シミュレーションで評価されるアサーションの数は減少したものの、シミュレーション実行時間を大幅に短縮することはなかった。

結論

本稿で提示されたCDCプロトコル検証メソドロジは、CDCシンクロナイザのプロトコルの設計と検証を体系的かつ反復可能なソリューションである。セットアッププロセスを自動化したことにより、セットアップにおける誤りの混入やそのデバッグの反復工数が削減される。CDC制約をフォーマル検証のモデルチェッキング制約へと自動変換することで、フォーマル解析の精度が向上し、擬似ファイアリングが減少する。最後に、CDC構造解析、フォーマル検証、シミュレーションのそれぞれの結果を統合化することでデバッグが容易化され、設計者はプロトコル違反をより速く、少ない労力でデバッグし改修することができる。

参考文献

[1] Mark Litterick, “Pragmatic Simulation-Based Verification of Clock Domain Crossing Signals and Jitter using System Verilog Assertions”, Verilab.

[2] William K. Lam, “Hardware Design Verification: Simulation and Formal Method-Based Approaches”, Prentice Hall, Mar 3, 2005.

[3] Sulabh K. Khare, Ashish Hari, “Systematic Speedup Techniques for Functional CDC Verification Closure”, Mentor Graphics, advanced verification white paper.

[4] Ping Yeung, “Five Steps to Quality CDC Verification,” Mentor Graphics, advanced verification white paper.

[5] Sukriti Bisht, Sulabh K. Khare, Ashish Hari, “A Systematic Take on Addressing Dynamic CDC Verification Challenges”, DVCon US, 2019.

「Design and Verification Landscape」技術情報メールニュース

PALTEKでは本ブログ「Design and Verification Landscape」シリーズの技術情報をメールで年に3-4回発信しています。
ご登録いただいた方には、最新の情報をメールニュースとしてお届けします。
ご希望の方はこちらのフォームよりご登録ください。

※競合製品取り扱い企業様の申込については、お断りする場合がありますので予めご了承ください。

関連ウェビナーのご案内

このブログのシリーズ一覧は下記になります。是非あわせてお読みください。