東芝情報システム株式会社

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

LSI設計において大きな問題となる検証工数の増加。この問題を解決する有効な手段として、近年注目を集めているのがフォーマル検証です。検証の網羅性を上げたい、テストベンチ作成工数を減らしたい、担当者の経験や能力依存を無くしたい、そんな声にお応えできるソリューションとして、東芝情報システムでは「フォーマル検証ソリューション」をご提供しています。

このページではこのようなことがわかります

  • 設計検証を効率的に進める方法

  • フォーマル検証の基盤技術が理解できる教育サービスについて

  • Cadence® Jasper™ RTL Appsの導入サービスのご提供

フォーマル検証とは?

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

フォーマル検証イメージ

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

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

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

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

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

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

提供ソリューションイメージ

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

ご相談、お問い合わせ

フォーマル検証の教育、導入のご相談はこちらからお問い合わせください。

お気軽にお問い合わせください。当社の製品・サービスは企業・団体・法人様向けに販売しております。

電話番号044-200-5300

コロナ禍のため、電話対応が難しい場合がございます。
[お問い合わせ]ボタンから問い合わせください。