半導体集積回路の検証装置及び検証方法
【課題】設計品質の向上を可能とする。
【解決手段】半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証装置であって、前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換するアサーション生成部と、前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較する比較部と、前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行うフォーマル検証部と、を有し、前記フォーマル検証部の検証結果と前記比較部の比較結果から、半導体集積回路を構成する回路の接続関係を検証する半導体集積回路の検証装置。
【解決手段】半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証装置であって、前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換するアサーション生成部と、前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較する比較部と、前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行うフォーマル検証部と、を有し、前記フォーマル検証部の検証結果と前記比較部の比較結果から、半導体集積回路を構成する回路の接続関係を検証する半導体集積回路の検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、半導体集積回路の検証装置及び検証方法に関するものである。
【背景技術】
【０００２】
一般に論理回路の検証方法には、大きく分けて論理シミュレーションとフォーマル検証がある。論理シミュレーションは、入力パターンを検証対象回路に与えて動作をシミュレーションし、出力パターンを期待値と比較して回路の正しさを検証する方法である。
【０００３】
一方、フォーマル検証は、設計の仕様と、検証対象回路をそれぞれ数学的に解析することで、回路の正しさを検証する方法である。なお、上記設計の仕様は、通常、ＩＥＥＥで標準化されたＰＳＬ（Property Specification Language）や、ＳＶＡ（System Verilog Assertion）のアサーション言語で記述される。
【０００４】
半導体集積回路は、各機能ブロック（以下、マクロと称す）から構成される。半導体集積回路は、年々回路の大規模化が進んでいる。大規模な半導体集積回路において、構成するマクロ間の接続関係を検証するために論理シミュレーションを用いる場合、膨大なテストパターンと、それをシミュレーションする膨大な時間がかかってしまう。このため、多大な検証工数が必要となってしまう。
【０００５】
一方、フォーマル検証では、テストパターンを作成する必要がないため、大幅な工数削減が期待できる。また、数学的に証明できるため、シミュレーションにおけるテストパターン漏れの心配が無い。そのため、マクロ間の接続検証には、フォーマル検証がシミュレーションより有効であり、その利用が拡大している。
【０００６】
半導体集積回路を構成する回路の接続仕様及びその回路記述との回路接続関係の一致性をフォーマル検証する半導体集積回路の検証装置として、例えば特許文献１のような検証装置が提案されている。特許文献１に開示されている検証装置１０の構成を図１３に示す。
【０００７】
図１３に示すように、検証装置１０は、プロパティ生成手段３と、検証実行手段５と、検証結果確認手段６とを有する。
【０００８】
プロパティ生成手段３は、検証対象回路の接続仕様１を読み込み、プロパティ４を生成する。プロパティ生成手段３は、個々の出力信号に対しユニークなプロパティを設定し、その出力信号が接続される入力信号については同一のプロパティ、若しくは同一のプロパティに極性情報を付加したプロパティを生成する。
【０００９】
検証実行手段５は、プロパティ４と回路記述２を読み込み、接続される出力信号と入力信号のプロパティが一致しているかの比較検証を行う。
【００１０】
検証結果確認手段６は、検証実行手段５での検証結果を表示する。
【先行技術文献】
【特許文献】
【００１１】
【特許文献１】特開２００５−１９６６８１号公報
【発明の概要】
【発明が解決しようとする課題】
【００１２】
特許文献１のような従来技術では、接続仕様からアサーション（プロパティ）に変換できるものしか検証できない。このため、通常、接続仕様として存在する半導体集積回路のマクロの端子がオープン（未接続）である箇所については検証できない。
【００１３】
このことは、半導体集積回路の設計仕様と回路記述との一致性を検証するために行われるフォーマル検証において、設計仕様の記述言語として一般に使用されるアサーション言語（例えばＰＳＬ、ＳＶＡ）では、オープンである端子を記述するという概念そのものがなく、記述できないからである。
【００１４】
従って、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかの区別がつかない問題がある。
【課題を解決するための手段】
【００１５】
本発明の一態様は、半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証装置であって、前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換するアサーション生成部と、前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較する比較部と、前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行うフォーマル検証部と、を有し、前記フォーマル検証部の検証結果と前記比較部の比較結果から、半導体集積回路を構成する回路の接続関係を検証する半導体集積回路の検証装置である。
【００１６】
本発明の他の態様は、半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証方法であって、前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換し、前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較し、前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行い、前記フォーマル検証の検証結果と、前記第１の端子情報と第２の端子情報の一致性の比較結果とから半導体集積回路を構成する回路の接続関係を検証する半導体集積回路の検証方法である。
【００１７】
本発明にかかる半導体集積回路の検証装置は、半導体集積回路を構成する回路の端子間に限定された接続仕様だけでなく、半導体集積回路を構成する回路の端子のオープン（未接続）箇所も含まれた接続仕様を用いて、設計結果である回路記述との回路接続関係の一致性を検証するこができる。これにより、半導体集積回路を構成する回路の接続検証に加えて、半導体集積回路を構成する回路のオープン端子について、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかを区別することが可能である。
【発明の効果】
【００１８】
本発明は、半導体集積回路の設計品質の向上を可能とする。
【図面の簡単な説明】
【００１９】
【図１】実施の形態１にかかる半導体集積回路の検証装置の構成を示すブロック図である。
【図２】実施の形態１にかかる接続仕様の情報の一例である。
【図３】実施の形態１にかかる回路記述により構成される半導体集積回路の構成の一例である。
【図４】実施の形態１にかかる回路記述のVerilog記述の一例である。
【図５】実施の形態１にかかるアサーション生成部により生成されるアサーションファイルの一例である。
【図６】実施の形態１にかかるアサーション生成部により生成されるバインドファイルの一例である。
【図７】実施の形態１にかかるオープンリスト生成部により生成されたオープンリストの一例である。
【図８】実施の形態１にかかる検証結果確認部の生成する結果情報の一例である。
【図９】実施の形態２にかかる半導体集積回路の検証装置の構成を示すブロック図である。
【図１０】実施の形態２にかかる接続仕様の情報の一例である。
【図１１】実施の形態２にかかる検証結果確認部の生成する結果情報の一例である。
【図１２】その他の実施の形態にかかる半導体集積回路の検証装置の構成を示すブロック図である。
【図１３】従来の半導体集積回路の検証装置の構成を示すブロック図である。
【発明を実施するための形態】
【００２０】
発明の実施の形態１
【００２１】
以下、本発明を適用した具体的な実施の形態１について、図面を参照しながら詳細に説明する。この実施の形態１は、本発明を半導体集積回路の検証装置に適用したものである。図１に本実施の形態１にかかる半導体集積回路１００の検証装置のブロック構成を示す。
【００２２】
図１に示すように、半導体集積回路の検証装置１００は、アサーション生成部１０３と、オープンリスト生成部１０５と、オープン検出部１０７と、フォーマル検証部１０８と、オープン比較部１０９と、検証結果確認部１１０とを有する。
【００２３】
アサーション生成部１０３は、接続仕様１０１をアサーション言語で記述された接続情報ファイルであるアサーション１０４に変換する。
【００２４】
ここで、接続仕様１０１は、検証対象となる回路記述１０２のマクロ間の接続仕様が記述されている。また、回路記述１０２は、半導体集積回路の構成を記述した検証対象となる回路記述であり、複数のマクロから構成され、通常VerilogやVHDLで記述される。
【００２５】
フォーマル検証部１０８は、接続情報ファイルであるアサーション１０４と回路記述１０２との一致性を検証する。
【００２６】
オープンリスト生成部１０５は、接続仕様１０１からオープン（未接続）である端子情報を抽出してオープンリスト１０６を生成する。
【００２７】
オープン検出部１０７は、回路記述１０２からオープン（未接続）である端子情報を抽出する。
【００２８】
オープン比較部１０９は、オープンリスト生成部１０５により生成されたオープンリスト１０６と、オープン検出部１０７により抽出された回路記述１０２のオープン端子情報とを比較する。
【００２９】
検証結果確認部１１０は、フォーマル検証部１０８により得られた検証結果と、オープン比較部１０９で得られたオープン比較結果とを合わせて総合的な検証結果として表示する。
【００３０】
次に、半導体集積回路の検証装置１００の動作について説明する。まず、図２に接続仕様１０１の一例を示す。また、図３、図４に、それぞれ回路記述１０２による半導体集積回路S_CHIPの構成例、Verilog記述例を示す。なお、図４のVerilogの記述内容が、図３の半導体集積回路S_CHIPの構成となることは、当業者において自明であるため図４の記述内容に関する詳細な説明は省略する。
【００３１】
半導体集積回路は、通常、複数のマクロから構成されており、図３の例では半導体集積回路S_CHIPが、２つのマクロD_MACRO、C_MACROを有する。ここでは、マクロD_MACRO、C_MACROのインスタンス名がそれぞれDINSTとCINSTとして構成され、図３で示されるように接続されている。
【００３２】
図３の半導体集積回路S_CHIPの構成を、接続仕様として定義しているが図２の接続仕様１０１である。この接続仕様１０１において、マクロ間の接続、マクロと外部端子との接続、マクロの端子でクランプされている箇所、マクロの端子でオープン（未接続）である箇所が定義されている。
【００３３】
詳細には、図２に示されているように、トップモジュール名、from側インスタンス名、ポート名、ビット範囲、to側インスタンス名、ポート名、ビット範囲が記述されていて、それぞれのマクロ端子間の接続が定義される。
【００３４】
例えば、マクロのインスタンス名CINST、端子名CLKである端子が、外部端子名CCLKである外部端子に接続される仕様の場合、From instance-name欄に「CINST」、From port-name欄に「CLK」、To instance-name欄に外部端子接続を示す「exported:」、To port-name欄に「CCLK」と記述される。
【００３５】
また、マクロのインスタンス名CINST、端子名DATA_O[31:0]であるバス端子が、マクロのインスタンス名DINST、端子名DATA_I[31:0]であるバス端子に接続される仕様の場合、From instance-name欄に「CINST」、From port-name欄に「DATA_O」、From msb欄に「31」、From lsb欄に「0」、To instance-name欄に「DINST」、To port-name欄に「DATA_I」、To msb欄に「31」、To lsb欄に「0」と記述される。
【００３６】
また、マクロのインスタンス名DINST、端子名がACKである端子が、オープン（未接続）である仕様の場合は、From instance-name欄に「DINST」、From port-name欄に「ACK」、To instance-name欄にオープンを示す「open:」と記述される。
【００３７】
このような接続仕様１０１からアサーション生成部１０３によりアサーション１０４が生成される。アサーション１０４は、アサーションファイル、バインドファイルから構成される。なお、アサーションは一般的に使用されているSVA（System Verilog Assertion）言語で生成される。以下、本実施の形態１においてもSVA言語が使用されるものとする。
【００３８】
図２の接続仕様の例からアサーション生成部１０３により生成されるアサーションファイルの例を図５、バインドファイルの例を図６に示す。図２、図５、図６を参照してアサーション生成部１０３の動作を説明する。
【００３９】
図５に示されるように、接続検証のアサーションは、プロパティ名がconnectionである以下に示すpropertyブロック構文を各assertステートメントが呼び出す形で作成される。
property connection(sig_a, sig_b);
@(sva_check_clk)(sig_a == sig_b);
endproperty:connection
【００４０】
図２の接続仕様１０１で、マクロのインスタンス名CINST、端子名CLKである端子が、外部端子名CCLKである外部端子に接続される仕様の場合、assertステートメントは次のように生成される。
CINST__CLK___CCLK:
assert property (connection (CINST_p_CLK, CCLK));
【００４１】
ここで、上記「CINST__CLK___CCLK」は、アサートラベルでインスタンス名、端子名、外部端子名が分かるようなラベルが生成される。また、上記「assert property (connection(CINST_p_CLK, CCLK))」でconnection propertyブロック構文を呼び出している。
【００４２】
connection(CINST_p_CLK, CCLK)の「CINST_p_CLK」は、回路記述１０２でマクロのインスタンス名CINST、端子名CLKである端子を示すS_CHIP.CINST.CLKとバインドされるよう図６のバンドファイルが生成される。同様に、connection(CINST_p_CLK, CCLK)の「CCLK」は、回路記述１０２で外部端子名CCLKである外部端子を示すS_CHIP.CCLKとバインドされるよう図６のバインドファイルが生成される。以降、同様な繰り返しで図２の接続仕様１０１からassertステートメントとバインドファイルが生成される。
【００４３】
ここで、接続仕様１０１から、オープンリスト生成部１０５によりオープンリスト１０６が生成される。図２の接続仕様１０１からオープンリスト生成部１０５により生成されたオープンリスト１０６を図７に示す。
【００４４】
図２、図７を参照してオープンリスト生成部１０５の動作を説明する。図２の接続仕様でTo instance-name欄が「open:」である行を抽出して、インスタンス名、端子名、ビット範囲からオープンリストを生成する。To instance-name欄が「open:」で、From instance-name欄が「DINST」、From port-name欄が「ACK」の場合は、図７に示すようにオープンリストに「DINST.ACK」が生成される。
【００４５】
ここで、回路記述１０２から、オープン検出部１０７によりオープン端子が検出される。図３を参照してオープン検出部１０７の動作を説明する。オープン検出部１０７は、図３の回路記述１０２で、各マクロのそれぞれの端子を一つずつ別のマクロに繋がっているか、外部端子に繋がっているか、あるいはクランプされているかをトレースし、そのいずれでもないものをオープンとして検出する。図３の回路記述１０２の場合では、マクロ名D_MACRO、インスタンス名DINSTの端子であるACKとEND[7:1]が検出される。そして、この検出結果がオープン端子情報として生成される。
【００４６】
ここで、アサーション１０４と回路記述１０２の一致性をフォーマル検証部１０８により検証する。図５、図６、図４を参照してフォーマル検証部１０８の動作を説明する。
【００４７】
フォーマル検証部１０８は、図６のバインドファイルに応じて、図５のアサーションファイルの記述と図４の回路記述１０２（Verilog記述）とをバインドし、その後、バインドした対象が接続されているかを検証する。例えば、以下に示すような図５のアサーションファイルの記述は、DINST_p_TCOとCINST_p_INT[9]とが接続されていることを検証するアサーションである。
DINST__TCO___CINST__INT__msb9lsb9:
assert property (connection (DINST_p_TCO, CINST_p_INT[9]));
【００４８】
上記アサーションファイルの記述により、DINST_p_TCOが、図６のバインドファイルに応じて、図４のVerilog記述のS_CHIP.DINST.TCOにバインドされる。ここで「S_CHIP.DINST.TCO」は図４のVerilog記述でモジュール名S_CHIP、インスタンス名DINST、端子名TCOの端子であることを示している。
【００４９】
また、CINST_p_INT[9]が、図６のバインドファイルに応じて、図４のVerilog記述のS_CHIP.CINST.INT[9]にバインドされる。ここで「S_CHIP.CINST.INT[9]」は図４のVerilog記述でモジュール名S_CHIP、インスタンス名CINST、端子名INT[9]の端子であることを示している。
【００５０】
そして、このアサーションファイルの記述により、Verilog記述のモジュール名S_CHIP、インスタンス名DINST、端子名TCOの端子と、モジュール名S_CHIP、インスタンス名CINST、端子名INT[9]の端子とが、接続されているかをフォーマル検証部１０８によりフォーマル検証される。このフォーマル検証において、上記端子同士が接続されていればそのアサーションはPassと判定、もしくは、Verilog記述で違った接続がされていればFailと判定される。そして、このようなフォーマル判定が図５のアサーションファイルの記述毎に行われる。
【００５１】
ここで、オープンリスト１０６とオープン検出部１０７により検出されたオープン端子情報とが、オープン比較部１０９により比較される。そして、その比較結果により、一致しているか、もしくは、オープンリスト１０６に余分なリストがあるのか、足りないリストがあるのかのオープン比較結果情報が生成される。
【００５２】
このオープン比較結果情報により、一致していると判定される場合は、接続仕様１０１に記述されたオープン端子の仕様通りに回路記述１０２は設計されていることを示している。
【００５３】
また、オープン比較結果情報により、オープンリスト１０６に余分なリストがあると判定される場合は、接続仕様１０１に記述されたオープン端子の仕様とは異なり、回路記述１０２ではオープンではない箇所があることを示している。逆に、オープン比較結果情報により、オープンリスト１０６に足らないリストがあると判定される場合は、接続仕様１０１で定義されていないオープン端子が回路記述１０２に存在していることを示している。
【００５４】
検証結果確認部１１０は、フォーマル検証部１０８からのアサーション１０４と回路記述１０２の一致性の判定情報を、オープン比較部１０９からオープンリスト１０６と回路記述１０２のマクロの端子がオープンである箇所とのオープン比較結果情報を、読み込む。そして、総合的な検証結果として表示装置等に表示、もしくは、データ出力装置等にデータとして出力する。例えば、図２の接続仕様１０１及び図４の回路記述１０２（Verilog記述）の場合、図８に示す結果が表示される。
【００５５】
以下に図８を参照して検証結果確認部１１０の動作を説明する。図８に示すように、「アサーションチェック結果（Summary）」の「Pass」には、接続仕様通りに回路記述が接続されている箇所の数、「Fail」には接続仕様通りに回路記述が接続されていない箇所の数が表示される。
【００５６】
また、図８に示すように、「オープン端子チェック結果（Summary）」の「Pass」には、接続仕様通りに回路記述のマクロの端子がオープンになっている箇所の数が示される。「Fail」には、接続仕様ではオープンになっているが回路記述では該当のマクロの端子がオープンになっていない箇所の数が示される。「Undef」には、接続仕様ではオープンと定義されていないが回路記述ではオープンになっている箇所の数が表示される。
【００５７】
更に、「アサーションチェック結果（詳細）」には、アサートラベルと前記Pass、Failの結果が表示される。アサートラベルは図５で示したものと同様で、「＜インスタンス名＞__＜端子名＞___＜インスタンス名＞__＜端子名＞」という構成となっている。そして、上記情報からどの端子間の接続アサーションがPass、Failしたかが分かる。
【００５８】
更に「オープン端子チェック結果（詳細）」には、接続仕様及び回路記述から抽出されたオープン端子が前記Pass、Fail、Undefの情報を伴い表示される。
【００５９】
以上のように、本実施の形態１の半導体集積回路の検証装置１００は、テストパターンが必要ないフォーマル検証でマクロ間の接続検証を行う場合に、接続仕様１０１を用いて、設計結果である回路記述１０２との回路接続関係の一致性を検証するこができる。
【００６０】
このことは、マクロの端子間の接続仕様についてはアサーション生成部１０３により生成されるアサーション１０４と回路記述１０２とのフォーマル検証で、マクロの端子のオープン仕様についてはオープンリスト生成部１０５により生成されるオープンリスト１０６と回路記述１０２からオープン検出部１０７により生成されるオープン端子情報との比較で、行われる。
【００６１】
これにより、マクロ間の接続検証に加えて、マクロのオープン端子について、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかの区別がつき、半導体集積回路の設計品質の向上が可能となる。
【００６２】
発明の実施の形態２
【００６３】
以下、本発明を適用した具体的な実施の形態２について、図面を参照しながら詳細に説明する。この実施の形態２は、実施の形態１と同様、本発明を半導体集積回路の検証装置に適用したものである。図９に本実施の形態１にかかる半導体集積回路２００の検証装置のブロック構成を示す。
【００６４】
図９に示すように、半導体集積回路の検証装置２００は、アサーション生成部１０３と、オープンリスト生成部１０５と、オープン検出部１０７と、フォーマル検証部１０８と、オープン比較部１０９と、検証結果確認部１１０と、仕様網羅性比較部２１１とを有する。なお、図９に示された符号のうち、図１と同じ符号を付した構成は、図１と同じか又は類似の構成を示している。実施の形態１と異なるのは、仕様網羅性比較部２１１を更に備えている点である。よって、本実施の形態２では、その相違部分を重点的に説明し、その他実施の形態１と同様の部分の説明は、特に必要でない限り省略する。
【００６５】
仕様網羅性比較部２１１は、アサーション１０４、オープンリスト１０６、回路記述１０２を読み込み、定義された接続仕様以外の余計な接続が回路記述１０２にないことの検証を行う。
【００６６】
検証結果確認部１１０は、フォーマル検証部１０８により得られた検証結果の判定情報と、オープン比較部１０９で得られたオープン比較結果情報と、仕様網羅性比較部２１１で得られた仕様網羅性比較結果情報とを合わせて総合的な検証結果として表示する。
【００６７】
次に、半導体集積回路の検証装置２００の動作について説明する。この動作の説明では、実施の形態１との差分部分のみを行う。その他の実施の形態１と同様の部分の説明は省略する。
【００６８】
仕様網羅性比較部２１１は、アサーション１０４、オープンリスト１０６、回路記述１０２を読み込む。そして、回路記述１０２からは、外部端子、マクロの端子を全て抽出する。アサーション１０４からは、アサーションの記述に含まれている外部端子、マクロの端子を全て抽出する。上記アサーション１０４から抽出された端子に、オープンリスト１０６の端子を加えたものと、上記回路記述１０２から抽出された端子の比較を行い、その結果を検証結果確認部１１０に伝える。
【００６９】
検証結果確認部１１０は、フォーマル検証部１０８からのアサーション１０４と回路記述１０２の一致性の判定情報を、オープン比較部１０９からオープンリスト１０６と回路記述１０２のマクロ端子がオープンである箇所との比較結果情報（オープン比較結果情報）を、仕様網羅性比較部２１１からアサーション１０４の端子情報にオープンリスト１０６の端子情報を加えたものと回路記述１０２の端子情報との比較結果情報（仕様網羅性比較結果情報）を読み込み、総合的な検証結果として表示する。
【００７０】
ここで、図１０に本実施の形態２の接続仕様１０１の例を示す。この接続仕様１０１と図４の回路記述１０２（Verilog記述）の場合、検証結果確認部１１０により図１１に示す結果が表示される。
【００７１】
図１０の接続仕様１０１では、図２の接続仕様１０１と比較して、マクロのインスタンス名DINST、端子名TCOである端子と、マクロのインスタンス名CINST、端子名INT[9]である端子との接続の定義がされていない。この図１０の接続仕様１０１と、設計された図４の回路記述１０２から、上述した定義の無い部分を接続仕様１０１で定義し忘れたか、あるいは、図４の回路記述１０２により誤って接続仕様１０１にない接続を設計してしまったことが考えられる。
【００７２】
図１１を参照して検証結果確認部１１０の動作を説明する。図１１に示す「アサーションチェック結果（Summary）」、「オープン端子チェック結果（Summary）」、「アサーションチェック結果（詳細）」、「オープン端子チェック結果（詳細）」については、実施の形態１と同様のため説明を省略する。
【００７３】
図１１に示すように、「接続定義漏れのチェック結果（Summary）」において、アサーション１０４の端子情報にオープンリスト１０６の端子情報を加えたものより、回路記述１０２の端子情報の方に一致しない余分な端子が存在する場合にその数を「Fail」として表示する。また、「接続定義漏れのチェック結果（詳細）」において、アサーション１０４の端子情報にオープンリスト１０６の端子情報を加えたもの以外の余計な端子情報が回路記述１０２の端子情報に存在する場合にその端子名を表示する。
【００７４】
以上のように、本実施の形態２の半導体集積回路の検証装置２００は、実施の形態１と同様、テストパターンが必要ないフォーマル検証でマクロ間の接続検証を行う場合に、接続仕様１０１を用いて、設計結果である回路記述１０２との回路接続関係の一致性を検証するこができる。
【００７５】
このことは、マクロの端子間の接続仕様についてはアサーション生成部１０３により生成されるアサーション１０４と回路記述１０２とのフォーマル検証で、マクロの端子のオープン仕様についてはオープンリスト生成部１０５により生成されるオープンリスト１０６と回路記述１０２からオープン検出部１０７により生成されるオープン端子情報との比較で、行われる。
【００７６】
これにより、マクロ間の接続検証に加えて、マクロのオープン端子について、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかの区別がつき、半導体集積回路の設計品質の向上が可能となる。
【００７７】
更に、本実施の形態２では、アサーション１０４の端子にオープンリスト１０６の端子を加えたものと、回路記述１０２の端子とを仕様網羅性比較部２１１で比較を行うことができる。
【００７８】
アサーション１０４の端子にオープンリスト１０６の端子を加えたものは、接続仕様１０１で定義されているオープン箇所を含めた端子である。このため、これと回路記述１０２の端子との比較を、仕様網羅性比較部２１１が行うことで、オープン箇所も含めて接続仕様が網羅的に検証できているのかを検証することができる。
【００７９】
実施の形態１では、接続仕様の網羅性検証として、接続仕様以外の余計な接続が回路記述にないことの検証、あるいは、接続仕様漏れの検証が不十分なものとなってしまう可能性があった。しかし、本実施の形態２では、定義された接続仕様以外の余計な接続が回路記述にないことの検証、あるいは、回路記述の接続仕様漏れの検証を正確に行うことができる。よって、実施の形態１と比較して、さらなる半導体集積回路の設計品質の向上が可能となる。
【００８０】
なお、本発明は上記実施の形態に限られたものでなく、趣旨を逸脱しない範囲で適宜変更することが可能である。
【００８１】
例えば、上述した実施の形態１、２の半導体集積回路の検証装置は、図１２に示すようなＰＣ等のコンピュータ３００で実現してもよい。以下、このようなコンピュータ３００で、半導体集積回路の検証装置を構成した例を簡単に説明する。図１２に示すようにコンピュータ３００は、ＣＰＵ３０１と、主メモリ３０２と、ＨＤＤ３０３と、ＲＯＭ３０４と、入出力装置３０５と、バス３０６とを有する。バス３０６は、ＣＰＵ３０１、主メモリ３０２、ＨＤＤ３０３、ＲＯＭ３０４、入出力装置３０５と接続され、各種情報を伝達する。
【００８２】
上述した接続仕様１０１、回路記述１０２の各情報は、コンピュータ３００のＨＤＤ３０３や、ネットワーク内のデータベース３０７等に保存されている。そして、ＣＰＵ３０１は、ＨＤＤ３０３もしくはＲＯＭ３０４に格納されている半導体集積回路の検証を実現するためのプログラム（以下、処理プログラムと称す）を呼び出し、主メモリ３０２に展開する。
【００８３】
上述したアサーション生成部１０３、オープンリスト生成部１０５、オープン検出部１０７、フォーマル検証部１０８、オープン比較部１０９、検証結果確認部１１０、仕様網羅性比較部２１１は、この処理プログラム内でモジュール化されている。なお、このコンピュータ３００を制御するオペレーティングシステムが各モジュールプログラムを制御するようにしてもよい。
【００８４】
例えば、実施の形態１において、アサーション生成部１０３及びオープンリスト生成部１０５として動作するプログラムは、ＨＤＤ３０３等に格納されている接続仕様１０１の情報から、それぞれアサーション１０４及びオープンリスト１０６を生成する。また、オープンリスト検出部１０５として動作するプログラムはＨＤＤ３０３等に格納されている回路記述１０２から、オープン端子情報を生成する。
【００８５】
そして、フォーマル検証部１０８として動作するプログラムが、アサーション１０４、接続仕様１０１から判定情報を生成する。また、オープン比較部１０９として動作するプログラムが、オープン比較結果情報を生成する。そして、検証結果確認部１１０として動作するプログラムが、判定情報、オープン比較結果情報に応じた総合的な検証結果として表示装置（不図示）等に表示する。
【００８６】
なお、アサーション生成部１０３、オープンリスト生成部１０５、オープン検出部１０７、フォーマル検証部１０８、オープン比較部１０９、検証結果確認部１１０、仕様網羅性比較部２１１をプログラムではなく、専用のハードウエアで実現してもよい。
【符号の説明】
【００８７】
１００、２００ 半導体集積回路の検証装置
１０１ 接続仕様
１０２ 回路記述
１０３ アサーション生成部
１０４ アサーション
１０５ オープンリスト生成部
１０６ オープンリスト
１０７ オープン検出部
１０８ フォーマル検証部
１０９ オープン比較部
１１０ 検証結果確認部
２１１ 仕様網羅性比較部
【技術分野】
【０００１】
本発明は、半導体集積回路の検証装置及び検証方法に関するものである。
【背景技術】
【０００２】
一般に論理回路の検証方法には、大きく分けて論理シミュレーションとフォーマル検証がある。論理シミュレーションは、入力パターンを検証対象回路に与えて動作をシミュレーションし、出力パターンを期待値と比較して回路の正しさを検証する方法である。
【０００３】
一方、フォーマル検証は、設計の仕様と、検証対象回路をそれぞれ数学的に解析することで、回路の正しさを検証する方法である。なお、上記設計の仕様は、通常、ＩＥＥＥで標準化されたＰＳＬ（Property Specification Language）や、ＳＶＡ（System Verilog Assertion）のアサーション言語で記述される。
【０００４】
半導体集積回路は、各機能ブロック（以下、マクロと称す）から構成される。半導体集積回路は、年々回路の大規模化が進んでいる。大規模な半導体集積回路において、構成するマクロ間の接続関係を検証するために論理シミュレーションを用いる場合、膨大なテストパターンと、それをシミュレーションする膨大な時間がかかってしまう。このため、多大な検証工数が必要となってしまう。
【０００５】
一方、フォーマル検証では、テストパターンを作成する必要がないため、大幅な工数削減が期待できる。また、数学的に証明できるため、シミュレーションにおけるテストパターン漏れの心配が無い。そのため、マクロ間の接続検証には、フォーマル検証がシミュレーションより有効であり、その利用が拡大している。
【０００６】
半導体集積回路を構成する回路の接続仕様及びその回路記述との回路接続関係の一致性をフォーマル検証する半導体集積回路の検証装置として、例えば特許文献１のような検証装置が提案されている。特許文献１に開示されている検証装置１０の構成を図１３に示す。
【０００７】
図１３に示すように、検証装置１０は、プロパティ生成手段３と、検証実行手段５と、検証結果確認手段６とを有する。
【０００８】
プロパティ生成手段３は、検証対象回路の接続仕様１を読み込み、プロパティ４を生成する。プロパティ生成手段３は、個々の出力信号に対しユニークなプロパティを設定し、その出力信号が接続される入力信号については同一のプロパティ、若しくは同一のプロパティに極性情報を付加したプロパティを生成する。
【０００９】
検証実行手段５は、プロパティ４と回路記述２を読み込み、接続される出力信号と入力信号のプロパティが一致しているかの比較検証を行う。
【００１０】
検証結果確認手段６は、検証実行手段５での検証結果を表示する。
【先行技術文献】
【特許文献】
【００１１】
【特許文献１】特開２００５−１９６６８１号公報
【発明の概要】
【発明が解決しようとする課題】
【００１２】
特許文献１のような従来技術では、接続仕様からアサーション（プロパティ）に変換できるものしか検証できない。このため、通常、接続仕様として存在する半導体集積回路のマクロの端子がオープン（未接続）である箇所については検証できない。
【００１３】
このことは、半導体集積回路の設計仕様と回路記述との一致性を検証するために行われるフォーマル検証において、設計仕様の記述言語として一般に使用されるアサーション言語（例えばＰＳＬ、ＳＶＡ）では、オープンである端子を記述するという概念そのものがなく、記述できないからである。
【００１４】
従って、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかの区別がつかない問題がある。
【課題を解決するための手段】
【００１５】
本発明の一態様は、半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証装置であって、前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換するアサーション生成部と、前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較する比較部と、前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行うフォーマル検証部と、を有し、前記フォーマル検証部の検証結果と前記比較部の比較結果から、半導体集積回路を構成する回路の接続関係を検証する半導体集積回路の検証装置である。
【００１６】
本発明の他の態様は、半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証方法であって、前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換し、前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較し、前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行い、前記フォーマル検証の検証結果と、前記第１の端子情報と第２の端子情報の一致性の比較結果とから半導体集積回路を構成する回路の接続関係を検証する半導体集積回路の検証方法である。
【００１７】
本発明にかかる半導体集積回路の検証装置は、半導体集積回路を構成する回路の端子間に限定された接続仕様だけでなく、半導体集積回路を構成する回路の端子のオープン（未接続）箇所も含まれた接続仕様を用いて、設計結果である回路記述との回路接続関係の一致性を検証するこができる。これにより、半導体集積回路を構成する回路の接続検証に加えて、半導体集積回路を構成する回路のオープン端子について、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかを区別することが可能である。
【発明の効果】
【００１８】
本発明は、半導体集積回路の設計品質の向上を可能とする。
【図面の簡単な説明】
【００１９】
【図１】実施の形態１にかかる半導体集積回路の検証装置の構成を示すブロック図である。
【図２】実施の形態１にかかる接続仕様の情報の一例である。
【図３】実施の形態１にかかる回路記述により構成される半導体集積回路の構成の一例である。
【図４】実施の形態１にかかる回路記述のVerilog記述の一例である。
【図５】実施の形態１にかかるアサーション生成部により生成されるアサーションファイルの一例である。
【図６】実施の形態１にかかるアサーション生成部により生成されるバインドファイルの一例である。
【図７】実施の形態１にかかるオープンリスト生成部により生成されたオープンリストの一例である。
【図８】実施の形態１にかかる検証結果確認部の生成する結果情報の一例である。
【図９】実施の形態２にかかる半導体集積回路の検証装置の構成を示すブロック図である。
【図１０】実施の形態２にかかる接続仕様の情報の一例である。
【図１１】実施の形態２にかかる検証結果確認部の生成する結果情報の一例である。
【図１２】その他の実施の形態にかかる半導体集積回路の検証装置の構成を示すブロック図である。
【図１３】従来の半導体集積回路の検証装置の構成を示すブロック図である。
【発明を実施するための形態】
【００２０】
発明の実施の形態１
【００２１】
以下、本発明を適用した具体的な実施の形態１について、図面を参照しながら詳細に説明する。この実施の形態１は、本発明を半導体集積回路の検証装置に適用したものである。図１に本実施の形態１にかかる半導体集積回路１００の検証装置のブロック構成を示す。
【００２２】
図１に示すように、半導体集積回路の検証装置１００は、アサーション生成部１０３と、オープンリスト生成部１０５と、オープン検出部１０７と、フォーマル検証部１０８と、オープン比較部１０９と、検証結果確認部１１０とを有する。
【００２３】
アサーション生成部１０３は、接続仕様１０１をアサーション言語で記述された接続情報ファイルであるアサーション１０４に変換する。
【００２４】
ここで、接続仕様１０１は、検証対象となる回路記述１０２のマクロ間の接続仕様が記述されている。また、回路記述１０２は、半導体集積回路の構成を記述した検証対象となる回路記述であり、複数のマクロから構成され、通常VerilogやVHDLで記述される。
【００２５】
フォーマル検証部１０８は、接続情報ファイルであるアサーション１０４と回路記述１０２との一致性を検証する。
【００２６】
オープンリスト生成部１０５は、接続仕様１０１からオープン（未接続）である端子情報を抽出してオープンリスト１０６を生成する。
【００２７】
オープン検出部１０７は、回路記述１０２からオープン（未接続）である端子情報を抽出する。
【００２８】
オープン比較部１０９は、オープンリスト生成部１０５により生成されたオープンリスト１０６と、オープン検出部１０７により抽出された回路記述１０２のオープン端子情報とを比較する。
【００２９】
検証結果確認部１１０は、フォーマル検証部１０８により得られた検証結果と、オープン比較部１０９で得られたオープン比較結果とを合わせて総合的な検証結果として表示する。
【００３０】
次に、半導体集積回路の検証装置１００の動作について説明する。まず、図２に接続仕様１０１の一例を示す。また、図３、図４に、それぞれ回路記述１０２による半導体集積回路S_CHIPの構成例、Verilog記述例を示す。なお、図４のVerilogの記述内容が、図３の半導体集積回路S_CHIPの構成となることは、当業者において自明であるため図４の記述内容に関する詳細な説明は省略する。
【００３１】
半導体集積回路は、通常、複数のマクロから構成されており、図３の例では半導体集積回路S_CHIPが、２つのマクロD_MACRO、C_MACROを有する。ここでは、マクロD_MACRO、C_MACROのインスタンス名がそれぞれDINSTとCINSTとして構成され、図３で示されるように接続されている。
【００３２】
図３の半導体集積回路S_CHIPの構成を、接続仕様として定義しているが図２の接続仕様１０１である。この接続仕様１０１において、マクロ間の接続、マクロと外部端子との接続、マクロの端子でクランプされている箇所、マクロの端子でオープン（未接続）である箇所が定義されている。
【００３３】
詳細には、図２に示されているように、トップモジュール名、from側インスタンス名、ポート名、ビット範囲、to側インスタンス名、ポート名、ビット範囲が記述されていて、それぞれのマクロ端子間の接続が定義される。
【００３４】
例えば、マクロのインスタンス名CINST、端子名CLKである端子が、外部端子名CCLKである外部端子に接続される仕様の場合、From instance-name欄に「CINST」、From port-name欄に「CLK」、To instance-name欄に外部端子接続を示す「exported:」、To port-name欄に「CCLK」と記述される。
【００３５】
また、マクロのインスタンス名CINST、端子名DATA_O[31:0]であるバス端子が、マクロのインスタンス名DINST、端子名DATA_I[31:0]であるバス端子に接続される仕様の場合、From instance-name欄に「CINST」、From port-name欄に「DATA_O」、From msb欄に「31」、From lsb欄に「0」、To instance-name欄に「DINST」、To port-name欄に「DATA_I」、To msb欄に「31」、To lsb欄に「0」と記述される。
【００３６】
また、マクロのインスタンス名DINST、端子名がACKである端子が、オープン（未接続）である仕様の場合は、From instance-name欄に「DINST」、From port-name欄に「ACK」、To instance-name欄にオープンを示す「open:」と記述される。
【００３７】
このような接続仕様１０１からアサーション生成部１０３によりアサーション１０４が生成される。アサーション１０４は、アサーションファイル、バインドファイルから構成される。なお、アサーションは一般的に使用されているSVA（System Verilog Assertion）言語で生成される。以下、本実施の形態１においてもSVA言語が使用されるものとする。
【００３８】
図２の接続仕様の例からアサーション生成部１０３により生成されるアサーションファイルの例を図５、バインドファイルの例を図６に示す。図２、図５、図６を参照してアサーション生成部１０３の動作を説明する。
【００３９】
図５に示されるように、接続検証のアサーションは、プロパティ名がconnectionである以下に示すpropertyブロック構文を各assertステートメントが呼び出す形で作成される。
property connection(sig_a, sig_b);
@(sva_check_clk)(sig_a == sig_b);
endproperty:connection
【００４０】
図２の接続仕様１０１で、マクロのインスタンス名CINST、端子名CLKである端子が、外部端子名CCLKである外部端子に接続される仕様の場合、assertステートメントは次のように生成される。
CINST__CLK___CCLK:
assert property (connection (CINST_p_CLK, CCLK));
【００４１】
ここで、上記「CINST__CLK___CCLK」は、アサートラベルでインスタンス名、端子名、外部端子名が分かるようなラベルが生成される。また、上記「assert property (connection(CINST_p_CLK, CCLK))」でconnection propertyブロック構文を呼び出している。
【００４２】
connection(CINST_p_CLK, CCLK)の「CINST_p_CLK」は、回路記述１０２でマクロのインスタンス名CINST、端子名CLKである端子を示すS_CHIP.CINST.CLKとバインドされるよう図６のバンドファイルが生成される。同様に、connection(CINST_p_CLK, CCLK)の「CCLK」は、回路記述１０２で外部端子名CCLKである外部端子を示すS_CHIP.CCLKとバインドされるよう図６のバインドファイルが生成される。以降、同様な繰り返しで図２の接続仕様１０１からassertステートメントとバインドファイルが生成される。
【００４３】
ここで、接続仕様１０１から、オープンリスト生成部１０５によりオープンリスト１０６が生成される。図２の接続仕様１０１からオープンリスト生成部１０５により生成されたオープンリスト１０６を図７に示す。
【００４４】
図２、図７を参照してオープンリスト生成部１０５の動作を説明する。図２の接続仕様でTo instance-name欄が「open:」である行を抽出して、インスタンス名、端子名、ビット範囲からオープンリストを生成する。To instance-name欄が「open:」で、From instance-name欄が「DINST」、From port-name欄が「ACK」の場合は、図７に示すようにオープンリストに「DINST.ACK」が生成される。
【００４５】
ここで、回路記述１０２から、オープン検出部１０７によりオープン端子が検出される。図３を参照してオープン検出部１０７の動作を説明する。オープン検出部１０７は、図３の回路記述１０２で、各マクロのそれぞれの端子を一つずつ別のマクロに繋がっているか、外部端子に繋がっているか、あるいはクランプされているかをトレースし、そのいずれでもないものをオープンとして検出する。図３の回路記述１０２の場合では、マクロ名D_MACRO、インスタンス名DINSTの端子であるACKとEND[7:1]が検出される。そして、この検出結果がオープン端子情報として生成される。
【００４６】
ここで、アサーション１０４と回路記述１０２の一致性をフォーマル検証部１０８により検証する。図５、図６、図４を参照してフォーマル検証部１０８の動作を説明する。
【００４７】
フォーマル検証部１０８は、図６のバインドファイルに応じて、図５のアサーションファイルの記述と図４の回路記述１０２（Verilog記述）とをバインドし、その後、バインドした対象が接続されているかを検証する。例えば、以下に示すような図５のアサーションファイルの記述は、DINST_p_TCOとCINST_p_INT[9]とが接続されていることを検証するアサーションである。
DINST__TCO___CINST__INT__msb9lsb9:
assert property (connection (DINST_p_TCO, CINST_p_INT[9]));
【００４８】
上記アサーションファイルの記述により、DINST_p_TCOが、図６のバインドファイルに応じて、図４のVerilog記述のS_CHIP.DINST.TCOにバインドされる。ここで「S_CHIP.DINST.TCO」は図４のVerilog記述でモジュール名S_CHIP、インスタンス名DINST、端子名TCOの端子であることを示している。
【００４９】
また、CINST_p_INT[9]が、図６のバインドファイルに応じて、図４のVerilog記述のS_CHIP.CINST.INT[9]にバインドされる。ここで「S_CHIP.CINST.INT[9]」は図４のVerilog記述でモジュール名S_CHIP、インスタンス名CINST、端子名INT[9]の端子であることを示している。
【００５０】
そして、このアサーションファイルの記述により、Verilog記述のモジュール名S_CHIP、インスタンス名DINST、端子名TCOの端子と、モジュール名S_CHIP、インスタンス名CINST、端子名INT[9]の端子とが、接続されているかをフォーマル検証部１０８によりフォーマル検証される。このフォーマル検証において、上記端子同士が接続されていればそのアサーションはPassと判定、もしくは、Verilog記述で違った接続がされていればFailと判定される。そして、このようなフォーマル判定が図５のアサーションファイルの記述毎に行われる。
【００５１】
ここで、オープンリスト１０６とオープン検出部１０７により検出されたオープン端子情報とが、オープン比較部１０９により比較される。そして、その比較結果により、一致しているか、もしくは、オープンリスト１０６に余分なリストがあるのか、足りないリストがあるのかのオープン比較結果情報が生成される。
【００５２】
このオープン比較結果情報により、一致していると判定される場合は、接続仕様１０１に記述されたオープン端子の仕様通りに回路記述１０２は設計されていることを示している。
【００５３】
また、オープン比較結果情報により、オープンリスト１０６に余分なリストがあると判定される場合は、接続仕様１０１に記述されたオープン端子の仕様とは異なり、回路記述１０２ではオープンではない箇所があることを示している。逆に、オープン比較結果情報により、オープンリスト１０６に足らないリストがあると判定される場合は、接続仕様１０１で定義されていないオープン端子が回路記述１０２に存在していることを示している。
【００５４】
検証結果確認部１１０は、フォーマル検証部１０８からのアサーション１０４と回路記述１０２の一致性の判定情報を、オープン比較部１０９からオープンリスト１０６と回路記述１０２のマクロの端子がオープンである箇所とのオープン比較結果情報を、読み込む。そして、総合的な検証結果として表示装置等に表示、もしくは、データ出力装置等にデータとして出力する。例えば、図２の接続仕様１０１及び図４の回路記述１０２（Verilog記述）の場合、図８に示す結果が表示される。
【００５５】
以下に図８を参照して検証結果確認部１１０の動作を説明する。図８に示すように、「アサーションチェック結果（Summary）」の「Pass」には、接続仕様通りに回路記述が接続されている箇所の数、「Fail」には接続仕様通りに回路記述が接続されていない箇所の数が表示される。
【００５６】
また、図８に示すように、「オープン端子チェック結果（Summary）」の「Pass」には、接続仕様通りに回路記述のマクロの端子がオープンになっている箇所の数が示される。「Fail」には、接続仕様ではオープンになっているが回路記述では該当のマクロの端子がオープンになっていない箇所の数が示される。「Undef」には、接続仕様ではオープンと定義されていないが回路記述ではオープンになっている箇所の数が表示される。
【００５７】
更に、「アサーションチェック結果（詳細）」には、アサートラベルと前記Pass、Failの結果が表示される。アサートラベルは図５で示したものと同様で、「＜インスタンス名＞__＜端子名＞___＜インスタンス名＞__＜端子名＞」という構成となっている。そして、上記情報からどの端子間の接続アサーションがPass、Failしたかが分かる。
【００５８】
更に「オープン端子チェック結果（詳細）」には、接続仕様及び回路記述から抽出されたオープン端子が前記Pass、Fail、Undefの情報を伴い表示される。
【００５９】
以上のように、本実施の形態１の半導体集積回路の検証装置１００は、テストパターンが必要ないフォーマル検証でマクロ間の接続検証を行う場合に、接続仕様１０１を用いて、設計結果である回路記述１０２との回路接続関係の一致性を検証するこができる。
【００６０】
このことは、マクロの端子間の接続仕様についてはアサーション生成部１０３により生成されるアサーション１０４と回路記述１０２とのフォーマル検証で、マクロの端子のオープン仕様についてはオープンリスト生成部１０５により生成されるオープンリスト１０６と回路記述１０２からオープン検出部１０７により生成されるオープン端子情報との比較で、行われる。
【００６１】
これにより、マクロ間の接続検証に加えて、マクロのオープン端子について、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかの区別がつき、半導体集積回路の設計品質の向上が可能となる。
【００６２】
発明の実施の形態２
【００６３】
以下、本発明を適用した具体的な実施の形態２について、図面を参照しながら詳細に説明する。この実施の形態２は、実施の形態１と同様、本発明を半導体集積回路の検証装置に適用したものである。図９に本実施の形態１にかかる半導体集積回路２００の検証装置のブロック構成を示す。
【００６４】
図９に示すように、半導体集積回路の検証装置２００は、アサーション生成部１０３と、オープンリスト生成部１０５と、オープン検出部１０７と、フォーマル検証部１０８と、オープン比較部１０９と、検証結果確認部１１０と、仕様網羅性比較部２１１とを有する。なお、図９に示された符号のうち、図１と同じ符号を付した構成は、図１と同じか又は類似の構成を示している。実施の形態１と異なるのは、仕様網羅性比較部２１１を更に備えている点である。よって、本実施の形態２では、その相違部分を重点的に説明し、その他実施の形態１と同様の部分の説明は、特に必要でない限り省略する。
【００６５】
仕様網羅性比較部２１１は、アサーション１０４、オープンリスト１０６、回路記述１０２を読み込み、定義された接続仕様以外の余計な接続が回路記述１０２にないことの検証を行う。
【００６６】
検証結果確認部１１０は、フォーマル検証部１０８により得られた検証結果の判定情報と、オープン比較部１０９で得られたオープン比較結果情報と、仕様網羅性比較部２１１で得られた仕様網羅性比較結果情報とを合わせて総合的な検証結果として表示する。
【００６７】
次に、半導体集積回路の検証装置２００の動作について説明する。この動作の説明では、実施の形態１との差分部分のみを行う。その他の実施の形態１と同様の部分の説明は省略する。
【００６８】
仕様網羅性比較部２１１は、アサーション１０４、オープンリスト１０６、回路記述１０２を読み込む。そして、回路記述１０２からは、外部端子、マクロの端子を全て抽出する。アサーション１０４からは、アサーションの記述に含まれている外部端子、マクロの端子を全て抽出する。上記アサーション１０４から抽出された端子に、オープンリスト１０６の端子を加えたものと、上記回路記述１０２から抽出された端子の比較を行い、その結果を検証結果確認部１１０に伝える。
【００６９】
検証結果確認部１１０は、フォーマル検証部１０８からのアサーション１０４と回路記述１０２の一致性の判定情報を、オープン比較部１０９からオープンリスト１０６と回路記述１０２のマクロ端子がオープンである箇所との比較結果情報（オープン比較結果情報）を、仕様網羅性比較部２１１からアサーション１０４の端子情報にオープンリスト１０６の端子情報を加えたものと回路記述１０２の端子情報との比較結果情報（仕様網羅性比較結果情報）を読み込み、総合的な検証結果として表示する。
【００７０】
ここで、図１０に本実施の形態２の接続仕様１０１の例を示す。この接続仕様１０１と図４の回路記述１０２（Verilog記述）の場合、検証結果確認部１１０により図１１に示す結果が表示される。
【００７１】
図１０の接続仕様１０１では、図２の接続仕様１０１と比較して、マクロのインスタンス名DINST、端子名TCOである端子と、マクロのインスタンス名CINST、端子名INT[9]である端子との接続の定義がされていない。この図１０の接続仕様１０１と、設計された図４の回路記述１０２から、上述した定義の無い部分を接続仕様１０１で定義し忘れたか、あるいは、図４の回路記述１０２により誤って接続仕様１０１にない接続を設計してしまったことが考えられる。
【００７２】
図１１を参照して検証結果確認部１１０の動作を説明する。図１１に示す「アサーションチェック結果（Summary）」、「オープン端子チェック結果（Summary）」、「アサーションチェック結果（詳細）」、「オープン端子チェック結果（詳細）」については、実施の形態１と同様のため説明を省略する。
【００７３】
図１１に示すように、「接続定義漏れのチェック結果（Summary）」において、アサーション１０４の端子情報にオープンリスト１０６の端子情報を加えたものより、回路記述１０２の端子情報の方に一致しない余分な端子が存在する場合にその数を「Fail」として表示する。また、「接続定義漏れのチェック結果（詳細）」において、アサーション１０４の端子情報にオープンリスト１０６の端子情報を加えたもの以外の余計な端子情報が回路記述１０２の端子情報に存在する場合にその端子名を表示する。
【００７４】
以上のように、本実施の形態２の半導体集積回路の検証装置２００は、実施の形態１と同様、テストパターンが必要ないフォーマル検証でマクロ間の接続検証を行う場合に、接続仕様１０１を用いて、設計結果である回路記述１０２との回路接続関係の一致性を検証するこができる。
【００７５】
このことは、マクロの端子間の接続仕様についてはアサーション生成部１０３により生成されるアサーション１０４と回路記述１０２とのフォーマル検証で、マクロの端子のオープン仕様についてはオープンリスト生成部１０５により生成されるオープンリスト１０６と回路記述１０２からオープン検出部１０７により生成されるオープン端子情報との比較で、行われる。
【００７６】
これにより、マクロ間の接続検証に加えて、マクロのオープン端子について、設計者が意図してオープンとしたのか、設計ミスとしてオープンとしたのかの区別がつき、半導体集積回路の設計品質の向上が可能となる。
【００７７】
更に、本実施の形態２では、アサーション１０４の端子にオープンリスト１０６の端子を加えたものと、回路記述１０２の端子とを仕様網羅性比較部２１１で比較を行うことができる。
【００７８】
アサーション１０４の端子にオープンリスト１０６の端子を加えたものは、接続仕様１０１で定義されているオープン箇所を含めた端子である。このため、これと回路記述１０２の端子との比較を、仕様網羅性比較部２１１が行うことで、オープン箇所も含めて接続仕様が網羅的に検証できているのかを検証することができる。
【００７９】
実施の形態１では、接続仕様の網羅性検証として、接続仕様以外の余計な接続が回路記述にないことの検証、あるいは、接続仕様漏れの検証が不十分なものとなってしまう可能性があった。しかし、本実施の形態２では、定義された接続仕様以外の余計な接続が回路記述にないことの検証、あるいは、回路記述の接続仕様漏れの検証を正確に行うことができる。よって、実施の形態１と比較して、さらなる半導体集積回路の設計品質の向上が可能となる。
【００８０】
なお、本発明は上記実施の形態に限られたものでなく、趣旨を逸脱しない範囲で適宜変更することが可能である。
【００８１】
例えば、上述した実施の形態１、２の半導体集積回路の検証装置は、図１２に示すようなＰＣ等のコンピュータ３００で実現してもよい。以下、このようなコンピュータ３００で、半導体集積回路の検証装置を構成した例を簡単に説明する。図１２に示すようにコンピュータ３００は、ＣＰＵ３０１と、主メモリ３０２と、ＨＤＤ３０３と、ＲＯＭ３０４と、入出力装置３０５と、バス３０６とを有する。バス３０６は、ＣＰＵ３０１、主メモリ３０２、ＨＤＤ３０３、ＲＯＭ３０４、入出力装置３０５と接続され、各種情報を伝達する。
【００８２】
上述した接続仕様１０１、回路記述１０２の各情報は、コンピュータ３００のＨＤＤ３０３や、ネットワーク内のデータベース３０７等に保存されている。そして、ＣＰＵ３０１は、ＨＤＤ３０３もしくはＲＯＭ３０４に格納されている半導体集積回路の検証を実現するためのプログラム（以下、処理プログラムと称す）を呼び出し、主メモリ３０２に展開する。
【００８３】
上述したアサーション生成部１０３、オープンリスト生成部１０５、オープン検出部１０７、フォーマル検証部１０８、オープン比較部１０９、検証結果確認部１１０、仕様網羅性比較部２１１は、この処理プログラム内でモジュール化されている。なお、このコンピュータ３００を制御するオペレーティングシステムが各モジュールプログラムを制御するようにしてもよい。
【００８４】
例えば、実施の形態１において、アサーション生成部１０３及びオープンリスト生成部１０５として動作するプログラムは、ＨＤＤ３０３等に格納されている接続仕様１０１の情報から、それぞれアサーション１０４及びオープンリスト１０６を生成する。また、オープンリスト検出部１０５として動作するプログラムはＨＤＤ３０３等に格納されている回路記述１０２から、オープン端子情報を生成する。
【００８５】
そして、フォーマル検証部１０８として動作するプログラムが、アサーション１０４、接続仕様１０１から判定情報を生成する。また、オープン比較部１０９として動作するプログラムが、オープン比較結果情報を生成する。そして、検証結果確認部１１０として動作するプログラムが、判定情報、オープン比較結果情報に応じた総合的な検証結果として表示装置（不図示）等に表示する。
【００８６】
なお、アサーション生成部１０３、オープンリスト生成部１０５、オープン検出部１０７、フォーマル検証部１０８、オープン比較部１０９、検証結果確認部１１０、仕様網羅性比較部２１１をプログラムではなく、専用のハードウエアで実現してもよい。
【符号の説明】
【００８７】
１００、２００ 半導体集積回路の検証装置
１０１ 接続仕様
１０２ 回路記述
１０３ アサーション生成部
１０４ アサーション
１０５ オープンリスト生成部
１０６ オープンリスト
１０７ オープン検出部
１０８ フォーマル検証部
１０９ オープン比較部
１１０ 検証結果確認部
２１１ 仕様網羅性比較部
【特許請求の範囲】
【請求項１】
半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証装置であって、
前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換するアサーション生成部と、
前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較する比較部と、
前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行うフォーマル検証部と、を有し、
前記フォーマル検証部の検証結果と前記比較部の比較結果から、半導体集積回路を構成する回路の接続関係を検証する
半導体集積回路の検証装置。
【請求項２】
オープン検出部と、オープンリスト生成部とを更に有し、
前記オープンリスト生成部は、前記接続仕様情報からオープンである端子の情報を抽出し、前記第１の端子情報として生成し、
前記オープン検出部は、前記回路記述情報からオープンである端子の情報を抽出し、前記第２の端子情報として生成する
請求項１に記載の半導体集積回路の検証装置。
【請求項３】
前記フォーマル検証部の検証結果と前記比較部の比較結果から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子を検証できる
請求項１または請求項２に記載の半導体集積回路の検証装置。
【請求項４】
仕様網羅性比較部を更に有し、
前記仕様網羅性比較部は、前記接続情報ファイルと、前記第１の端子情報と、前記回路記述情報とから前記半導体集積回路を構成する回路の接続関係を抽出し、第３の端子情報を生成する
請求項１〜請求項３のいずれか１項に記載の半導体集積回路の検証装置。
【請求項５】
前記フォーマル検証部の検証結果と、前記比較部の比較結果と、前記第３の端子情報から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子、及び、前記接続仕様情報と前記回路記述情報の一致誤差を検証できる
請求項４に記載の半導体集積回路の検証装置。
【請求項６】
半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証方法であって、
前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換し、
前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較し、
前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行い、
前記フォーマル検証の検証結果と、前記第１の端子情報と第２の端子情報の一致性の比較結果とから半導体集積回路を構成する回路の接続関係を検証する
半導体集積回路の検証方法。
【請求項７】
前記フォーマル検証の検証結果と、前記第１の端子情報と前記第２の端子情報の一致性の比較結果から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子を検証できる
請求項６に記載の半導体集積回路の検証方法。
【請求項８】
前記接続情報ファイルと、前記第１の端子情報と、前記回路記述情報とから前記半導体集積回路を構成する回路の接続関係を抽出し、第３の端子情報を生成する
請求項６もしくは請求項７に記載の半導体集積回路の検証方法。
【請求項９】
前記フォーマル検証の検証結果と、前記第１の端子情報と第２の端子情報の一致性の比較結果と、前記第３の端子情報から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子、及び、前記接続仕様情報と前記回路記述情報の一致誤差を検証できる
請求項８に記載の半導体集積回路の検証方法。
【請求項１】
半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証装置であって、
前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換するアサーション生成部と、
前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較する比較部と、
前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行うフォーマル検証部と、を有し、
前記フォーマル検証部の検証結果と前記比較部の比較結果から、半導体集積回路を構成する回路の接続関係を検証する
半導体集積回路の検証装置。
【請求項２】
オープン検出部と、オープンリスト生成部とを更に有し、
前記オープンリスト生成部は、前記接続仕様情報からオープンである端子の情報を抽出し、前記第１の端子情報として生成し、
前記オープン検出部は、前記回路記述情報からオープンである端子の情報を抽出し、前記第２の端子情報として生成する
請求項１に記載の半導体集積回路の検証装置。
【請求項３】
前記フォーマル検証部の検証結果と前記比較部の比較結果から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子を検証できる
請求項１または請求項２に記載の半導体集積回路の検証装置。
【請求項４】
仕様網羅性比較部を更に有し、
前記仕様網羅性比較部は、前記接続情報ファイルと、前記第１の端子情報と、前記回路記述情報とから前記半導体集積回路を構成する回路の接続関係を抽出し、第３の端子情報を生成する
請求項１〜請求項３のいずれか１項に記載の半導体集積回路の検証装置。
【請求項５】
前記フォーマル検証部の検証結果と、前記比較部の比較結果と、前記第３の端子情報から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子、及び、前記接続仕様情報と前記回路記述情報の一致誤差を検証できる
請求項４に記載の半導体集積回路の検証装置。
【請求項６】
半導体集積回路を構成する回路の接続関係を示す接続仕様情報と、前記半導体集積回路の構成を記述した回路記述情報との回路接続関係の一致性を検証する半導体集積回路の検証方法であって、
前記接続仕様情報をアサーション言語で記述された接続情報ファイルに変換し、
前記接続仕様情報からオープンである端子を抽出した第１の端子情報と、前記回路記述情報からオープンである端子の情報を抽出した第２の端子情報とに応じて、前記第１の端子情報と第２の端子情報の一致性を比較し、
前記接続情報ファイルと前記回路記述情報とに応じてフォーマル検証を行い、
前記フォーマル検証の検証結果と、前記第１の端子情報と第２の端子情報の一致性の比較結果とから半導体集積回路を構成する回路の接続関係を検証する
半導体集積回路の検証方法。
【請求項７】
前記フォーマル検証の検証結果と、前記第１の端子情報と前記第２の端子情報の一致性の比較結果から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子を検証できる
請求項６に記載の半導体集積回路の検証方法。
【請求項８】
前記接続情報ファイルと、前記第１の端子情報と、前記回路記述情報とから前記半導体集積回路を構成する回路の接続関係を抽出し、第３の端子情報を生成する
請求項６もしくは請求項７に記載の半導体集積回路の検証方法。
【請求項９】
前記フォーマル検証の検証結果と、前記第１の端子情報と第２の端子情報の一致性の比較結果と、前記第３の端子情報から、前記半導体集積回路を構成する回路の接続関係において、オープンである端子、及び、前記接続仕様情報と前記回路記述情報の一致誤差を検証できる
請求項８に記載の半導体集積回路の検証方法。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図８】
【図９】
【図１０】
【図１１】
【図１２】
【図１３】
【公開番号】特開２０１１−２０３９６２（Ｐ２０１１−２０３９６２Ａ）
【公開日】平成２３年１０月１３日（２０１１．１０．１３）
【国際特許分類】
【出願番号】特願２０１０−７０００５（Ｐ２０１０−７０００５）
【出願日】平成２２年３月２５日（２０１０．３．２５）
【出願人】（３０２０６２９３１）ルネサスエレクトロニクス株式会社 (8,021)
【Ｆターム（参考）】
【公開日】平成２３年１０月１３日（２０１１．１０．１３）
【国際特許分類】
【出願日】平成２２年３月２５日（２０１０．３．２５）
【出願人】（３０２０６２９３１）ルネサスエレクトロニクス株式会社 (8,021)
【Ｆターム（参考）】
[ Back to top ]