フォーマル検証の用途をJasperとCyberTecが調査，日米で同じ点と違う点
論理機能をチェックするためなどに使うフォーマル検証ツール。その用途などに関して，同ツールのEDAベンダーである米Jasper Design Automation, Inc.と同社の代理店を務めるCyberTec（本社：神奈川県）がEDAの展示会で調査した( CyberTec関連ページ)。
米国の調査は2009年7月の「DAC（Design Automation Conference） 2009」の来場者に対して，日本の調査は2010年1月の「EDSF（Electronic Design and Solution Fair 2010）」の来場者に対して行われた。どちらも，120名以上から回答を得て，その結果をまとめた。
調査方法に少々の違いはあるものの，日米どちらの調査でも，フォーマル検証への適用先で最も回答が多かったのは「RTLブロックの検証」だった（図1）。一方で最も大きな差があるのが，「アーキテクチャ検証」である。米国の調査では4位につけたが，日本の調査では8番目と最も低かった。
2位と3位のグループも米国と日本で同じで，「RTL開発」と「設計とIPコアの再利用」である。ただし，米国の結果では「設計とIPコアの再利用」の利用が2位なのに対して，日本の結果では「RTL開発」の方が僅差ながら2位だった。
この調査では，図1の各選択肢（x軸の項目）に対して，もう1段階細かな質問をしている（以下の結果は日本のみ）。例えば，全体の1位のRTLブロックの検証では，図2のように，その目的として「クリチカル機能」の検証を挙げている回答が多い。2位は「非同期の検証」，僅差で「プロトコルの確認」が続く。また3位の「設計とIPコアの再利用」では，「調査と理解」および「修正や再利用の促進」をフォーマル検証を適用する/したい先とするという回答が多かった。
