米国EDAベンチャーのReal Intent社は、先月末にパシフィコ横浜で行われたEDS Fairにおいて、論理設計の検証作業を楽にするツールAscentと、複数のクロックが引き起こすCDC（clock domain crossing）問題を解決するツールMeridianをデモした。一般に、論理LSI設計では、HDLというLSI設計用言語で論理を記述したRTLコードを書き終えると、そのコードに間違いがないかを検証する。検証を終えたら論理合成ツールにより回路を生成する。それを配置配線に落とし、シミュレーションで確認する。

Ascentは、RTLコードが間違っていないかどうかを検証するためのツールであり、フォーマル検証ツールと呼ばれている。従来は、入力のテストベクターを作りその出力値を予測値と比較して誤りの有無を検出していた。これでは作成するテストベクターすべての組み合わせをカバーできない。このため、数学的な手法を使ってすべての組み合わせをカバーできるようにするのが、最近、登場してきたフォーマル検証である。このAscentは自動的にフォーマル検証する。テストベクターを作る必要がない。設計したRTLコードのどこが間違っているかを出力してくれるため、設計者はデバッグだけを行えばよい。

AscentにはLint解析機能があり、誤り個所を指摘する。シンタックス（構文）や合成のミスマッチなどチェックし、手順も解析する。チェックするところは、データバスが競合しないか、出力がフローティングになっていないか、デッドロックがないか、などの状況である。

Ascentのようなフォーマル検証ツールはタイミングについては全く確認できない。このため、あとの工程になる配置配線ツールを使って論理回路を実際のシリコンに焼き付けるような状態（実際にはまだシリコンに落とさない）にしてからタイミングを検証してみる。

もう一つのMeridianは、そのタイミング検証ツールの一つであり、昨今の数種類のクロックを利用する複雑なSoCの設計検証に使う。一つのクロックと別のクロックが同時に一つのゲート回路に入ると不具合を起こすことがある。このCDCと呼ばれる不具合をチェックするのがMeridianである。

CDC（クロックドメインが交わる所）は、フロップからフロップへのパスとして定義され、そこでは送信フロップが受信フロップのクロックと非同期のクロックによってトリガーされている。クロックドメインAとクロックドメインBは互いに非同期である。

Meridianは基本的なフォーマルチェックを行う。人手でCDCを見つけるとすると、大変な作業になる。Meridianは、CDCのテンプレートを作成する必要はなく、まずクロックドメインが意図することを自動的に推論する。次に、CDCが非同期で働いていても準安定な状態（1と0の中間の状態で、時間が経つにつれどちらかになる）なのか安定な状態なのかを知る。準安定であれば、クロックを調整する。このようにして、いろいろな回路ブロックに渡り、CDCの検証を行い、階層的に推論し、最終的にシミュレーション結果をまとめる。

自動推論によるこの方法は検証時間を70%短縮できる、と同社社長兼CEOのPrakash Narain氏は言う。ベンダーが設計する市販のIPにもこの手法を使うことで、CDCデザインが悪いIP製品ではグリッチが見つかったとしている。