検証対象の回路にクロックゲーティング回路を挿入することで前記検証対象の回路の消費電力を低減する効果が得られるか否かを検証するためのアサーション記述を生成するアサーション生成部と、前記アサーション記述に基づいて、前記検証対象の回路の動作を検証するフォーマルシミュレーションを行うシミュレーション部と、前記フォーマルシミュレーションの結果に基づいて、前記検証対象の回路にクロックゲーティング回路を挿入すべきか否かを記述した挿入制約を生成するクロックゲーティング効果制約生成部と、を有することを特徴とする設計支援装置。前記シミュレーション部は、特定の入力信号に対する前記検証対象の回路の動作を検証するダイナミックシミュレーションを実行し、前記ダイナミックシミュレーションの結果によっても前記消費電力を低減する前記効果が得られるか否かが不明な回路に対してのみ前記フォーマルシミュレーションを実行することを特徴とする請求項1に記載の設計支援装置。前記挿入制約に基づいて、前記検証対象の回路を含む回路の論理合成を行う論理合成部をさらに備えることを特徴とする請求項1に記載の設計支援装置。前記アサーション生成部は、前記検証対象の回路に対するイネーブル信号の値がアクティブの論理値に遷移した際に、前記検証対象の回路の出力する信号の値が変化するか否かを検証するアサーション記述を生成することを特徴とする請求項1に記載の設計支援装置。前記検証対象の回路は、前記イネーブル信号に応答して動作する少なくとも一のフリップフロップ、または複数の前記フリップフロップから構成されるレジスタであることを特徴とする請求項4に記載の設計支援装置。検証対象の回路にクロックゲーティング回路を挿入することで前記検証対象の回路の消費電力を低減する効果が得られるか否かを検証するためのアサーション記述をアサーション生成部が生成するステップと、前記アサーション生成部が生成した前記アサーション記述に基づいて、フォーマルシミュレーション部が前記検証対象の回路の動作を検証するフォーマルシミュレーションを行うステップと、前記フォーマルシミュレーションの結果に基づいて、クロックゲーティング効果制約生成部が前記検証対象の回路にクロックゲーティング回路を挿入すべきか否かを記述した挿入制約を生成するステップと、を有することを特徴とする半導体集積回路の設計方法。前記シミュレーション部が、特定の入力信号に対する前記検証対象の回路の動作を検証するダイナミックシミュレーションを実行するステップと、前記シミュレーション部が、前記ダイナミックシミュレーションの結果によっても前記消費電力を低減する前記効果が得られるか否かが不明な回路に対してのみ前記フォーマルシミュレーションを実行するステップと、をさらに有することを特徴とする請求項6に記載の半導体集積回路の設計方法。前記挿入制約に基づいて、論理合成部が前記検証対象の回路を含む回路の論理合成を行うステップをさらに備えることを特徴とする請求項6に記載の半導体集積回路の設計方法。前記アサーション記述は、前記検証対象の回路に対するイネーブル信号の値がアクティブの論理値に遷移した際に、前記検証対象の回路の出力する信号の値が変化するか否かを検証するアサーション記述であることを特徴とする請求項6に記載の半導体集積回路の設計方法。前記検証対象の回路は、前記イネーブル信号に応答して動作する少なくとも一のフリップフロップ、または複数の前記フリップフロップから構成されるレジスタであることを特徴とする請求項9に記載の半導体集積回路の設計方法。検証対象の回路にクロックゲーティング回路を挿入することで前記検証対象の回路の消費電力を低減する効果が得られるか否かを検証するためのアサーション記述を生成するステップと、前記アサーション生成部が生成した前記アサーション記述に基づいて、前記検証対象の回路の動作を検証するフォーマルシミュレーションを行うステップと、前記フォーマルシミュレーションの結果に基づいて、前記検証対象の回路にクロックゲーティング回路を挿入すべきか否かを記述した挿入制約を生成するステップとをコンピュータに実行させるための設計支援プログラム。特許文献1では、テストベクトルに従ったシミュレーション結果を用いてCGセルを挿入するF/Fを決定している。テストベクトルを利用したシミュレーションの場合、特定の動作パタンに対するアクティブ率しか求められない。すなわち、特許文献1の技術では、特定の動作において消費電力の削減効果があると判断できる回路に対してはCGセルを挿入することは有効である。しかし、特定の動作パタンによって消費電力の削減効果が得られるか分からなかった回路に対しては、CGセルを挿入すべきか否かの適切な判断ができない。例えば当該特定の動作パタンの場合には消費電力を低減する効果がなくCGセルを挿入すべきでないと判定できるように見える回路であっても、別の異なる動作パタンの場合にはCGセルを挿入することによって消費電力の低減効果が得られる可能性もあるからである。しかし、テストベクトルを利用して全てのパタンを網羅的にシミュレーションすることは現実的ではない。従って、特許文献1の技術では、回路に特定の動作を実行させた場合の消費電力の削減効果に基づくCGセルの挿入しか行うことができず、回路の消費電力の低減を正確に反映したCGセルの挿入を行うことができないという解決すべき課題が存在する。上記の課題を解決するために、本発明は、以下に述べられる手段を採用する。その手段を構成する技術的事項の記述には、[特許請求の範囲]の記載と[発明を実施するための形態]の記載との対応関係を明らかにするために、[発明を実施するための形態]で使用される番号符号が付加されている。ただし、付加された番号符号は、[特許請求の範囲]に記載されている発明の技術的範囲を限定的に解釈するために用いてはならない。本発明による半導体集積回路の設計支援装置は、アサーション生成部、シミュレーション部、クロックゲーティング効果制約生成部を具備する。アサーション生成部は検証対象の回路にクロックゲーティング回路を挿入することで検証対象の回路の消費電力を低減する効果が得られるか否かを検証するためのアサーション記述を生成する。シミュレーション部は、アサーション記述に基づいて、検証対象の回路の動作を検証するフォーマルシミュレーションを行う。クロックゲーティング効果制約生成部はフォーマルシミュレーションの結果に基づいて、検証対象の回路にクロックゲーティング回路を挿入すべきか否かを記述した挿入制約を生成する。本発明による半導体集積回路の設計方法は、検証対象の回路にクロックゲーティング回路を挿入することで検証対象の回路の消費電力を低減する効果が得られるか否かを検証するためのアサーション記述をアサーション生成部が生成するステップと、アサーション生成部が生成したアサーション記述に基づいて、フォーマルシミュレーション部が検証対象の回路の動作を検証するフォーマルシミュレーションを行うステップと、フォーマルシミュレーションの結果に基づいて、クロックゲーティング効果制約生成部が検証対象の回路にクロックゲーティング回路を挿入すべきか否かを記述した挿入制約を生成するステップとを具備する。上述の半導体集積回路の設計方法は、コンピュータによって実行される設計支援プログラムによって実現されることが好ましい。本発明ではアサーションベース検証によってクロックゲーティングの挿入効果を検証するため、特定の動作パタンを用いずにクロックゲーティングの挿入箇所を決定することができる。従って、本発明によれば、特定の動作パタンに拠らずに、消費電力の低減に効果のないCGセルの挿入を排除することができる。以下、添付図面を参照しながら本発明の実施の形態を説明する。図面において同一、又は類似の参照符号は、同一、類似、又は等価な構成要素を示している。概要本発明による半導体集積回路の設計支援装置以下、設計支援装置と称すは、RTL記述によるDUTDeviceUnderTestにアサーション記述アサーションモニタを追加してフォーマルシミュレーションフォーマル検証とも称すを行い、このシミュレーション結果に基づいて論理合成において挿入するCGセルを決定する。フォーマルシミュレーションでは、アサーションモニタが追加された箇所の動作が、そのアサーション記述によって検証されるため、検証対象箇所の全ての動作を網羅的に検証することができる。このため、特定の動作パタンに拠らずに、挿入するCGセルを論理合成前に決定することが可能となる。構成図1及び図2を参照して、本発明による設計支援装置10の構成を説明する。図1は、本発明による設計支援装置10の実施の形態における構成図である。設計支援装置10は、バス16を介して相互に接続されるCPU11と、RAM12と、記憶装置13と、入力装置14と、出力装置15とを具備する。記憶装置13はハードディスクやメモリ等に例示される外部記憶装置である。又、入力装置14は、キーボードやマウス等のユーザによって操作されることで、各種データをCPU11や記憶装置13に出力する。出力装置15は、モニタやプリンタに例示され、CPU11から出力される半導体装置のレイアウト結果をユーザに対し視認可能に出力する。記憶装置13は、DUT情報20、制約スクリプト30、設計支援プログラム40を格納している。CPU11は、入力装置14からの入力に応答して、記憶装置13内の設計支援プログラム40を実行し、挿入するCGセルの決定CG挿入制約の生成及び論理合成によるネットリストの作成を行う。この際、記憶装置13からの各種データやプログラムはRAM12に一時格納され、CPU11は、RAM12内のデータを用いて各種処理を実行する。尚、CG挿入制約生成処理と論理合成処理は、異なるプログラムや装置によって実現されても構わない。DUT情報20は、RTL記述による設計対象回路DUTである。ここでは、論理合成対象回路のRTL記述がDUT情報20として記録される。DUT情報20は、一般の論理合成で利用されるRTL記述が好適に利用される。制約スクリプト30は、DUTの使用条件や制約を規定したスクリプトである。例えば使用条件としてDUT半導体集積回路の動作環境温度や使用電圧があり、制約としてクロック周波数や遅延値がある。制約スクリプト30も一般の論理合成で利用される使用条件及び制約が定義されたスクリプトが好適に利用される。設計支援プログラム40は、CPU11によって実行されることで、図2に示すアサーション生成部41、シミュレーション部42、CG挿入制約生成部43、論理合成部44の各機能を実現する。アサーション生成部41は、DUT情報20からアサーション検証対象を抽出するとともに、監視対象の動作仕様を定義したアサーション記述アサーションモニタをアサーション言語例示:SVASystemVerilogAssertionやPSLPropertySpecificationLanguageにより生成する。生成されたアサーションモニタはアサーション記述ファイル22として記憶装置13に記録される。シミュレーション部42は、設計者が設定する信号の値やRTL記述を入力として検証対象の回路に信号を入力した場合の出力を設計者に通知する論理シミュレータや、検証対象となる回路の消費電力の値を出力して設計者に通知する消費電力解析ツールといったプログラムがCPU11によって実行されることで実現される。また、後述するが、シミュレーション部42は、フォーマル検証フォーマルシミュレーションを行っても良い。この場合、シミュレーション部42は、CPU11がフォーマル検証ツールを実行することで、フォーマル検証を実行するハードウェア資源として機能する。フォーマル検証は、上述した論理シミュレータや消費電力解析ツールとは異なり、設計者が指定した特定の信号値に基づいてその特定の信号値に対応した信号値を出力結果とするのではない。すなわちフォーマル検証は、検証の対象となっている回路のRTL記述から当該回路が出力する可能性がある結果を数学的に解析して証明するものである。例えばシミュレーション部42は、RTL記述から検証対象となっている回路の状態遷移図を導き出し、その状態遷移図を追っていくことで当該回路の出力となるあらゆる組み合わせを導き出す。すなわち、フォーマル検証は、上記した論理シミュレータや消費電力解析ツールとは異なり、設計者が指定する信号値に依存しない網羅的な解析結果が得られることを特徴としている。なお、以下、本明細書では、検証対象の回路の具体例としてフリップフロップ、あるいは複数のフリップフロップから構成されるレジスタが例示されるが、検証対象の回路はこれに限らず、そのほかの回路であってもよい。シミュレーション部42は、アサーションモニタをDUT情報20に挿入することでシミュレーション用のDUT情報を生成し、当該DUT情報に対してフォーマルシミュレーションを行う。シミュレーション部42は、フォーマルシミュレーションの前に所定のテストパタンに従ったダイナミックシミュレーションを行っても良い。ここで、ダイナミックシミュレーションとは、上述した論理シミュレータによって実行されるシミュレーションのこと意味しており、検証対象の回路が設計者によって指定された信号値に応じてどのような信号値を出力するかを解析する。この点については第2の実施の形態で述べる。CG挿入制約生成部43は、フォーマルシミュレーション結果に基づいてDUTに挿入するCGセルを設定するDUTへの挿入を禁止するCGセルを設定する。あるいは、CG挿入制約生成部43は、フォーマルシミュレーション結果に基づいてDUTに挿入するCGセルの位置を設定するDUTへの挿入を禁止するCGセルの位置を設定する。CG挿入制約生成部43は、この設定に基づきDUTに挿入するDUTへの挿入を禁止するCGセル制約スクリプトを生成し、CG挿入制約スクリプト24として記憶装置13に記録する。論理合成部44は、一般的な論理合成ツールと同様に、DUT情報20RTL記述を解析して論理式に変換しネットリスト25を生成する。この際、制約スクリプト30やCG挿入制約スクリプト24に従い、回路の最適化例えば論理圧縮や回路面積の縮小を行う。本発明では、CG挿入制約スクリプト24に従う最適化により、低消費電力化に不要なCGセルが削除されるあるいは、低消費電力化に必要なCGセルのみが選択的に挿入される。以上のような構成により、本発明による設計支援装置10は、アサーション記述アサーションモニタを挿入したDUT情報RTL記述を用いてフォーマルシミュレーションを行い、この結果に基づいて低消費電力化に不要なCGセルを排除するための制約を生成する。又、論理合成において、この制約を利用することで、低消費電力化に不要なCGセルを排除したネットリストを作成することが可能となる。動作第1の実施の形態以下、図3Aから図8を参照して、本発明による半導体集積回路の設計方法の第1の実施の形態を説明する。図3A及び図3Bは、本発明による半導体集積回路の設計方法の一例を示すフロー図である。アサーション生成部41は、先ず、DUT情報20を解析してアサーションモニタの挿入箇所となるアサーション検証ポイントを特定するステップS101。詳細には、アサーション生成部41は、DUT情報20を解析してアサーションモニタを挿入する箇所、すなわちアサーション記述によって動作を検証する箇所アサーション検証ポイントを特定する。本発明では、論理合成においてCGセルが挿入され得る箇所が監視ポイントとなる。このため、アサーション生成部41は、論理合成においてCGセルを挿入する条件となるクロックゲーティング条件例えばイネーブル信号をアサーション検証ポイントとして特定する。ステップS101において特定されたアサーション検証ポイントは検証ポイント情報21として記憶装置13に記録される。図4は、本発明による検証ポイント情報21の構造の一例を示す図である。論理合成部44では、クロック信号、イネーブル信号、レジスタ又はF/FによってCGセルを挿入する箇所を特定する。このため、アサーション生成部41は、DUT情報20から少なくともクロック信号、イネーブル信号、レジスタ又はF/Fを示す情報クロック識別子211、イネーブル識別子212、レジスタ識別子213を抽出し、それぞれを対応付けて検証ポイント情報21として記録する。尚、検証ポイント情報21としては、少なくともイネーブル信号とレジスタ又はF/Fの組合せが抽出されればよいため、クロック識別子211は省略され得る。例えば、検証ポイント情報21の抽出ツールとして、一般的な消費電力解析ツールが好適に利用される。具体的には、アトレンタ社によるSpyGlass-Powerツールが利用される。そのためにまずCPU11は上述した論理シミュレータの機能を実現するため、記憶装置13にアクセスして設計支援プログラム40の内の論理シミュレータを読み出し実行する。当該実行によりシミュレーション部42は、設計者が指定した信号値およびRTL記述に基づいて、検証対象である回路、例えばイネーブル信号に基づき動作するレジスタの出力結果を得る。次にCPU11は、記憶装置13から設計支援プログラム40内に含まれる消費電力解析ツール、例えば上述のSpyGlass-Powerツールを読み出して実行する。シミュレーション部42は、論理シミュレータの実行結果を入力とし、検証対象の回路の消費電力の解析を行う。ここで、消費電力解析ツールの実行によって作成される消費電力結果には、イネーブル信号と、これに関連するレジスタ及び当該レジスタに入力されるクロック信号が示される。消費電力解析ツールは、レジスタの動作率Duty-Cycleに関わらずDUTにおける全てのイネーブル信号と関連するレジスタの組合せを抽出するため、本発明における検証ポイント情報21の抽出ツールとして好適に利用され得る。アサーション生成部41は、このようなツールを利用することで、DUT情報20から検証ポイント情報21を網羅的に抽出することができる。シミュレーション部42は、例えば消費電力解析ツールの実行結果を記憶装置13に書き込んで記憶させると共に、出力装置15を介して出力し、設計者に当該実行結果を通知する。図5は、SpyGlass-Powerツールによって得られた消費電力結果ログの一例を示す図である。図5を参照して、消費電力結果ログには、クロック信号Clock及びイネーブル信号Enableに関連するレジスタのサイズRegisterwidth、動作率Duty-CycleEnable、有効クロックActivityClock、ゲーティングがない場合の消費電力Powerw/ogating、ゲーティングされた場合の消費電力Powergating、ゲーティング有無間の消費電力差PowerDifference、モジュール階層レジスタ位置Hierarchy、レジスタ識別子RegistersAffectedが、記録されている。ここで、上段の行のレジスタ識別子には、r1_reg[0:35]と記載され、下段の行のレジスタ識別子にはr3_reg[0:35]と記載されている。これらはそれぞれレジスタの名称を意味しており、この例ではr1というレジスタは36ビットの値を記憶可能であることになる。具体的にはレジスタr1は、1ビットの記憶素子であるフリップフロップF/Fを36個有する。r3という名称のレジスタについても同様である。これらのF/Fのそれぞれには、イネーブル信号が入力されている。なお、このレジスタ識別子に記載されている回路が、消費電力解析ツールが検証対象としている回路になる。以下では具体例として、これらのレジスタが検証対象の回路であるとして説明する。図5における、クロック信号Clockとは、例えば半導体集積回路内に設けられたPLL等の発振回路が出力したクロック信号であり、クロックツリーを介して半導体集積回路内の各回路に伝達される。図5ではmc_top.clk_i211の記載が2ヶ所ある。mc_top.clk_iはクロック信号の名称である。したがって、これらの同一名称のクロック信号はそれぞれ周波数が同一であり、クロックスキューがなければ同位相でトグルするクロック信号である。この例では、レジスタr1とレジスタr3に入力されるクロックは共にmc_top.clk_i211であり、同じクロック信号がそれぞれのレジスタの各F/Fに入力されていることになる。動作率Duty-CycleEnableの列には、上段の行に0.00、下段の行に1.00と記載されている。ここで、クロックゲーティング回路にはクロック信号とイネーブル信号が入力される。イネーブル信号がアクティブである場合にはゲーティング回路はクロック信号のパルスを後段の回路に出力し、イネーブル信号がインアクティブであればゲーティング回路はパルスを出力しない。このようなクロックゲーティング回路の最も簡単な例はクロック信号とイネーブル信号を入力する2入力のANDゲートである。そして動作率Duty-CycleEnableの値が0.00であれば、このイネーブル信号がシミュレーション電源解析シミュレーションを実行している間、常にインアクティブであることを示し、1.00であれば、当該イネーブル信号がシミュレーション電源解析シミュレーションを実行している間、常にアクティブであることを意味する。なお、図5では動作率の値として0.00と1.00の2種類の値しか示されていないが、実際には0.3、0.5、0.7といった値であってもよい。そしてこの動作率の値は、CPU11が消費電力解析シミュレーションの前に実行した論理シミュレータに対する入力であり、設計者が設定した信号値である。また、上段の行、すなわちレジスタr1に入力されるイネーブル信号はenable1であり、下段の行、すなわちレジスタr3に入力されるイネーブル信号はenable2であることが分かる。名称が異なるため、これらは別々のイネーブル信号である。なお、イネーブル信号は、回路構成上、複数の論理回路の論理演算の結果として生成される場合がある。例えばenable1は、実際の半導体集積回路では、メモリに対するアドレスを指定する信号の1ビットと、ライトイネーブル信号のAND演算の結果として生成されることもある。enable2についても同様である。図5における有効クロックActivityClockは、検証対象となっている回路、この説明では具体例としてレジスタr1とr3に実際に入力されているクロック信号の周波数を示す。図5の例ではレジスタr1もレジスタr3もそれぞれ2.00の値が示されている。有効クロックの値が2.00の場合、レジスタr1とr3を含む半導体集積回路中の最大の周波数がレジスタr1とr3に入力されていることを意味する。また、有効クロックの値が1.00の場合には上記した最大の周波数の1/2の周波数が検証対象の回路に入力されることになる。ゲーティングがない場合の消費電力Powerw/ogatingに関しては、レジスタr1、r3共に186μWの電力を消費していることが分かる。一方、ゲーティングされた場合の消費電力Powergatingを見ると、レジスタr1は18.7μWの電力を消費しているのに対し、レジスタr3は800μWの電力を消費している。これは、レジスタr1は動作率Duty-CycleEnableの値が0.00であるため、ゲーティング回路を挿入することで効果的に電力消費を抑制できることを意味している。一方、レジスタr3は、動作率の値が1.00であり、イネーブル信号が常にアクティブであるため、ゲーティング回路を挿入してもレジスタr3が消費する電力にゲーティング回路自体が消費する電力が上乗せされてしまうため、値が800μWに上昇しているのである。ゲーティング有無間の消費電力差PowerDifferenceはゲーティングがない場合の消費電力Powerw/ogatingとゲーティングされた場合の消費電力Powergatingの差分である。モジュール階層レジスタ位置Hierarchyはモジュールの名称を記載しており、レジスタr1やr3が属するモジュール名がこの記載で分かる。消費電力解析ツールでは、従来技術と同様にテストパタンを利用した消費電力シミュレーションを行っているため、検証対象の回路が消費する電力の値等の具体的なシミュレーション結果は本発明では利用しない。しかし、本発明によるアサーション生成部41は、消費電力解析ツールの実行の結果として抽出されたクロック識別子211、イネーブル識別子212、レジスタ識別子213を検証ポイント情報21に使用する。例えば、アサーション生成部41は、図5に示す消費電力解析結果から、図6に示す検証ポイント情報21を抽出する。ここでは、クロック識別子211mc_top.clk_i、イネーブル識別子212enable1、レジスタ識別子213r1_reg[0:35]の組合せと、クロック識別子211mc_top.clk_i、イネーブル識別子212enable2、レジスタ識別子213r3_reg[0:35]の組合せが、検証ポイント情報21として抽出される。尚、レジスタ位置を特定するモジュール階層Hierarchyも検証ポイント情報21として抽出されても構わない。図5に示す一例では、レジスタr1_reg[0:35]の位置を示すmc_top.u3.u0、レジスタr3_reg[0:35]の位置を示すmc_top.u3.u0がそれぞれ検証ポイント情報21として抽出されても良い。本実施例では、一般の消費電力解析ツールを利用した検証ポイント情報21の抽出方法を一例としたが、DUT情報20から全てのイネーブル信号とこれに関連するレジスタとの組合せを抽出できればこれに限らない。上記の消費電力解析ツールを使用した検証ポイント情報21の抽出は一例であり、請求項の記載を消費電力解析ツールの結果を用いることに限定しなくても、本発明は明確に理解されるところである。続いて、アサーション生成部41は、検証ポイント情報21を利用してCG効果チェック用アサーションを生成するステップS102。ここでのCG効果チェック用アサーションとは、より大略的には、検証対象の回路にクロックゲーティング回路を挿入することで検証対象の回路の消費電力を低減する効果が得られるか否かを検証するためのアサーション記述を意味する。CG効果チェック用アサーションには、CGセルによる低電力化効果を検証するために、イネーブル信号に応じた関連レジスタの動作仕様期待動作が規定される。CGセルによる低電力化効果は、イネーブル信号の発生信号変化に応じて、関連レジスタの出力が発生信号変化するか否かによって検証できる。明確に述べれば、イネーブル信号の信号値が遷移してアクティブの論理値に変化した場合に、検証対象となっているレジスタの各F/Fが出力する信号値が変化する否かを検証することで、各F/Fがゲーティング回路を挿入することで効果的に消費電力を削減可能であるかを検証できる。アサーションベース検証は、レジスタの各F/Fに、個別に行われるがレジスタ全体を検証の対象としてもよい。なお、以下では分かりやすさのため、それぞれのF/Fごとに検証を行うとして、具体的に説明していく。また、アクティブの論理値とは、回路が正論理であればハイレベル1の論理値を意味し、回路が負論理であればローレベル0の論理値を意味する。例えば、イネーブル信号がアクティブの論理値に遷移しても、そのイネーブル信号に対応するレジスタの各F/Fの出力する信号の値が変化しない場合、各F/Fに対するゲーティング効果が期待できない。この場合、当該レジスタの当該各F/Fに対するクロックゲーティングによる低電力効果は期待できない以下、CG効果なしと称すと判定できる。あるいは、イネーブル信号の信号値がアクティブの論理値に遷移することに応じて対応するレジスタの各F/Fが出力する信号の値が変化する場合、ゲーティングすることで当該各F/Fの動作を停止できる。この場合、当該レジスタに対するクロックゲーティングによる低電力効果は期待できる以下、CG効果ありと称すと判定できる。アサーションベース検証はF/Fごとに行うため、イネーブル信号に対応するレジスタを構成するF/Fの内の少なくとも一つ以上の一部分のF/Fの出力値は変化せず、他の部分のF/Fの出力値は変化するというケースもある。その場合、出力値が変化しなかった当該一部分のF/Fにはゲーティング回路を挿入しても電力消費を抑制する効果がなく、他の部分のF/Fにはゲーティング回路を挿入することで電力消費を抑制する効果がある、と判定できる。なお、イネーブル信号がアクティブの論理値に遷移しても出力値が変化しないF/Fとは、例えば設計において冗長に設けられ、実際の回路の動作では使用されることがない、あるいは使用される頻度が少ないようなレジスタである。具体例を挙げると、カウンタ回路を構成する各F/Fが考えられる。半導体集積回路の新製品を開発する場合には前製品で使用した機能回路を流用することで、開発期間を短縮することが行われる。このとき、新製品では前製品で搭載されていたカウンタ回路がカウントする桁数よりも少ない桁数までのカウントを繰り返せば問題ない場合が考えられる。その場合、新製品でのカウンタ回路の上位ビットの値を保持するF/Fは常に0の論理値を保持し、保持する値が0から1へ遷移することはない。このようなF/Fには、クロックゲーティング回路を挿入する必要はなく、挿入すればゲーティング回路が消費する電力によるチップ全体としての消費電力の増加と、チップ面積の増加を招くことになる。上記の例以外にも、回路の動作上、固定の信号値の制御信号がそのF/Fから出力される必要があり、常に固定値を保持するF/Fが存在する場合なども考えられる。本発明は、このようなF/Fに対する不要なゲーティング回路の挿入を防止するものである。図7は、本発明によるアサーション記述の一例を示す図である。アサーション記述AST1では動作条件としてイネーブル信号Enableenable1がアクティブの論理に遷移することが規定され、期待動作期待仕様としていつかはレジスタr1_reg[0]の出力する信号の値が変化することが規定されている。AST1は、レジスタr1の0ビット目のF/Fに対し、ゲーティング効果があるか否かを判定するための記述である。ここで、インプリケーション演算子|=>は、先行する左辺シーケンス条件が成立した場合に、プロパティの検証右辺が行われることを意味し、ここでは、イネーブル信号enable1がアクティブの論理に遷移することが条件として規定される。又、右辺のサイクルカウント[0:]は、レジスタr1_reg[0]が出力する信号値の変化までの時間を示し、ここでは無限の時間が規定されている。AST2についても同様であり、36ビットのレジスタr1に対してアサーション生成部41は、AST1からAST36をアサーション記述として生成する。図7に示す一例では、イネーブル信号の信号値の遷移からレジスタの出力信号の値の遷移までの期間を無限として規定しているが、これに限らず、所定の期間を指定しても構わない。作成されたアサーション記述アサーションモニタは、検証ポイント情報21に紐付けられてアサーション記述ファイル22として記憶装置13に記録される。シミュレーション部42は、アサーション生成部41が生成したアサーション記述に基づいて、検証対象の回路の動作を検証するフォーマルシミュレーションを行う。具体的には、シミュレーション部42は、DUT情報20、検証ポイント情報21、アサーション記述ファイル22を利用してDUTに対してフォーマルシミュレーションを実行するステップS103。詳細には、CPU11が記憶装置13にアクセスし、設計支援プログラム40に含まれるフォーマル検証ツールを記憶装置13から読み出して実行する。CPU11がフォーマル検証ツールを実行することによって、CPU11はフォーマル検証を実行するシミュレーション部42となる。シミュレーション部42は、一例としてDUT情報20にアサーション記述ファイル22を挿入し、シミュレーション用のDUT情報を作成する。この際、シミュレーション部42は、記憶装置13から読み出したアサーション記述ファイル22から抽出したアサーション記述を、当該アサーション記述に紐付けられた検証ポイント情報21に挿入する。これにより、ゲーティング効果を検証するためのアサーションモニタが、ステップS101において特定されたDUT情報20における検証ポイントに挿入されることとなる。シミュレーション部42は、アサーション記述が挿入されたDUT情報を用いてフォーマルシミュレーションを実行する。ここで実行されるフォーマル検証は、例えば、一般的なプロパティチェッキング方法により実現できる。すなわち、本発明では、上述したアサーション記述に基づいて検証対象の回路をフォーマル検証によって検証する。フォーマル検証は、上述したように設計者が検証対象の回路に特定の入力信号を与える手法ではなく、回路のあらゆる出力結果を状態遷移図に基づくなどの手法により数学的に証明していくものだからである。具体的に言えば、本実施の形態では、フォーマル検証によって導かれる各F/Fの出力値あるいはレジスタの出力値を、上述したアサーション記述に基づいて検証するのである。つまり、フォーマル検証の結果から、イネーブル信号の信号値が遷移してアクティブの論理値に変化したとき、検証対象となっているレジスタ、あるいはレジスタを構成する各F/Fが出力する信号値が変化する否かを検証するのである。これによって、特定の入力パタンに対応した限定的な出力結果による判断ではない検証が実現できる。なお、アサーション記述は、DUT情報20に挿入されなくてもよい。この場合、フォーマル検証を実行するシミュレーション部42にDUT情報20とアサーション記述が別々に入力される。シミュレーション部42は、検証対象の回路であるレジスタr1の出力値、あるいはレジスタr1を構成する各F/Fの出力値が、当該レジスタr1または各F/Fに入力されるイネーブル信号がアクティブの論理に遷移した場合に変化するかを、フォーマル検証によって検証する。次に、CPU11は、記憶装置13から設計支援プログラム40を読み出して実行することで、CG効果判定を行う。この場合、CPU11は、フォーマルシミュレーションの結果に基づいて、検証対象の回路にクロックゲーティング回路を挿入すべきか否かを記述した挿入制約を生成するクロックゲーティング効果制約生成部となる。より具体的には、設計支援プログラム40が実行されることによってCPU11がCG挿入制約生成部43となってCG効果判定を実現する。CG挿入制約生成部43は、フォーマルシミュレーション結果に基づいて、CG効果判定を行うステップS104。ここでは、アサーション検証された検証ポイント毎にCG効果判定が行われる。例えば、複数のF/Fを備えるレジスタの全体を検証ポイントとした場合、レジスタ全体についてCG効果判定が行われ、複数のF/Fのそれぞれを検証ポイントとした場合、F/F毎にCG効果判定が行われる。例えば、イネーブル信号enable1がアクティブの論理値に変化しても、レジスタF/Fr1_reg[0:1]の出力が変化しない場合、CG挿入制約生成部43は、レジスタF/Fr1_reg[0:1]に対してCG効果なしと判定する。あるいは、イネーブル信号enable1が変化すると、レジスタr1_reg[0:1]の出力が変化する場合、CG挿入制約生成部43は、レジスタF/Fr1_reg[0:1]に対してCG効果ありと判定する。CG挿入制約生成部43は、ステップS104のCG効果判定結果に応じてCGセルを挿入するレジスタF/F又はCGセルの挿入を禁止するレジスタF/Fを、CG効果レジスタファイル23として記憶装置13に記録するステップS105。ここでCG挿入制約生成部43は、CG効果ありと判定したレジスタF/Fを、CGセルの挿入するレジスタとしてCG効果レジスタファイル23に記録する。あるいは、CG挿入制約生成部43は、CG効果なしと判定したレジスタF/Fを、CGセルの挿入を禁止するレジスタとしてCG効果レジスタファイル23に記録し、記憶装置13に書き込む。記憶装置13は当該CG効果レジスタファイル23を記憶する。CG挿入制約生成部43は、CG効果レジスタファイル23に基づいて、CG挿入制約スクリプト24を作成するステップS106。CG挿入制約スクリプト24は、論理合成時にCGセルの挿入制約として利用される。CG挿入制約スクリプト24には、CGセルを挿入するレジスタF/Fを特定する情報、あるいは、CGセルの挿入を禁止するレジスタF/Fを特定する情報が含まれる。論理合成部44は、DUT情報20、制約スクリプト30、CG挿入制約スクリプト24に基づいて、論理合成を行い、DUTに対するネットリスト25を生成するステップS107。論理合成部44は、CG挿入制約スクリプト24に応じてCGセルを選択的に挿入、あるいは不用なCGセルの挿入を排除する。これにより、レジスタのビット幅に応じた数のCGセルの自動挿入に比べて、挿入するCGセル数を低減することが可能となる。図8から図10を参照して、本発明による設計方法によるCGセルの削減効果について説明する。図8は、本発明によるCG挿入制約スクリプト24を利用しない場合の論理合成結果ネットリストの一例を示す図である。図8を参照して、レジスタ100は、クロック識別子211mc_top.clk_iイネーブル識別子212enable1、レジスタ識別子213r1_reg[0:4]で特定される4ビットのレジスタであり、F/F111、112、113、114を備える。ここで、CG挿入制約スクリプト24を利用せず、最大3つのF/Fを駆動可能なCGセルを挿入する場合、レジスタ100に対して少なくとも2つのCGセルが挿入されることとなる。例えば、図8で示すように、論理合成においてF/F111、112に対してCGセル122が挿入され、F/F113、114に対してCGセル121が挿入される。一方、本発明によるCG挿入制約スクリプト24に応じて論理合成した場合、イネーブル信号が変化しても出力変動しないレジスタF/FへのCGセルの挿入が禁止されるため、レジスタ100へ挿入されるCGセルの数を削減することができる。図9は、本発明によるCG挿入制約スクリプト24を利用した場合の論理合成結果ネットリストの一例を示す図である。ここでは、CG挿入制約スクリプト24によってF/F111へのCGセルの挿入が禁止された場合の論理合成結果の一例が示される。レジスタ100の構造、及びCGセルの駆動能力が図8に示す一例と同じ条件である場合、論理合成においてF/F111以外のF/F112~114に対して1つのCGセル120が挿入される。図9の一例では、図8に比べてCGセルが1つ削減されることとなる。このように、CGセルの挿入をF/F毎に制御することで、レジスタに対して挿入するCGセルの数を削減することができる。図10は、本発明によるCG挿入制約スクリプト24を利用した場合の論理合成結果ネットリストの他の一例を示す図である。ここでは、CG挿入制約スクリプト24によってレジスタ100全体へのCGセルの挿入が禁止された場合の論理合成結果の一例が示される。この場合、レジスタ100に対してCGセルは挿入されないため、図8に比べてCGセルが2つ削減されることとなる。以上のように、本発明によれば、アサーションベース検証によってCG効果のないレジスタ又はF/Fを特定し、当該レジスタ又はF/FへのCGセルの挿入を禁止することで、論理合成時に挿入され得る不要なCGセルを排除することができる。このように、無駄なCGセルの挿入を排除することで、半導体集積回路の回路面積を低減することができる。又、無駄なCGセルを削減することで、配線混雑も低減されるためレイアウト処理が容易となる。更に、低電力化に効果のないCGセルを排除しながら論理合成できるため、CGセル削減のための後戻り処理が不要となりレイアウト半導体集積回路の設計TATを短縮することができる。第2の実施の形態次に、図11A及び図11Bを参照して、本発明による半導体集積回路の設計方法の第2の実施の形態を説明する。第2の実施の形態では、ステップS103におけるフォーマルシミュレーションの前に、ユーザの仕様に応じたテストパタンによるダイナミックシミュレーションを行うことで、フォーマルシミュレーション対象となる検証ポイントを絞り込むことができる。図11A及び図11Bは、ダイナミックシミュレーションを併用した本発明による設計方法の一例を示すフロー図である。図11Aを参照して、アサーション生成部41は、図3Aに示す動作と同様のステップS101、ステップS102の処理によりアサーション記述ファイル22を生成する。本一例のシミュレーション部42は、シミュレーション部42が、特定の入力信号に対する検証対象の回路の動作を検証するダイナミックシミュレーションを実行し、ダイナミックシミュレーションの結果によっても消費電力を低減する効果が得られるか否かが不明な回路に対してのみフォーマルシミュレーションを実行する。具体的には、フォーマルシミュレーションの前に、DUT情報20、検証ポイント情報21、アサーション記述ファイル22、テストパタン図示なしを利用して、DUTに対してダイナミックシミュレーションを実行するステップS201。詳細には、CPU11が、記憶装置13に記憶されている論理シミュレータを読み出し実行する。当該論理シミュレータが実行されることによってCPU11が実現するシミュレーション部42は、DUT情報20にアサーション記述ファイル22を挿入し、シミュレーション用のDUT情報を作成する。この際、シミュレーション部42は、アサーション記述ファイル22から抽出したアサーション記述を、当該アサーション記述に紐付けられた検証ポイント情報21に挿入する。これにより、ゲーティング効果を検証するためのアサーションモニタが、ステップS101において特定されたDUT情報20における検証ポイントに挿入されることとなる。シミュレーション部42は、アサーション記述が挿入されたDUT情報20とテストパタンを入力として、検証対象のレジスタあるいはF/Fに対するダイナミックシミュレーションを実行する。シミュレーション部42は、ダイナミックシミュレーション結果に基づいてCG効果を判定するステップS202。ここでは、テストパタンに応じてアサーション検証された検証ポイント毎にCG効果判定が行われる。このため、判定結果は、テストパタンに応じた検証ポイントに対する判定結果となる。シミュレーション部42は、当該判定結果を記憶装置13に書き込む。ステップS202において、CG効果ありと判定された検証ポイントレジスタは、少なくともテストパタンに応じた動作時においてCG効果があるため、フォーマルシミュレーションせずともCGセルの挿入対象と設定され得る。このため、シミュレーション部42は、ダイナミックシミュレーションの結果として得られた前記判定結果を記憶装置13から読み出し、ダイナミックシミュレーションで効果有りと判定された検証ポイントレジスタをアサーション検証対象から外して、次工程であるフォーマルシミュレーションを実行するステップS103。図11Bに示すステップS103~S107までの処理は、図3A及び図3Bと同様であるが、本一例では、ダイナミックシミュレーション結果に応じてアサーション検証の対象となるレジスタF/Fを検証対象から除外してフォーマルシミュレーションを実行する。換言すると、ダイナミック検証の結果に応じて絞り込まれたアサーション記述のみがDUT情報20に追加され、当該DUT情報に対してフォーマルシミュレーションが行われる。フォーマルシミュレーションでは、絞りこまれたアサーション記述アサーションモニタのみを検証すればよいため、検証時間の短縮化が期待できる。尚、ダイナミックシミュレーションで利用するアサーション記述アサーションモニタとフォーマルシミュレーションで利用するアサーション記述アサーションモニタは、CG効果判定ができれば、同一の動作条件及び動作仕様が規定されても、異なる動作条件及び動作仕様が規定されてもどちらでも良い。例えば、イネーブル信号が変化した場合、レジスタ出力が変化するを規定したアサーション記述をダイナミックシミュレーションで利用し、イネーブル信号が変化しても、レジスタ出力は変化しないを規定したアサーション記述をフォーマルシミュレーションで利用してもよい。この場合、ダイナミックシミュレーションにおいて、イネーブル信号が変化したときにレジスタ出力が変化するレジスタは、CG効果ありのため、フォーマル検証対象から除外される。以上、本発明の実施の形態を詳述してきたが、具体的な構成は上記実施の形態に限られるものではなく、本発明の要旨を逸脱しない範囲の変更があっても本発明に含まれる。上述した一例では、アサーション生成部41は、アサーション検証ポイントを特定するための論理シミュレータや消費電力解析ツールの機能を有していたが、これに限らず、他の装置において出力された消費電力解析結果を利用して、検証ポイント情報21を取得してもよい。すなわち、設計支援プログラム40には、論理シミュレータや消費電力解析ツールが含まれなくてもよい。