(57)【要約】【課題】形式的検証を実施したときに、ＲＴＬ記述において定量的な検証進捗を提供することができない。【解決手段】本発明の半導体集積回路の回路検証方法は、論理回路を設計したＲＴＬ記述を導入するＲＴＬ導入工程Ｓ１０と、ＲＴＬ記述をネットリストに変換するネットリスト変換工程Ｓ２０と、論理回路の動作仕様を示すプロパティを導入するプロパティ導入工程Ｓ３０と、プロパティを用いてネットリストに対して形式的検証を実施する形式的検証実施工程Ｓ４０と、検証されたネットリストのサブセットを用いて、ＲＴＬ記述において、検証されたネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程Ｓ５０とを含み、ＲＴＬ記述において定量的な検証進捗を提供することが可能になる。【選択図】図１
2008059032.tif 000002
【特許請求の範囲】
【請求項１】
半導体集積回路の論理回路を検証するための回路検証方法であって、
前記論理回路を設計したレジスタトランスファレベル記述を導入するＲＴＬ導入工程と、
前記レジスタトランスファレベル記述をネットリストに変換するネットリスト変換工程と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入工程と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施工程と、
前記形式的検証実施工程で検証された前記ネットリストのサブセットを用いて、前記レジスタトランスファレベル記述において、検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程とを含む回路検証方法。
【請求項２】
さらに、前記サブセット抽出工程で抽出された前記レジスタトランスファレベル記述のサブセットから、前記形式的検証で検証された前記論理回路の構成要素であるコンポーネントを導出するコンポーネント導出工程を含む請求項１に記載の回路検証方法。
【請求項３】
半導体集積回路の論理回路を検証するための回路検証方法であって、
論理シミュレーションによるカバレッジ結果を導入する論理シミュレーションカバレッジ導入工程と、
前記論理回路を設計したレジスタトランスファレベル記述を導入するＲＴＬ導入工程と、
前記レジスタトランスファレベル記述をネットリストに変換するネットリスト変換工程と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入工程と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施工程と、
前記形式的検証実施工程で検証された前記ネットリストのサブセットを用いて、前記レジスタトランスファレベル記述において、検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程と、
前記サブセット抽出工程で抽出された前記レジスタトランスファレベル記述のサブセットと、前記論理シミュレーションカバレッジ導入工程で導入された論理シミュレーションによるカバレッジ結果とをマージするカバレッジマージ工程とを含む回路検証方法。
【請求項４】
さらに、前記サブセット抽出工程で抽出された前記レジスタトランスファレベル記述のサブセットから、前記形式的検証で検証された前記論理回路の構成要素であるコンポーネントを導出するコンポーネント導出工程と、
前記コンポーネント導出工程で導出された前記コンポーネントと、前記論理シミュレーションカバレッジ導入工程で導入された論理シミュレーションによるカバレッジ結果とをマージするコンポーネントマージ工程とを含む請求項３に記載の回路検証方法。
【請求項５】
前記コンポーネントは演算器またはセレクタを含む請求項２または請求項４に記載の回路検証方法。
【請求項６】
前記形式的検証実施工程で検証された前記ネットリストのサブセットは、
前記形式的検証で用いた前記ネットリスト内のフリップフロップを抽出するＦＦ抽出工程と、
前記フリップフロップを用いて、検証済みの前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程とにより得られる請求項１から請求項５までのいずれかに記載の回路検証方法。
【請求項７】
前記レジスタトランスファレベル記述を示すサブセットは、前記フリップフロップを記述した前記レジスタトランスファレベル記述と、組み合わせ回路を記述した前記レジスタトランスファレベル記述を含む請求項６に記載の回路検証方法。
【請求項８】
前記組み合わせ回路を記述した前記レジスタトランスファレベル記述に、前記フリップフロップを記述した前記レジスタトランスファレベル記述からの論理段数の情報を含む請求項７に記載の回路検証方法。
【請求項９】
前記サブセット抽出工程は、前記レジスタトランスファレベル記述からコードのパス経路情報を導出し、前記パス経路情報を用いて前記レジスタトランスファレベル記述のサブセットを抽出する請求項１から請求項８までのいずれかに記載の回路検証方法。
【請求項１０】
前記カバレッジマージ工程は、前記レジスタトランスファレベル記述のサブセットと前記論理シミュレーションによるカバレッジ結果とを前記レジスタトランスファレベル記述におけるモジュール単位でマージする請求項３に記載の回路検証方法。
【請求項１１】
前記カバレッジマージ工程は、前記コンポーネントと前記論理シミュレーションによるカバレッジ結果とを前記レジスタトランスファレベル記述におけるコード単位でマージする請求項３に記載の回路検証方法。
【請求項１２】
前記コンポーネントマージ工程は、前記レジスタトランスファレベル記述のサブセットと前記論理シミュレーションによるカバレッジ結果とを前記レジスタトランスファレベル記述におけるモジュール単位でマージする請求項４に記載の回路検証方法。
【請求項１３】
前記コンポーネントマージ工程は、前記コンポーネントと前記論理シミュレーションによるカバレッジ結果とを前記レジスタトランスファレベル記述におけるコンポーネント種別ごとにマージする請求項４に記載の回路検証方法。
【請求項１４】
半導体集積回路の論理回路を検証するための回路検証装置であって、
前記論理回路を設計したレジスタトランスファレベル記述を導入するＲＴＬ導入部と、
前記レジスタトランスファレベル記述をネットリストに変換するネットリスト変換部と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入部と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施部と、
前記形式的検証実施部で検証された前記ネットリストのサブセットを用いて、前記レジスタトランスファレベル記述において、前記形式的検証実施部で検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出部と、
前記サブセット抽出部で抽出された前記レジスタトランスファレベル記述のサブセットにより回路検証の進捗を表示するカバレッジ表示部とを備えた回路検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、半導体集積回路に対する回路検証方法および回路検証装置に関する。
【背景技術】
【０００２】
半導体集積回路に対するテストベクタを用いた回路検証において、どこまで検証すればよいかという指標としてカバレッジ（coverage）が用いられている。カバレッジの算出方法の一例として、レジスタトランスファレベル（ＲＴＬ）記述の全記述行のうち、シミュレーションで何行実行されたかを計測する。これをラインカバレッジと呼ぶ。
【０００３】
別の回路検証方法として、論理が数学的に成立するかを証明する形式的検証方法がある。形式的検証方法ではラインカバレッジのような検証指標がなく、どれだけの検証がなされたかということが確認できない。そこで、形式的検証のカバレッジが考え出された。従来の形式的検証のカバレッジを以下に説明する。
【０００４】
図１５は従来の形式的検証のカバレッジ導出方法の流れを示すフローチャートである。
【０００５】
図１５において、Ｎ１０は設計回路を導入するステップ、Ｎ２０は動作仕様を示すプロパティを導入するステップ、Ｎ３０はプロパティを用いて形式的検証を実施するステップ、Ｎ４０はプロパティ検証の検証済みサブセットにより回路検証の進捗であるカバレッジを導出するステップである。Ｎ５０はステップＮ４０で導出したカバレッジが終了基準を満たさない場合にステップＮ２０に戻るステップである。
【０００６】
このようなステップを有することにより、形式的検証においても検証指標としてカバレッジを導出でき、カバレッジ結果を形式的検証のプロパティに追加するという形でフィードバックできる。結果として、効率的な形式的検証が実現される（特許文献１参照）。
【特許文献１】米国特許２００３−６５９４８０４号
【発明の開示】
【発明が解決しようとする課題】
【０００７】
昨今の半導体集積回路は、規模の増大が著しく、形式的検証の検証指標が必須となっている。そこで、カバレッジという概念が必須となる。図１５で述べた従来の形式的検証のカバレッジは、ネットリストにおける検証進捗を示したものであって、ラインカバレッジのようにＲＴＬ記述においてどこまで検証がなされているかというものを表したものではない。そのため、従来の形式的検証のカバレッジは、ＲＴＬ設計者やＲＴＬ検証者にとっては十分な指標とはなっていない。
【０００８】
本発明は、このような事情に鑑みて創作したものであり、ＲＴＬ設計者やＲＴＬ検証者にとって有効な検証指標となるように、形式的検証においても、ＲＴＬ記述において把握可能な検証指標が得られる回路検証方法および回路検証装置を提供することを目的としている。
【課題を解決するための手段】
【０００９】
（１）本発明による回路検証方法は、
半導体集積回路の論理回路を設計したＲＴＬ記述を導入するＲＴＬ導入工程と、
前記ＲＴＬ記述をネットリストに変換するネットリスト変換工程と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入工程と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施工程と、
前記形式的検証実施工程で検証された前記ネットリストのサブセットを用いて、前記ＲＴＬ記述において、検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程とを含むものである。
【００１０】
この構成によれば、半導体集積回路に対して形式的検証を実施した際に、サブセット抽出工程において、形式的検証で検証済みのネットリストのサブセットを用いて、ＲＴＬ記述において、ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出することにより、ＲＴＬ記述において把握可能な検証指標を示すことが可能になる。
【００１１】
（２）また、本発明による回路検証方法は、
半導体集積回路の論理回路を設計したＲＴＬ記述を導入するＲＴＬ導入工程と、
前記ＲＴＬ記述をネットリストに変換するネットリスト変換工程と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入工程と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施工程と、
前記形式的検証実施工程で検証された前記ネットリストのサブセットを用いて、前記ＲＴＬ記述において、検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程と、
前記サブセット抽出工程で抽出された前記ＲＴＬ記述のサブセットから、前記形式的検証で検証された前記論理回路の構成要素であるコンポーネントを導出するコンポーネント導出工程とを含むものである。
【００１２】
この構成によれば、半導体集積回路に対して形式的検証を実施した際に、コンポーネント導出工程において検証済みのコンポーネントを導出することにより、ＲＴＬ記述内のコンポーネントを用いて検証指標を示すことが可能になる。なお、論理回路の構成要素であるコンポーネントとは、例えば、加算、減算、乗算、除算やセレクタなどである。
【００１３】
（３）また、本発明による回路検証方法は、
論理シミュレーションによるカバレッジ結果を導入する論理シミュレーションカバレッジ導入工程と、
半導体集積回路の論理回路を設計したＲＴＬ記述を導入するＲＴＬ導入工程と、
前記ＲＴＬ記述をネットリストに変換するネットリスト変換工程と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入工程と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施工程と、
前記形式的検証実施工程で検証された前記ネットリストのサブセットを用いて、前記ＲＴＬ記述において、検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程と、
前記サブセット抽出工程で抽出された前記ＲＴＬ記述のサブセットと、前記論理シミュレーションカバレッジ導入工程で導入された論理シミュレーションによるカバレッジ結果とをマージするカバレッジマージ工程とを含むものである。
【００１４】
この構成によれば、半導体集積回路に対して形式的検証を実施した際に、カバレッジマージ工程において、サブセット抽出工程で抽出されたＲＴＬ記述のサブセットと、論理シミュレーションカバレッジ導入工程で導入された論理シミュレーションによるカバレッジ結果とをマージ（統合）することにより、従来のテストベクタを用いた回路検証と形式的検証の検証指標を統合した形で示すことが可能になる。
【００１５】
（４）また、本発明による回路検証方法は、
論理シミュレーションによるカバレッジ結果を導入する論理シミュレーションカバレッジ導入工程と、
半導体集積回路の論理回路を設計したＲＴＬ記述を導入するＲＴＬ導入工程と、
前記ＲＴＬ記述をネットリストに変換するネットリスト変換工程と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入工程と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施工程と、
前記形式的検証実施工程で検証された前記ネットリストのサブセットを用いて、前記ＲＴＬ記述において、検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程と、
前記サブセット抽出工程で抽出された前記ＲＴＬ記述のサブセットから、前記形式的検証で検証された前記論理回路の構成要素であるコンポーネントを導出するコンポーネント導出工程と、
前記コンポーネント導出工程で導出された前記コンポーネントと、前記論理シミュレーションカバレッジ導入工程で導入された論理シミュレーションによるカバレッジ結果とをマージするコンポーネントマージ工程とを含むものである。
【００１６】
この構成によれば、半導体集積回路に対して形式的検証を実施した際に、コンポーネントマージ工程において、コンポーネント導出工程で導出されたコンポーネントと論理シミュレーションカバレッジ導入工程で導入された論理シミュレーションによるカバレッジ結果とをマージすることにより、従来のテストベクタを用いた回路検証と形式的検証の検証指標を、ＲＴＬ記述内のコンポーネントを用いて統合した形で示すことが可能になる。
【００１７】
さらに、上記のコンポーネントに言及した回路検証方法において、前記コンポーネントとして演算器またはセレクタを含むという態様がある。この場合、ＲＴＬ記述内の演算器またはセレクタを用いて検証指標を示すことが可能になる。
【００１８】
また、上記のいずれかの回路検証方法において、前記形式的検証実施工程で検証された前記ネットリストのサブセットは、前記形式的検証で用いた前記ネットリスト内のフリップフロップを抽出するＦＦ抽出工程と、前記フリップフロップを用いて、検証済みの前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出工程とにより得られるという態様がある。この場合、サブセット抽出工程において、フリップフロップ（以下ＦＦ）を用いて検証済みのネットリストのサブセットを抽出するため、サブセット抽出工程においてＦＦを記述したＲＴＬ記述を手掛かりにサブセットの抽出が可能となる。
【００１９】
また、上記のフリップフロップに言及した回路検証方法において、前記ＲＴＬ記述を示すサブセットは、前記ＦＦを記述した前記ＲＴＬ記述と、組み合わせ回路を記述した前記ＲＴＬ記述を含むという態様がある。この場合、ＲＴＬ記述における検証指標を示す際に、ＦＦ記述、組み合わせ回路記述の両方を含むことにより、ＲＴＬ記述全体の検証指標が提供される。
【００２０】
また、上記の組み合わせ回路に言及した回路検証方法において、前記組み合わせ回路を記述した前記ＲＴＬ記述に、前記ＦＦを記述した前記ＲＴＬ記述からの論理段数の情報を含むという態様がある。この場合、ＲＴＬ記述における検証指標を示す際に、組み合わせ回路に論理段数の深さの情報が加わることにより、論理段数に比例したコードの実行確率に関する情報を提供することが可能となる。
【００２１】
また、上記のいずれかの回路検証方法において、前記サブセット抽出工程は、前記ＲＴＬ記述からコードのパス経路情報を導出し、前記パス経路情報を用いて前記ＲＴＬ記述のサブセットを抽出するという態様がある。この場合、ＲＴＬ記述のサブセットを抽出する際に、コードのパス経路情報を用いることにより、詳細にＲＴＬ記述における検証指標を提供することが可能となる。
【００２２】
また、上記のカバレッジマージ工程に言及した回路検証方法において、前記カバレッジマージ工程は、前記ＲＴＬ記述のサブセットと前記論理シミュレーションによるカバレッジ結果とを前記ＲＴＬ記述におけるモジュール単位でマージするという態様がある。この場合、モジュール単位でカバレッジ結果をマージすることにより、モジュール単位での検証進捗を提供することが可能となる。
【００２３】
また、上記のカバレッジマージ工程に言及した回路検証方法において、前記カバレッジマージ工程は、前記コンポーネントと前記論理シミュレーションによるカバレッジ結果とを前記ＲＴＬ記述におけるコード単位でマージするという態様がある。この場合、コード単位でカバレッジ結果をマージすることにより、コード単位での検証進捗を提供することが可能となる。
【００２４】
また、上記のコンポーネントマージ工程に言及した回路検証方法において、前記コンポーネントマージ工程は、前記ＲＴＬ記述のサブセットと前記論理シミュレーションによるカバレッジ結果とを前記ＲＴＬ記述におけるモジュール単位でマージするという態様がある。この場合、モジュール単位でカバレッジ結果をマージすることにより、モジュール単位でＲＴＬ記述内のコンポーネントを用いた検証進捗を提供することが可能となる。
【００２５】
また、上記のコンポーネントマージ工程に言及した回路検証方法において、前記コンポーネントマージ工程は、前記コンポーネントと前記論理シミュレーションによるカバレッジ結果とを前記ＲＴＬ記述におけるコンポーネント種別ごとにマージするという態様がある。この場合、コンポーネント種別単位でカバレッジ結果をマージすることにより、コンポーネント種別ごとの検証進捗を提供することが可能となる。
【００２６】
また、本発明による回路検証装置は、
半導体集積回路の論理回路を設計したＲＴＬ記述を導入するＲＴＬ導入部と、
前記ＲＴＬ記述をネットリストに変換するネットリスト変換部と、
前記論理回路の動作仕様を示すプロパティを導入するプロパティ導入部と、
前記プロパティを用いて前記ネットリストに対して形式的検証を実施する形式的検証実施部と、
前記形式的検証実施部で検証された前記ネットリストのサブセットを用いて、前記ＲＴＬ記述において、前記形式的検証実施部で検証された前記ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出するサブセット抽出部と、
前記サブセット抽出部で抽出された前記ＲＴＬ記述のサブセットにより回路検証の進捗を表示するカバレッジ表示部とを備えたものである。
【００２７】
この構成によれば、半導体集積回路に対して形式的検証を実施した際に、回路検証の進捗を表示するカバレッジ表示部により、ＲＴＬ記述において把握可能な検証指標を提供することが可能になる。
【発明の効果】
【００２８】
以上のように本発明によれば、形式的検証で検証済みのネットリストのサブセットを用いて、、サブセット抽出工程において、ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出することにより、ＲＴＬ記述において把握可能な検証指標を示すことが可能になる。
【００２９】
また、コンポーネント導出工程において検証済みのコンポーネントを導出することにより、ＲＴＬ記述内のコンポーネントを用いて検証指標を示すことが可能になる。
【００３０】
さらに、論理シミュレーションによるカバレッジ結果とマージすることにより、従来のテストベクタを用いた回路検証と形式的検証の検証指標を統合した形で示すことが可能になる。
【発明を実施するための最良の形態】
【００３１】
以下、本発明にかかわる半導体集積回路の回路検証方法の実施の形態について、図面を参照しながら具体的に説明する。
【００３２】
（実施の形態１）
図１は本発明の実施の形態１におけるＬＳＩの回路検証方法の処理の手順を示すフローチャートである。図１において、Ｓ１０はＲＴＬ導入工程であり、設計したＲＴＬ記述を導入するステップ、Ｓ２０はネットリスト変換工程であり、ＲＴＬ記述をネットリストに変換するステップ、Ｓ３０はプロパティ導入工程であり、動作仕様を示すプロパティを導入するステップ、Ｓ４０は形式的検証実施工程であり、プロパティを用いてネットリストに対して形式的検証を実施するステップ、Ｓ５０はサブセット抽出工程であり、検証済みのネットリストのサブセットを用いてＲＴＬ記述のサブセットを抽出するステップ、Ｓ６０はステップＳ５０で抽出されたＲＴＬ記述のサブセットにより回路検証の進捗を把握するステップ、Ｓ７０はステップＳ６０で把握した検証進捗が終了基準を満たしているか確認するステップである。なお、ネットリストのサブセットとは、検証対象である半導体集積回路のネットリストのうちの一部を示すものであり、ＲＴＬ記述のサブセットとは、検証対象である半導体集積回路を表現したＲＴＬ記述のうちの一部を示すものである。
【００３３】
以上のようなステップを有する実施の形態１の回路検証方法について、その動作を以下に説明する。
【００３４】
まずステップＳ１０において、設計したＲＴＬ記述を導入する。このＲＴＬ記述は形式的検証を実施する検証対象そのものである。なお、ＲＴＬ記述としては、Ｖｅｒｉｌｏｇ‐ＨＤＬやＶＨＤＬなど公知の設計言語が一般的であるが、これに限定されるものではない。
【００３５】
次に、ステップＳ２０において、ＲＴＬ記述をネットリストに変換する。
【００３６】
その後、ステップＳ３０において、動作仕様を示すプロパティを導入する。本実施の形態におけるプロパティは、「入力信号ｘと入力信号ｙが等しいとき、出力ｑは必ず０である。」とする。なお、プロパティはこれに限定されるものでない。
【００３７】
形式的検証実施工程のステップＳ４０において、ステップＳ３０で導入したプロパティを用いてネットリストに対して形式的検証を実施する。形式的検証の手法としては、図２で示すように、ＦＦを頂点とする組み合わせ回路網であるロジックコーンにＯＢＤＤ（Ordered Binary Decision Diagram）などの数学的解法により、図２の上図の設計回路と下図の期待値（ここでは、プロパティにより決定される）が等価であるかを調査する手法を用いることができる。なお、形式的検証の手法としてはこれに限定されるものでない。
【００３８】
次にステップＳ５０において、形式的検証において検証済みのネットリストのサブセットに対応したＲＴＬ記述のサブセットを抽出する。ここで、ＲＴＬ記述のサブセットを抽出するために、図３のステップを実施する。Ｓ５１は、形式的検証で用いたネットリスト内のＦＦを抽出するステップである。Ｓ５２はステップＳ５１で抽出したＦＦを用いて、対応するＲＴＬ記述のサブセットを抽出するステップである。
【００３９】
図４は、形式的検証において対象となったロジックコーンを示したものである。複数のロジックコーンのうち、ＦＦ２、ＦＦ３、ＦＦ５がステップＳ５１で抽出したＦＦである。ここで、形式的検証において対象となったロジックコーンとは、数学的解法を実施したロジックコーンを示しており、形式的検証ツールが出力することにより容易に知ることができる。なお、図４におけるＰＩはプライマリ入力、ＰＯはプライマリ出力を示している。
【００４０】
次に、ステップＳ５２でＲＴＬ記述のサブセットを抽出するが、本実施の形態においては検証済みのネットリストのサブセットは、ステップＳ５１で抽出したＦＦと等しく、ＦＦ２、ＦＦ３、ＦＦ５のみである。なお、検証したネットリストのサブセットに対応したＲＴＬ記述のサブセットを抽出する方法は、これに限定されるものでない。
【００４１】
図５は、本実施の形態におけるＲＴＬ記述の一部を示したものである。本実施の形態の場合、出力ＦＦ２、ＦＦ３、ＦＦ５のみを、検証済みのネットリストのサブセットとした。これは、図５における式１、式２、式３はＦＦ３の出力ｑにおけるＦＦ部の記述を表したものであり、形式的検証において検証したＲＴＬ記述となる。このように、形式的検証において検証済みのネットリストのサブセットに対応したＲＴＬ記述のサブセットを、ネットリストにおけるＦＦを基に抽出した。
【００４２】
なお、本実施の形態においてＲＴＬ記述のサブセットは、ＦＦ記述と組み合わせ回路記述を含んでいる。また、ＲＴＬ記述のサブセット出力ｑからの論理段数情報を所有している。その結果、組み合わせ回路記述においてＦＦからの論理深さにより、コードの実行可能性について推察できる。
【００４３】
図６は、本実施の形態におけるＲＴＬ記述のサブセットである。なお、サブセットの表現方法として、論理段数情報を所有するとは限らない。
【００４４】
また、ＲＴＬ記述からコードのパス経路情報を導出し、パス経路情報を用いて、ＲＴＬ記述のサブセットを抽出することも可能である。例えば、図４のＦＦ２、ＦＦ３を記述したＲＴＬ記述のコードの間で必ず実行されるＲＴＬ記述のコードは、検証されたＲＴＬ記述のサブセットとすることが可能である。
【００４５】
次に、図１のステップＳ６０において、ＲＴＬ記述のサブセットにより回路検証の進捗を把握する。本実施の形態では、図６のように、検証済みのＲＴＬ記述がサブセットとして表現されている。すなわち、実施されていないコード情報などを把握することができる。
【００４６】
最後に、図１のステップＳ７０において、検証進捗が終了基準を満たしているか確認する。例えば、ＲＴＬ記述のすべてのコードを検証するということを検証終了基準とした場合、すべてのコードが検証されていなければ、終了基準を満たしていないことになる。そこで、新たにプロパティを追加し、形式的検証を実施し、終了基準を満たすまで繰り返す。
【００４７】
本実施の形態によれば、半導体集積回路に対して形式的検証を実施した際に、形式的検証で検証済みのネットリストのサブセットを用いて、ＲＴＬ記述において、ネットリストのサブセットに対応するＲＴＬ記述のサブセットを抽出することにより、ＲＴＬ記述において把握可能な検証指標を示すことが可能になる。
【００４８】
また、ＦＦを用いて検証済みのネットリストのサブセットを抽出するため、ＦＦを記述したＲＴＬ記述を手掛かりにＲＴＬ記述のサブセットを抽出できる。また、コードパス情報を用いることにより、詳細にＲＴＬ記述のサブセットを抽出することができる。
【００４９】
さらに、ＲＴＬ記述のサブセットに論理段数情報を加えることにより、コードの実行しやすさに関する情報を把握することが可能になる。
【００５０】
（実施の形態２）
図７は本発明の実施の形態２におけるＬＳＩの回路検証方法の処理の手順を示すフローチャートである。図７において、実施の形態１の図１におけるのと同じステップ番号は同一の処理内容を示している。本実施の形態に特有のステップは、次のとおりである。Ｓ５３はステップＳ５０で抽出されたＲＴＬ記述のサブセットから検証済みのコンポーネントを導出するステップ、Ｓ６１はステップＳ５３で導出されたコンポーネントにより回路検証の進捗を把握するステップである。なお、コンポーネントとは、検証対象である半導体集積回路の論理の構成要素を示すものである。その他のステップについては、実施の形態１と同様であるので、説明を省略する。
【００５１】
本実施の形態は、実施の形態１と比較して、ステップＳ５３により検証したコンポーネントを導出することと、その後の検証進捗把握において、サブセットでなく、コンポーネントを用いている点が異なる。
【００５２】
図８は本実施の形態における検証済みのＲＴＬ記述のサブセット例である。ここで、乗算・減算などの四則演算または、セレクタ記述をコンポーネントとした。なお、コンポーネントとしては、これに限定されるものでない。
【００５３】
図９は、検証済みのコンポーネントを示した例である。すべてのコンポーネントのうち検証済みのコンポーネントを把握することができ、検証指標として用いることができる。
【００５４】
本実施の形態によれば、半導体集積回路に対して形式的検証を実施した際に、ＲＴＬ記述内のコンポーネントを用いて検証指標を示すことが可能となる。
【００５５】
（実施の形態３）
図１０は本発明の実施の形態３におけるＬＳＩの回路検証方法の処理の手順を示すフローチャートである。図１０において、実施の形態１の図１におけるのと同じステップ番号は同一の処理内容を示している。本実施の形態に特有のステップは、次のとおりである。Ｓ５は論理シミュレーションによるカバレッジ結果を導入するステップ、Ｓ５４はＲＴＬ記述のサブセットと論理シミュレーションによるカバレッジ結果とをマージするステップ、Ｓ６２はマージしたカバレッジ結果により回路検証の進捗を把握するステップである。その他のステップについては、実施の形態１と同様であるので、説明を省略する。
【００５６】
本実施の形態は、実施の形態１と比較して、論理シミュレーションによるカバレッジ結果を導入するステップＳ５と、ＲＴＬ記述のサブセットと論理シミュレーションによるカバレッジ結果とをマージするステップＳ５４が追加されている点が異なる。
【００５７】
図１１は今回マージを行う上で、検証対象となったモジュールとそのＲＴＬ記述を示したものである。モジュールＡには（ａ）〜（ｅ）の５つのＲＴＬ記述、モジュールＢには（ｆ）〜（ｉ）の４つのＲＴＬ記述が存在する。
【００５８】
図１２の上図はテストベクタのカバレッジ結果と、形式的検証によるサブセットを示したものである。図１２の下図はマージ結果例を示している。ここで、テストベクタまたは形式的検証で検証済みであるＲＴＬ記述を、マージ後の検証済みのＲＴＬ記述とした。モジュール単位でマージしたものと、コード単位でマージしたものを示している。なお、マージの方法はこれに限らない。
【００５９】
本実施の形態においては、形式的検証によるサブセットを用いてマージを行ったが、実施の形態２のようにコンポーネントを用いても構わない。
【００６０】
図１３の上図はテストベクタのカバレッジ結果と、形式的検証によるコンポーネントを示したものである。図１３の下図はマージ結果例を示している。モジュール単位でマージしたものと、コンポーネント種別単位でマージしたものを示している。なお、マージの方法はこれに限らない。
【００６１】
本実施の形態によれば、従来のテストベクタを用いた回路検証と形式的検証の検証指標を統合することが可能になる。
【００６２】
（実施の形態４）
図１４は本発明の実施の形態４におけるＬＳＩの回路検証装置の構成を示す概略構成図である。この構成において、中央演算装置１は、ＲＴＬ記述をネットリストに変換するネットリスト部、プロパティを用いてネットリストに対して形式的検証を実施する形式的検証実施部、および形式的検証実施部で検証済みのネットリストのサブセットに対応したＲＴＬ記述のサブセットを抽出するサブセット抽出部を担当する。また、入力装置３を用いて、半導体集積回路を設計したＲＴＬ記述と動作仕様を示すプロパティをハードディスク２に格納する。格納されたデータは、中央演算装置１とハードディスク２とのインターフェースを介して中央演算装置１内に取り込まれる。さらに、サブセット抽出部で抽出されたＲＴＬ記述のサブセットにより回路検証の進捗を中央演算装置１が外部出力装置４に出力するよう命令し、出力される。
【００６３】
この構成によれば、半導体集積回路に対して形式的検証を実施した際に、回路検証の進捗を表示することにより、ＲＴＬで把握可能な検証指標を視覚的に認識することが可能になる。
【産業上の利用可能性】
【００６４】
本発明の回路検証方法は、形式的検証における検証進捗を把握することができる方法であり、半導体集積回路の回路検証方法として有用である。
【図面の簡単な説明】
【００６５】
【図１】本発明の実施の形態１における半導体集積回路の回路検証方法の処理の手順を示すフローチャート
【図２】本発明の実施の形態１における形式的検証方法の説明図
【図３】本発明の実施の形態１のサブセットの抽出の処理の手順を示すフローチャート
【図４】本発明の実施の形態１において形式的検証の対象となるロジックコーンの説明図
【図５】本発明の実施の形態１において対象となるＲＴＬ記述の一部の例示図
【図６】本発明の実施の形態１において抽出されたＲＴＬ記述のサブセットの例示図
【図７】本発明の実施の形態２における半導体集積回路の回路検証方法の処理の手順を示すフローチャート
【図８】本発明の実施の形態２において用いたＲＴＬ記述のサブセットの例示図
【図９】本発明の実施の形態２において導出されたコンポーネントの例示図
【図１０】本発明の実施の形態３における半導体集積回路の回路検証方法の処理の手順を示すフローチャート
【図１１】本発明の実施の形態３において用いたモジュールとそれに対するＲＴＬ記述の例示図
【図１２】本発明の実施の形態３においてマージされたＲＴＬ記述のサブセットの例示図
【図１３】本発明の実施の形態３においてマージされたコンポーネントの例示図
【図１４】本発明の実施の形態４における半導体集積回路の回路検証装置の概略構成図
【図１５】従来の検証方法の処理の手順を示すフローチャート
【符号の説明】
【００６６】
Ｓ５  論理シミュレーションカバレッジ導入工程
Ｓ１０  ＲＴＬ導入工程
Ｓ２０  ネットリスト変換工程
Ｓ３０  プロパティ導入工程
Ｓ４０  形式的検証実施工程
Ｓ５０  サブセット抽出工程
Ｓ５１  ＦＦ抽出工程
Ｓ５２  サブセット抽出工程
Ｓ５３  コンポーネント導出工程
Ｓ５４  カバレッジマージ工程
Ｓ６０  サブセットにより回路検証の進捗を把握するステップ
Ｓ６１  コンポーネントにより回路検証の進捗を把握するステップ
Ｓ６２  マージしたカバレッジ結果により回路検証の進捗を把握するステップ
Ｓ７０  把握した検証進捗が終了基準を満たしているか確認するステップ
【図１】
2008059032.tif 000003
【図２】
2008059032.tif 000004
【図３】
2008059032.tif 000005
【図４】
2008059032.tif 000006
【図５】
2008059032.tif 000007
【図６】
2008059032.tif 000008
【図７】
2008059032.tif 000009
【図８】
2008059032.tif 000010
【図９】
2008059032.tif 000011
【図１０】
2008059032.tif 000012
【図１１】
2008059032.tif 000013
【図１２】
2008059032.tif 000014
【図１３】
2008059032.tif 000015
【図１４】
2008059032.tif 000016
【図１５】
2008059032.tif 000017