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

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

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

もう�kつのMeridianは、そのタイミング検証ツールの�kつであり、昨今の数�|類のクロックを�W��する複雑なSoCの設��検証に使う。�kつのクロックと別のクロックが同時に�kつのゲート�v路に入ると不�差腓���こすことがある。このCDCと�}ばれる不�差腓鬟船Д奪�するのがMeridianである。

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

Meridianは基本的なフォーマルチェックを行う。人�}でCDCを見つけるとすると、�j変な作業になる。Meridianは、CDCのテンプレートを作成する��要はなく、まずクロックドメインが�T図することを�O動的に推�bする。次に、CDCが��同期で働いていても���W定な�X��（1と0の中間の�X��で、時間が経つにつれどちらかになる）なのか�W定な�X��なのかを�瑤襦����W定であれば、クロックを調�Dする。このようにして、いろいろな�v路ブロックに渡り、CDCの検証を行い、階層的に推�bし、最終的にシミュレーション�T果をまとめる。

�O動推�bによるこの�桔，聾‐攣�間を70%�]縮できる、と同社社長兼CEOのPrakash Narain��は言う。ベンダーが設��する�x販のIPにもこの�}法を使うことで、CDCデザインが�KいIP����ではグリッチが見つかったとしている。