フォーマル検証ソリューション

フォーマル検証とは？

フォーマル検証とは、数学を基盤としたハードウェアの仕様記述・開発(設計/検証)の技術です。 科学的に裏付けされた仕様記述言語を用いて設計対象を表現することで、曖昧さが取り除かれ機械処理が可能になります。 自然言語で記述されている要求仕様の曖昧さを排除するために、専用の仕様記述言語で記号化することを「形式化」といい、形式化した仕様をもとに対象をとらえて検証する手法を「形式的検証手法」といいます。 形式的検証手法であるフォーマル検証では、計算のみで 動作の確認が可能であり、 回路を実際に動かして確認する 動的検証(Simulation)に対して「静的検証」と呼ばれます。 RTLの論理構造と、プロパティで定義した要求仕様の構造の等価性を計算によって検証します。

フォーマル検証のメリット

計算のみで実際に回路を動作させる必要がないため、テストベンチなど用意する必要がなく RTLがあれば実行できます。 網羅的に検証されるため、検証者がコーナーケース・レアケースを意識する必要もありません。

※ただし計算量が多いので、一度に検証できる回路規模には制限があります

しかしながら、フォーマル検証を使いこなすには専門知識が必要なため導入ハードルが高く、 実際に使ってみると、様々なトラブルが発生することもあります。 当社では、長年にわたる開発で培った経験をもとに、これらの課題を解決できるサービスを提供しています。

当社の提供するソリューション

フォーマル検証のメリットを最大限生かすためには、シミュレーション検証等の従来の手法とは異なる様々な専門知識やノウハウが必要となります。そのため、実際に使ってみたがうまく行かなかった、収束せずに諦めた等の声もよく聞かれます。当社では、過去10年以上のフォーマル検証活用実績を通じ、様々な課題を解決し、知見を蓄積してきました。そこで得られたノウハウをもとに、教育セミナーの実施や、使い勝手を大幅改善する導入環境のご提供など、 皆さまのお困りごとを解決するための様々なサービスを提供しています。