(57)【要約】【課題】回路の論理検証の作業効率を向上させる。【解決手段】信号線認識部１１は、信号線を選択するデコーダを含む回路群の設計情報を基に、信号線を認識する。デコーダ認識部１２は、認識された記各信号線を始点としてそれより入力側の論理素子を、設計情報を基に順次認識し、論理値１を出力する論理積ゲートとして動作する論理素子とインバータとから構成される領域をデコーダ回路領域として認識するとともに、始点とした信号線の論理値を１としたときのデコーダ回路領域への入力信号の論理値を判別する。判定部１３は、デコーダ回路領域への入力信号の数と、各信号線を始点としてそれぞれ認識されたデコーダ回路領域の間での入力信号の論理値の組み合わせとを基に、デコーダ回路領域の論理構成が正しいか否かを判定する。【選択図】図１
2010055212.tif 000002
【特許請求の範囲】
【請求項１】
入力された選択信号をデコードして複数の信号線のうちの１本を選択するデコーダを含む回路群の論理検証を行う論理検証方法において、
信号線認識部が、前記回路群を記述した設計情報を基に前記信号線を認識し、
デコーダ認識部が、認識された前記各信号線を始点としてそれより入力側の論理素子を前記設計情報を基に順次認識し、論理値１を出力する論理積ゲートとして動作する論理素子とインバータとから構成される領域をデコーダ回路領域として認識するとともに、始点とした前記信号線の論理値を１としたときの当該デコーダ回路領域への入力信号の論理値を判別し、
判定部が、前記デコーダ回路領域への入力信号の数と、前記各信号線を始点としてそれぞれ認識された前記デコーダ回路領域の間での入力信号の論理値の組み合わせとを基に、前記デコーダ回路領域の論理構成が正しいか否かを判定する、
ことを特徴とする論理検証方法。
【請求項２】
前記判定部による論理構成の判定処理では、前記各信号線を始点としてそれぞれ認識された前記デコーダ回路領域への入力信号の数が、前記信号線を選択するために必要な前記選択信号のビット数と一致し、なおかつ、前記各信号線を始点としてそれぞれ認識された前記デコーダ回路領域の間で入力信号の論理値がすべて異なる場合に、前記デコーダ回路領域の論理構成が正しいと判定し、それ以外の場合には当該デコーダ回路領域の論理構成が正しくないと判定することを特徴とする請求項１記載の論理検証方法。
【請求項３】
前記デコーダは、ｎビット（ただし、ｎは自然数）の前記選択信号をデコードして２n本の前記信号線のうちの１本を選択することを特徴とする請求項２記載の論理検証方法。
【請求項４】
前記デコーダ認識部による前記デコーダ回路領域の認識処理では、論理値フラグを初期値として１に設定して、前記各信号線を始点としてそれより入力側の論理素子を順次認識し、論理素子としてインバータを認識すると、前記論理値フラグの値を反転させ、前記デコーダ回路領域の境界を認識した時点での前記論理値フラグの値を、当該境界から入力される入力信号の論理値と判別することを特徴とする請求項１〜３のいずれか１項に記載の論理検証方法。
【請求項５】
前記デコーダ認識部による前記デコーダ回路領域の認識処理では、論理素子として論理積ゲートを認識した場合、前記論理値フラグが１であれば、当該論理積ゲートの入力側の論理素子の認識処理を当該論理積ゲートの入力端子ごとにさらに続行し、前記論理値フラグが０であれば、当該論理積ゲートの出力ノードを前記デコーダ回路領域の境界として認識するとともに、この時点での前記論理値フラグの値を、当該境界から入力される入力信号の論理値と判別することを特徴とする請求項４記載の論理検証方法。
【請求項６】
前記デコーダ認識部による前記デコーダ回路領域の認識処理では、論理素子として論理和ゲートを認識した場合、前記論理値フラグが０であれば、当該論理和ゲートの入力側の論理素子の認識処理を当該論理和ゲートの入力端子ごとにさらに続行し、前記論理値フラグが１であれば、当該論理和ゲートの出力ノードを前記デコーダ回路領域の境界として認識するとともに、この時点での前記論理値フラグの値を、当該境界から入力される入力信号の論理値と判別することを特徴とする請求項５記載の論理検証方法。
【請求項７】
論理検証の対象とする前記回路群が、アレイ状に配列された単位回路のうちの任意の単位回路を前記信号線によって選択するアレイ回路を含む場合に、前記信号線認識部による前記信号線の認識処理では、前記設計情報を基に前記単位回路を認識し、認識した前記単位回路同士の接続状態を検証することで、前記信号線を認識することを特徴とする請求項１〜６のいずれか１項に記載の論理検証方法。
【請求項８】
前記回路群は、前記単位回路としてメモリセルがアレイ状に配列された半導体メモリを含むことを特徴とする請求項７記載の論理検証方法。
【請求項９】
前記判定部による論理構成の判定処理では、前記各信号線を始点としてそれぞれ認識された前記デコーダ回路領域の間で同一の論理値をとる入力信号を除外した後、残りの入力信号の数とその論理値とを基に前記デコーダ回路領域の論理構成が正しいか否かを判定することを特徴とする請求項１〜８のいずれか１項に記載の論理検証方法。
【請求項１０】
入力された選択信号をデコードして複数の信号線のうちの１本を選択するデコーダを含む回路群の論理検証を行う論理検証装置において、
前記回路群を記述した設計情報を基に前記信号線を認識する信号線認識部と、
認識された前記各信号線を始点としてそれより入力側の論理素子を前記設計情報を基に順次認識し、論理値１を出力する論理積ゲートとして動作する論理素子とインバータとから構成される領域をデコーダ回路領域として認識するとともに、始点とした前記信号線の論理値を１としたときの当該デコーダ回路領域への入力信号の論理値を判別するデコーダ認識部と、
前記デコーダ回路領域への入力信号の数と、前記各信号線を始点としてそれぞれ認識された前記デコーダ回路領域の間での入力信号の論理値の組み合わせとを基に、前記デコーダ回路領域の論理構成が正しいか否かを判定する判定部と、
を有することを特徴とする論理検証装置。
【請求項１１】
入力された選択信号をデコードして複数の信号線のうちの１本を選択するデコーダを含む回路群の論理検証を行うための論理検証プログラムにおいて、
コンピュータを、
前記回路群を記述した設計情報を基に前記信号線を認識する信号線認識部、
認識された前記各信号線を始点としてそれより入力側の論理素子を前記設計情報を基に順次認識し、論理値１を出力する論理積ゲートとして動作する論理素子とインバータとから構成される領域をデコーダ回路領域として認識するとともに、始点とした前記信号線の論理値を１としたときの当該デコーダ回路領域への入力信号の論理値を判別するデコーダ認識部、
前記デコーダ回路領域への入力信号の数と、前記各信号線を始点としてそれぞれ認識された前記デコーダ回路領域の間での入力信号の論理値の組み合わせとを基に、前記デコーダ回路領域の論理構成が正しいか否かを判定する判定部、
として機能させることを特徴とする論理検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、回路の論理検証を行う論理検証方法、その方法を実現する論理検証装置、および論理検証プログラムに関する。
【背景技術】
【０００２】
近年、ＬＳＩ（Large Scale Integration）の内部あるいは外部に搭載されるＲＡＭ（Random Access Memory）の高機能化が進んでおり、その回路規模は大きくなり、論理構成も複雑化している。このため、高機能のＲＡＭの論理検証作業の困難さが増しており、論理検証を正確かつ効率的に実行できることが望まれている。このような要望に対して、例えば、ビヘイビア（Behavior）レベルでの論理検証時の信号遷移情報を、ＲＡＭマクロ全体のトランジスタレベル論理検証における入力ベクタおよび出力期待値として用いるようにした論理検証方法が提案されている（例えば、非特許文献１）。
【０００３】
ここで、一般的な回路の論理検証の方法としては、論理シミュレーション、コーン（cone）ベース論理一致検証、シンボリックシミュレーションの３種類を挙げることができる。
【０００４】
論理シミュレーションでは、実現する論理回路の正しいモデル（リファレンス）を、ゲートレベルより抽象度の高いＲＴＬ（Register Transfer Level）で記述する。一方、実際に設計する論理回路を、実装回路（インプリメンテーション）として、ゲートレベルあるいはトランジスタレベルのネットリストで設計する。そして、リファレンスとインプリメンテーションの両方に様々な入力信号を与え、両者の出力信号の一致を確認することで、インプリメンテーションの論理回路が正しいことを検証する。
【０００５】
この方法では、リファレンスとインプリメンテーションとで入出力端子が一致している必要がある他には制約がなく、適用範囲が広いという利点がある。その反面、論理検証を完全に行うためには、可能なすべての入力信号を与える必要がある。このため、入力数が多くなると組み合わせの数が膨大になってしまい、完全な検証が難しい。
【０００６】
また、コーンベース論理一致検証では、上記のリファレンスとインプリメンテーションとを、記憶素子や入出力ポートなどを境界とする論理グループである論理コーンに分解する。そして、各論理コーンについて、リファレンスとインプリメンテーションとの形式的論理一致検証が行われる。
【０００７】
この方法では、可能な入力信号のすべてに対して検証することと等価になるため、完全な検証が可能であり、その検証効率が高いという利点がある。その反面、論理合成できる論理記述モデルが必要となるため、適用範囲が組み合わせ回路に限られてしまう。このことから、この方法は、トランジスタレベルでの設計や、回路規模が大きいメモリ素子への適用には向かないと言える。
【０００８】
シンボリックシミュレーションは、これら２つの方法を融合させたものである。上記の論理シミュレーションでは、入力信号として“０”や“１”という具体的な論理値が入力されるが、シンボリックシミュレーションではその代わりに記号が論理値として入力される。１つの記号の論理値は“０”か“１”をとるため、ｎ入力（ｎは自然数）に対してｎ個の記号が入力される。従って、これらのｎ個の記号は２のｎ乗の個数の入力信号を表現している（例えば、非特許文献２，３参照）。
【０００９】
この方法では、シミュレーションがベースとなるために、コーンベース論理一致検証のように適用対象が限定されないという利点がある。その反面、対象設計に応じたテストベンチを作成する必要があり、論理シミュレーションのためのテストベンチと比較して難易度が高い。
【非特許文献１】檜垣直志，外２名、“低消費電力ＲＡＭ  ＩＰ化のための設計手法”、雑誌ＦＵＪＩＴＳＵ、富士通株式会社、２００２年１月、ｐ．４０−４６
【非特許文献２】Simon Napper，Dian Yang、“Equivalence Checking a 256MB SDRAM”、Memory Technology, Design and Testing、IEEE International Workshop on. 2002、２００１年８月、ｐ．８５−８９
【非特許文献３】Paul Hoxey，外２名、“An introduction to symbolic simulation”、［online］、２００５年１２月１９日、United Business Media LLC、［平成２０年８月１４日検索］、インターネット＜http://www.eetimes.com/showArticle.jhtml?articleID=175004754＞
【発明の開示】
【発明が解決しようとする課題】
【００１０】
前述のように、ＲＡＭの機能や構成が複雑化しているために、その論理検証作業をより効率的に行うことが望まれている。ここで、上記の３種類の論理検証方法のうち、高機能のＲＡＭの論理検証方法としては、一般的に論理シミュレーションまたはシンボリックシミュレーションが適していると言えるが、特に最近では、検証作業をより効率化できるシンボリックシミュレーションが注目されている。
【００１１】
しかし、シンボリックシミュレーションは非常に新しい技術であるため、入手可能なツールが高価であり、その種類も限られている。また、論理検証の実行のためには、リファレンスモデルや、検証対象範囲ごとにテストベンチを作成する必要があるが、このモデルやテストベンチの作成には、論理シミュレーションのためのものと比較して高いスキルが必要となる。さらに、検証対象はテストベンチによって指定された範囲となるので、検証漏れが完全になくなる訳ではない。
【００１２】
従って、シンボリックシミュレーションのように高いコストやスキルが要求される論理検証方法は、回路内のできるだけ少ない領域に適用することが望ましく、回路内の多くの領域には、より低コストで作業効率の高い論理検証方法を適用することが望ましいと言える。また、このような要求は、ＲＡＭに限らず、ＲＯＭ（Read Only Memory）などの他の半導体メモリや、規則性を有する大規模な論理構成を含む半導体回路に対しても、一般的に存在している。
【００１３】
本発明はこのような点に鑑みてなされたものであり、回路の論理検証の作業効率が向上した論理検証方法、装置およびプログラムを提供することを目的とする。
【課題を解決するための手段】
【００１４】
上記目的を達成するために、入力された選択信号をデコードして複数の信号線のうちの１本を選択するデコーダを含む回路群の論理検証を行う論理検証方法が提供される。この論理検証方法では、信号線認識部が、前記回路群を記述した設計情報を基に前記信号線を認識し、デコーダ認識部が、認識された前記各信号線を始点としてそれより入力側の論理素子を前記設計情報を基に順次認識し、論理値１を出力する論理積ゲートとして動作する論理素子とインバータとから構成される領域をデコーダ回路領域として認識するとともに、始点とした前記信号線の論理値を１としたときの当該デコーダ回路領域への入力信号の論理値を判別し、判定部が、前記デコーダ回路領域への入力信号の数と、前記各信号線を始点としてそれぞれ認識された前記デコーダ回路領域の間での入力信号の論理値の組み合わせとを基に、前記デコーダ回路領域の論理構成が正しいか否かを判定する。
【００１５】
このような論理検証方法では、まず、回路群の設計情報を基に、回路群内の信号線が認識され、さらに、デコーダ回路領域が認識される。デコーダ回路領域の認識処理では、認識された各信号線を始点としてそれより入力側の論理素子が順次認識されていき、論理値１を出力する論理積ゲートとして動作する論理素子とインバータとから構成される領域が、デコーダ回路領域として認識される。このとき、始点とした信号線の論理値を１としたときのデコーダ回路領域への入力信号の論理値も判別される。この後、認識されたデコーダ回路領域への入力信号の数と、各信号線を始点としてそれぞれ認識されたデコーダ回路領域の間での入力信号の論理値の組み合わせとを基に、認識されたデコーダ回路領域の論理構成が正しいか否かが判定されることで、デコーダの論理検証が行われる。
【００１６】
また、上記目的を達成するために、上記の論理検証方法と同様の処理を行う論理検証装置および論理検証プログラムが提供される。
【発明の効果】
【００１７】
上記の論理検証方法では、回路群の論理検証の作業効率が向上する。
【発明を実施するための最良の形態】
【００１８】
以下、実施の形態を図面を参照して詳細に説明する。
図１は、実施の形態に係る論理検証装置の概要を示す図である。
図１に示す論理検証装置１は、検証対象とされる回路群を記述した設計情報を基に、その回路群の論理検証を行うための装置である。ここで、検証対象とされる回路群には、選択信号の入力を受けてこれをデコードし、出力側の複数の信号線のうちの１本を選択するデコーダが含まれているものとする。そして、論理検証装置１は、設計情報を基に、回路群からデコーダの回路領域（以下、デコーダ回路領域と呼ぶ）を自動的に認識し、このデコーダ回路領域における論理検証を実行する。
【００１９】
論理検証装置１は、図１に示すように、信号線認識部１１、デコーダ認識部１２および判定部１３の各機能を備えている。なお、これらの機能またはその一部は、例えば、所定の論理検証プログラムをコンピュータのＣＰＵ（Central Processing Unit）によって実行することで、実現される。
【００２０】
信号線認識部１１は、設計情報を基に、回路群内のデコーダによって選択される信号線を認識する。例えば、上記のように単位回路がアレイ状に配列された構成の回路が存在する場合には、その単位回路を認識した後、単位回路同士の接続状態を基に、信号線を認識する。
【００２１】
デコーダ認識部１２は、認識された信号線の位置を基に、デコーダの回路構成上の特徴を利用して、デコーダ回路領域を認識する。この特徴とは、入力される選択信号が１つの値をとるとき、ただ１つの出力信号のみが“１”になるというものであり、そのような特徴を有するためには、デコーダは、全体として入力信号の値の論理積をとる回路である必要がある。デコーダ認識部１２は、このような特徴に基づき、まず、認識された各信号線を始点として、それより入力側の論理素子を設計情報を基に順次認識していく。そして、論理値１を出力する論理積ゲートとして動作する論理素子とインバータとから構成される領域を、デコーダ回路領域として認識する。
【００２２】
このとき、始点とした信号線の論理値を１としたときの、認識したデコーダ回路領域への入力信号の論理値も判別する。この論理値はすなわち、始点とした信号線を選択するためにデコーダに入力される信号の値と推定できる。また、論理素子を入力側にトレースしていった場合、途中に例えば論理積ゲートが認識された場合には、上記条件に合致していれば、その入力端子のそれぞれからさらに入力側に対して論理素子のトレースが行われる。このため、デコーダ回路領域への入力信号としては通常複数の入力信号が認識され、各入力信号がデコーダへの選択信号の各ビットに対応するようになる。従って、デコーダ回路領域への入力信号の論理値は、始点として信号線を選択するための選択信号の各ビットの値を推定していることになる。
【００２３】
判定部１３は、認識されたデコーダ回路領域を論理検証する。具体的には、デコーダ回路領域への入力信号の数と、各信号線を始点としてそれぞれ認識されたデコーダ回路領域の間での入力信号の論理値の組み合わせとを基に、デコーダ回路領域の論理構成が正しいか否かを判定する。
【００２４】
ここで、デコーダにおいては、選択可能な信号線の数によって、デコーダに入力される選択信号に必要なビット数が一意に決定される。例えば、２n本の信号線のうちの１本を選択するためのデコーダには、ｎビットの選択信号が入力されればよい。また、選択信号の論理値は、その選択信号によって選択する信号線ごとにすべて異なっている。
【００２５】
判定部１３は、このようなデコーダの特徴に基づき、デコーダ回路領域の論理構成が正しいか否かを判定する。すなわち、各信号線を始点としてそれぞれ認識されたデコーダ回路領域への入力信号の数が、信号線を選択するために必要な選択信号のビット数と一致し、なおかつ、各信号線を始点としてそれぞれ認識されたデコーダ回路領域の間で入力信号の論理値がすべて異なる場合に、認識したデコーダ回路領域の論理構成が正しいと判定する。
【００２６】
以上の論理検証装置１によれば、例えば論理シミュレーションやシンボリックシミュレーションのように、リファレンスモデルやテストベンチを作成することなく、デコーダの論理検証を自動的に実行できる。従って、デコーダの論理検証の作業効率を向上させ、結果として、回路群全体の論理検証の作業効率を向上させることができる。特に、デコーダその選択対象となる回路の規模が大きい場合には、論理検証の作業効率をより顕著に向上させることができる。
【００２７】
なお、上記の論理検証装置１ではデコーダを含む回路群が検証対象とされるが、このようなデコーダを含む回路群としては種々考えられる。その代表的な例としては、所定の単位回路がアレイ状に配列され、任意の単位回路を選択するために、単位回路に接続した選択信号線をデコーダによって選択するような回路を適用可能である。このような回路としては、単位回路としてメモリセルが配列されたＲＡＭやＲＯＭなどの半導体メモリが考えられる。あるいは、ＣＣＤ（Charge Coupled Device）などの撮像素子も考えられる。また、単位回路をアレイ状に配列した構成に限らず、例えば、１次元方向に並列された信号線のうちの１つをデコーダによって選択するような回路を、検証対象とすることも可能である。
【００２８】
次に、論理検証の対象とする回路群としてＲＡＭを適用した場合を例に挙げて、論理検証装置の機能およびその動作について具体的に説明する。
図２は、ＲＡＭ検証用の論理検証装置のハードウェア構成例を示すブロック図である。
【００２９】
本実施の形態の論理検証装置１００は、図２に示すようなコンピュータとして実現される。このコンピュータは、ＣＰＵ１０１、ＲＡＭ１０２、ＨＤＤ（Hard Disk Drive）１０３、グラフィック処理部１０４、入力Ｉ／Ｆ（インタフェース）１０５および通信Ｉ／Ｆ１０６を有し、これらはバス１０７を介して相互に接続されている。
【００３０】
ＣＰＵ１０１は、このコンピュータ全体に対する制御をつかさどる。ＲＡＭ１０２は、ＣＰＵ１０１に実行させるプログラムの少なくとも一部や、このプログラムによる処理に必要な各種データを一時的に記憶する。ＨＤＤ１０３には、ＯＳ（Operating System）やアプリケーションプログラム、各種データが格納される。このアプリケーションプログラムには、ＲＡＭの論理検証を行うための論理検証プログラムが含まれる。
【００３１】
グラフィック処理部１０４には、モニタ１０４ａが接続されている。このグラフィック処理部１０４は、ＣＰＵ１０１からの命令に従って、モニタ１０４ａの画面上に画像を表示させる。入力Ｉ／Ｆ１０５には、キーボード１０５ａやマウス１０５ｂが接続されている。この入力Ｉ／Ｆ１０５は、キーボード１０５ａやマウス１０５ｂからの信号を、バス１０７を介してＣＰＵ１０１に送信する。通信Ｉ／Ｆ１０６は、通信ケーブルを介してネットワークに接続し、ネットワーク上の他の機器との間でデータの送受信を行う。
【００３２】
図３は、ＲＡＭ検証用の論理検証装置の機能を示すブロック図である。
論理検証装置１００は、大別して、回路認識部１１０と、検証処理部１２０とを備えている。また、回路認識部１１０は、ビットセル認識部１１１、セルアレイ認識部１１２およびデコーダ認識部１１３を備えている。なお、これらの機能は、ＣＰＵ１０１で論理検証プログラムが実行されることによって実現される。
【００３３】
回路認識部１１０には、検証対象の回路（ＲＡＭ）の設計情報が入力される。本実施の形態では例として、回路設計情報が、トランジスタレベルで記述されたネットリスト１３１として入力される。回路認識部１１０の各機能は、例えばＨＤＤ１０３などに記憶されたネットリスト１３１を読み込み、このネットリスト１３１を基に以下のような回路の認識処理を行う。
【００３４】
ビットセル認識部１１１は、検証対象のＲＡＭに形成されたビットセルを認識し、各ビットセルに対応する回路情報群を、セルアレイ認識部１１２に通知する。
セルアレイ認識部１１２は、認識されたビットセル同士の接続状況を基に、それらがアレイ状に接続されていることを認識する。そして、ビットセルを選択するための選択信号線（ワード線、ビット線など）を認識する。さらに、例えば、複数のビット線が共通に接続されるマルチプレクサ（ＭＵＸ）が存在する場合には、このＭＵＸを認識し、複数のＭＵＸに接続されているビット選択信号線も認識する。
【００３５】
デコーダ認識部１１３は、認識された選択信号線（ワード線、ビット線、ビット選択信号線など）の情報を基に、アドレスデコーダを認識する。この処理では、認識された選択信号線を始点として回路設計情報をバックトレースし（すなわち、信号の入力側にトレースし）、回路上の論理素子を順に認識していくことで、アドレスデコーダの領域を認識する。そして、認識されたアドレスデコーダの領域において実現される論理式を示す論理式情報１３２を、検証処理部１２０に対して出力する。
【００３６】
検証処理部１２０は、回路認識部１１０によって得られた論理式情報１３２を基に、後述する判定基準に従って、アドレスデコーダの論理構成が正しいものであるか否かを検証し、検証結果情報１３３を出力する。検証結果情報１３３は、例えばＨＤＤ１０３に格納される。
【００３７】
なお、回路認識部１１０での処理によって、回路構成にエラーが発見された場合にも、検証結果情報１３３にそのエラーの内容が記述される場合もある。
次に、検証対象とする回路の具体的な構成例を挙げて、上記機能による処理をさらに詳しく説明する。
【００３８】
図４は、検証対象とするＲＡＭの回路構成例を概略的に示す図である。
図４に示すＲＡＭ２００には、ビットセル２１０がアレイ状に配列されている。水平方向に並列したビットセル２１０にはワード線２２１が共通に接続され、これらのワード線２２１は行アドレスデコーダ２２２に接続されている。行アドレスデコーダ２２２には、ワード線２２１を指定するためのアドレス信号Ｒ＿ＡＤＤＲが入力され、行アドレスデコーダ２２２は、アドレス信号Ｒ＿ＡＤＤＲをデコードして、指定された１本のワード線を選択する。なお、例えば、ビットセル２１０の垂直方向の並列数が２５６個である場合、アドレス信号Ｒ＿ＡＤＤＲは８ビットのデータとして入力される。
【００３９】
一方、垂直方向の並列したビットセル２１０にはビット線２３１が共通に接続されている。この例では、隣接する４本のビット線２３１が１つのＭＵＸ２３２に接続され、ビット線２３１を通じた入出力信号がＭＵＸ２３２により選択される構成となっている。そして、選択されたビット線２３１を通じて転送された信号は、各ＭＵＸ２３２からセンスアンプ２３３を通じて並列に出力される。
【００４０】
各ＭＵＸ２３２にはビット選択信号線２３４が共通に接続されており、ビット選択信号線２３４は列アドレスデコーダ２３５に接続されている。列アドレスデコーダ２３５にはビット線２３１を指定するためのアドレス信号Ｃ＿ＡＤＤＲが入力され、列アドレスデコーダ２３５は、アドレス信号Ｃ＿ＡＤＤＲをデコードして、各ＭＵＸ２３２に接続された中の１つのビット線２３１をビット選択信号線２３４を通じて選択する。なお、この例の場合、アドレス信号Ｃ＿ＡＤＤＲは２ビットのデータとして入力され、列アドレスデコーダ２３５は、アドレス信号Ｃ＿ＡＤＤＲをデコードして、４本のビット選択信号線２３４のうちのいずれかを選択することで、ＭＵＸ２３２に接続されたいずれかのビット線２３１を選択する。
【００４１】
ところで、上記構成のＲＡＭ２００において、ビットセル２１０を除く構成要素の中で回路規模が大きいのは、行アドレスデコーダ２２２および列アドレスデコーダ２３５である。このため、ＲＡＭ２００の論理検証の作業の中で、行アドレスデコーダ２２２および列アドレスデコーダ２３５の検証作業は大きな割合を占める。
【００４２】
そこで、論理検証装置１００では、行アドレスデコーダ２２２および列アドレスデコーダ２３５の論理検証作業を、これらの回路の構成上の特徴を基に簡易な手順で自動的に実現する。これにより、ＲＡＭ設計者によるＲＡＭ全体の論理検証作業の負担を大きく低減させる。
【００４３】
図５は、ビットセルの回路構成例を示す図である。
図５は、ＲＡＭ２００がＳＲＡＭ（Static RAM）である場合のビットセル２１０の回路構成の一例を示している。この回路は、インバータＩＮＶ１，ＩＮＶ２と、トランジスタＴＲ３，ＴＲ４とを備えている。インバータＩＮＶ１，ＩＮＶ２は互いにループ接続されており、データの保持機能を有している。インバータＩＮＶ１の入力端子は、トランジスタＴＲ３を介してビット線ｂｌに接続され、インバータＩＮＶ２の出力端子は、トランジスタＴＲ４を介してビット線ｂｌｂに接続されている。なお、この構成の場合、図４のＭＵＸには、ビット線ｂｌ，ｂｌｂの組み合わせがそれぞれ４組ずつ接続されて、アドレス信号Ｃ＿ＡＤＤＲによっていずれかの組み合わせが選択される。また、トランジスタＴＲ３，ＴＲ４の各ゲート端子には、ワード線ｗｌが接続されている。
【００４４】
このようなビットセルにデータが書き込まれる際には、ビット線ｂｌｂにはビット線ｂｌの反転信号が流れる。このとき、ワード線ｗｌが選択されてトランジスタＴＲ３，ＴＲ４がオンになることで、ビット線ｂｌ，ｂｌｂの値に応じたデータが入力され、その後にトランジスタＴＲ３，ＴＲ４がオフになっても、入力データが保持される。また、データの読み出しの際には、ワード線ｗｌが選択されてトランジスタＴＲ３，ＴＲ４がオンになることで、保持されたデータがビット線ｂｌ，ｂｌｂを通じて出力される。
【００４５】
図６は、図５の回路構成に対応する設計情報の例を示す図である。
図６は、ＲＡＭ２００をＳＰＩＣＥ形式のネットリストとして記述した例である。この記載のうち、領域３０１の記載が、図５の構成を有するビットセルを示している。
【００４６】
領域３０１において、第２行目から第６行目までの記載が、ビットセルを構成するトランジスタとその接続状態を示している。これらの各行には、先頭から順に、トランジスタ名、ドレイン端子に接続された信号線、ゲート端子に接続された信号線、ソース端子に接続された信号線が記述されている。
【００４７】
例えば、第２行目には、トランジスタ名としてｐチャネルＭＯＳ（Metal-Oxide-Semiconductor）トランジスタを示す“ｍｐ０”が記述され、このトランジスタのドレイン、ゲート、ソースの各端子には、図５中の信号線ｓ２，ｓ１、電源線ｖｄｄ（図示せず）が接続されていることが記述されている。また、第３行目には、トランジスタ名としてｎチャネルＭＯＳトランジスタを示す“ｍｎ０”が記述され、このトランジスタのドレイン、ゲート、ソースの各端子には、信号線ｓ２，ｓ１、電源線ｖｓｓが接続されていることが記述されている。従って、第２行目と第３行目によって、図５のインバータＩＮＶ１が表されている。
【００４８】
同様に、第３行目と第４行目の記載によって、図５のインバータＩＮＶ２が表されている。また、第５行目にはトランジスタＴＲ３が表され、第６行目にはトランジスタＴＲ４が表されている。
【００４９】
次に、回路認識部１１０の処理について説明する。
前述のように、ビットセル認識部１１１は、ＲＡＭ２００のネットリストを基にビットセルを認識する。ここで、図６のようなネットリストが入力された場合、このネットリストから図６中の領域３０１の第１行目に記載された宣言文などを判別することで、ビットセルの回路構成を記述した情報を抽出できる。または、このような宣言文を基にせずに、次の図７に示すような処理により、ネットリスト内からビットセルを記述した情報を抽出することもできる。あるいは、宣言文に基づいてビットセルを記述した情報を抽出した後、その抽出した情報が確かにビットセルを記述したものであるか否かを、図７の処理により確認してもよい。
【００５０】
図７は、ビットセル認識部の処理手順の例を示すフローチャートである。
ビットセル認識部１１１は、まず、ネットリストから、ループ接続されたインバータ（図５のインバータＩＮＶ１，ＩＮＶ２に対応）を抽出する（ステップＳ１１）。次に、抽出したループ回路の両側に接続された転送トランジスタ（図５のトランジスタＴＲ３，ＴＲ４に対応）を抽出する（ステップＳ１２）。次に、抽出した転送トランジスタのゲート端子に共通に接続された信号線（図５のワード線ｗｌに対応）を抽出する（ステップＳ１３）。
【００５１】
以上のステップＳ１１〜Ｓ１３の処理により、インバータのループ回路と２つの転送トランジスタとが抽出された場合、ビットセル認識部１１１は、それらの回路群をビットセルと認識して、その回路群を記述した回路情報群をセルアレイ認識部１１２に出力する（ステップＳ１４）。
【００５２】
なお、以上の処理は、図５に示した構成を有するビットセルを認識するための処理例であり、他の構成のビットセルを認識するためには、その構成に応じた認識アルゴリズムが適用されればよい。例えば、検証対象がＤＲＡＭ（Dynamic RAM）であれば、回路設計情報から、データを保持するコンデンサや、そこに接続された各種のトランジスタなどを抽出することで、ビットセルを認識できる。また、ＳＲＡＭを検証対象としたときに、図７の認識処理によってビットセルが認識されなかった場合には、異なる構成のビットセルを認識するための別の認識アルゴリズムを再度適用するようにしてもよい。
【００５３】
次に、図８は、セルアレイ認識部の処理手順の例を示すフローチャートである。
前述のように、セルアレイ認識部１１２は、認識されたビットセル同士の接続状況を基に、ビットセルを選択するための選択信号線を認識する。このために、セルアレイ認識部１１２は、まず、ビットセル認識部１１１によって認識されたビットセル同士を接続する接続線を抽出する（ステップＳ２１）。次に、抽出した接続線の中から、複数のビットセルに共通に接続された接続線を抽出する（ステップＳ２２）。
【００５４】
ステップＳ２２の処理により、共通の接続線が抽出された場合には、セルアレイ認識部１１２は、それらの接続線をワード線またはビット線と仮定したとき、ビットセルがアレイ状に配列されているか否かを判別する（ステップＳ２３）。ここで、セルアレイが正しく成立しない場合（例えば、各ワード線またはビット線に接続されるビットセルの数が異なる場合など）には、エラーを出力する。このエラーの情報は、例えば、検証結果情報１３３に記述される。
【００５５】
一方、セルアレイが正しく成立していた場合には、セルアレイ認識部１１２は、そのセルアレイに含まれるワード線およびビット線を抽出する（ステップＳ２４）。次に、複数のビット線が共通に接続されている回路があるか否かを判別し、その回路が複数存在した場合、さらにそれらの回路に共通の信号線（ビット選択信号線に対応）が接続していた場合には、ＭＵＸ（図４のＭＵＸ２３２に対応）と判別する。そして、ＭＵＸに接続されたビット選択信号線を抽出する（ステップＳ２５）。
【００５６】
次に、図９は、デコーダ認識部の処理について説明するための図である。
前述のように、デコーダ認識部１１３は、セルアレイ認識部１１２によって認識された選択信号線を始点として論理ゲートをバックトレースすることで、アドレスデコーダの領域を認識する。この処理では、１つの値の入力信号（アドレス信号）に対して、ただ１つの出力信号のみが“１”になるという、アドレスデコーダの回路構成上の特徴を利用して、アドレスデコーダの回路領域を認識していく。このような回路構成上の特徴から、アドレスデコーダは、基本的に、出力側の１つの選択信号線に対して入力信号の論理積をとる回路として表すことができる、と言うことができる。
【００５７】
図９は、例として、８本のワード線を選択するために３ビットのアドレス信号が入力される行アドレスデコーダの構成を、概念的に示したものである。図９において、出力信号ＷＬ０〜ＷＬ７は、０番目から７番目までのワード線にそれぞれ出力されるイネーブル信号である。また、入力信号Ａ０〜Ａ２は、入力されるアドレス信号の各ビットを下位から順に示したものであり、例えばアドレス信号の値が“１００”の場合、各ビットの値を下位からＡ０（０），Ａ１（０），Ａ２（１）と表している。
【００５８】
図９において、出力信号ＷＬ０を“１”とするためのアドレス信号が“０００”であるとすると、行アドレスデコーダにおいて０番目のワード線に接続している回路領域は、入力信号Ａ０〜Ａ２の反転信号の論理積をとるＡＮＤゲートＧ０として表すことができる。また、出力信号ＷＬ１を“１”とするためのアドレス信号が“００１”であるとすると、行アドレスデコーダにおいて１番目のワード線に接続している回路領域は、入力信号Ａ０と入力信号Ａ１，Ａ２の各反転信号との論理積をとるＡＮＤゲートＧ１として表すことができる。さらに、出力信号ＷＬ７を“１”とするためのアドレス信号が“１１１”であるとすると、行アドレスデコーダにおいて７番目のワード線に接続している回路領域は、入力信号Ａ０〜Ａ２の論理積をとるＡＮＤゲートＧ７として表すことができる。
【００５９】
なお、実際の行アドレスデコーダでは、入力信号Ａ０〜Ａ２の入力端子は共通化されている。また、ＡＮＤゲートＧ０〜Ｇ７に対応する回路領域の一部が重複していてもよい。
これらのＡＮＤゲートＧ０〜Ｇ７の各領域内では、その入力端から出力端に向かって、出力信号が“１”となるＡＮＤゲートが縦続に接続されていると見なすことができる。このため、逆にその出力端から入力端に向かって、出力信号が“１”となるようなＡＮＤゲート（または、このようなＡＮＤゲートと等価な動作を行う論理素子）を順次トレースしていくことで、上記のＡＮＤゲートＧ０〜Ｇ７として機能する回路領域を認識できる。デコーダ認識部１１３は、このようなバックトレースを行うことで、選択信号線ごとにアドレスデコーダの回路領域を認識していく。
【００６０】
次に、図１０は、デコーダ認識部の処理手順の例を示すフローチャートである。
デコーダ認識部１１３は、まず、セルアレイ認識部１１２によって認識された選択信号線（本実施の形態では、ワード線またはビット選択線）の１つを選択して、トレースの始点に設定する（ステップＳ３１）。また、認識処理に用いる変数ｆの値を“１”に初期化する（ステップＳ３２）。なお、この変数ｆの値は、始点に設定した選択信号線への出力値が“１”となる場合の、現在認識しているノードの信号値を示すものである。
【００６１】
次に、デコーダ認識部１１３は、ネットリスト１３１を基に、現在のノードの入力側に存在する論理素子の種類が、インバータであるか（ステップＳ３３）、ＡＮＤゲートであるか（ステップＳ３５）、ＯＲゲートであるか（ステップＳ３７）を判定する。
【００６２】
ステップＳ３３の判定処理で、論理素子がインバータであった場合、デコーダ認識部１１３は、変数ｆの値を反転させて（ステップＳ３４）、処理をステップＳ３９に進め、さらに上流側の論理素子の認識処理を続ける。
【００６３】
また、ステップＳ３５の判定処理で、論理素子がＡＮＤゲートであった場合、デコーダ認識部１１３は、現在の変数ｆの値が“１”であるか否かを判定する（ステップＳ３６）。ここで、変数ｆの値が“１”であった場合、すなわち、認識したＡＮＤゲートの出力信号が“１”となっている場合には、このＡＮＤゲートはアドレスデコーダの一部であると判断される。この場合、デコーダ認識部１１３は、処理をステップＳ３９に進めて、さらに上流側の論理素子の認識処理を続ける。
【００６４】
一方、ステップＳ３６の判定処理で、変数ｆの値が“０”であった場合には、認識したＡＮＤゲートはアドレスデコーダの外部のものであると判断される。この場合、デコーダ認識部１１３は、認識したＡＮＤゲートの出力ノードを、アドレスデコーダの入力側の境界として登録するとともに、この情報に対応付けて変数ｆの値を登録する（ステップＳ４０）。なお、これらの情報は、例えばＲＡＭ１０２などに一時的に記憶される。
【００６５】
また、ステップＳ３７の判定処理で、論理素子がＯＲゲートであった場合、デコーダ認識部１１３は、現在の変数ｆの値が“０”であるか否かを判定する（ステップＳ３８）。この判定処理では、認識したＯＲゲートがＡＮＤゲートに対して論理的に相補の動作を行う場合に、ＯＲゲートをＡＮＤゲートと等価と考えることができる。このため、変数ｆの値が“０”であった場合、すなわち、ＯＲゲートの出力信号が“０”となっている場合に、デコーダ認識部１１３は、このＯＲゲートがアドレスデコーダの一部であると判断して、処理をステップＳ３９に進め、さらに上流側の論理素子の認識処理を続ける。
【００６６】
一方、ステップＳ３８の判定処理で、変数ｆの値が“１”であった場合、デコーダ認識部１１３は、認識したＯＲゲートがアドレスデコーダの外部のものであると判断し、このＯＲゲートの出力ノードをアドレスデコーダの入力側の境界として登録するとともに、この情報に対応付けて変数ｆの値を登録する（ステップＳ４０）。
【００６７】
また、ステップＳ３３，Ｓ３５，Ｓ３７の判定処理で、入力ノードにインバータ、ＡＮＤゲート、ＯＲゲートのいずれの論理素子も認識できなかった場合、デコーダ認識部１１３は、その出力ノード（すなわち、直前に認識された論理素子の入力ノード）をアドレスデコーダの入力側の境界として登録するとともに、この情報に対応付けて変数ｆの値を登録する（ステップＳ４０）。
【００６８】
ただし、ステップＳ３１で選択信号線を始点として設定した直後に、ステップＳ３３，Ｓ３５，Ｓ３７の処理でインバータ、ＡＮＤゲート、ＯＲゲートのいずれの論理素子も認識できなかった場合には、デコーダ認識部１１３は、ステップＳ４０の処理の代わりに、アドレスデコーダを認識できなかったことを示す情報を、検証結果情報１３３に記述する。また、ステップＳ３１において選択信号線を始点として設定した直後に、ステップＳ３６において変数ｆの値が“０”と判定された場合、あるいは、ステップＳ３８において変数ｆの値が“１”と判定された場合にも、同様に、ステップＳ４０の処理の代わりに、アドレスデコーダを認識できなかったことを示す情報が、検証結果情報１３３に記述される。
【００６９】
ステップＳ３４で、変数ｆの値が判定された場合、および、ステップＳ３６，Ｓ３８で、認識したゲートがアドレスデコーダの一部であると判断された場合には、デコーダ認識部１１３は、認識処理対象のノードを、現在認識している論理素子の入力ノードに移動して、上記のステップＳ３３〜Ｓ３８の処理を再度実行する（ステップＳ３９）。
【００７０】
ここで、ＡＮＤゲートやＯＲゲートの入力ノードは複数存在する。このように入力ノードが複数存在した場合には、デコーダ認識部１１３は、それらの全ノードを認識処理対象として、上記のステップＳ３３〜Ｓ３８の処理をそれぞれの入力ノードに対して適用する。従って、１つの選択信号線を始点とした上記の認識処理により、アドレスデコーダが正しく認識される場合には、上記条件に合致したＡＮＤゲートやＯＲゲートが認識されるごとに、その入力側に認識される信号線が増加していき、最終的にステップＳ４０では、入力信号のビット数と同じ数の情報が登録されることになる。
【００７１】
ステップＳ４０の処理の終了後、デコーダ認識部１１３は、認識されたアドレスデコーダの回路領域における入出力の関係を示す論理式情報１３２を生成する（ステップＳ４１）。この処理では、アドレスデコーダの入力側の境界として登録された位置のそれぞれを、アドレス信号の各ビットに対応付け、各ビットの論理値を登録された変数ｆの値として、論理積の演算式が生成される。このような演算式は、認識処理で始点とされた選択信号線ごとに得られる。すなわち、選択信号線ごとに得られた演算式は、各選択信号線を選択するために入力されるアドレス信号の値を示していることになる。そして、後述するように、これらの演算式を検証することにより、アドレスデコーダが正しい構成を有しているか否かが検証される。
【００７２】
ここで、図１１は、アドレスデコーダの回路構成の一部を示す図である。
図１１では、例として、図９で述べた１番目のワード線を選択するための行アドレスデコーダ内の回路領域の構成を示している。なお、ここではアドレス信号の他に、制御信号Ｅ１，Ｅ２も入力される構成としている。これらの制御信号Ｅ１，Ｅ２は、すべてのワード線に対して共通の値をとるものであり、アドレス信号のさらに上位ビット側に付加される。そして、図１１の回路では、アドレス信号および制御信号を含めた入力信号の値が“０１００１”のとき、１番目のワード線が正しく選択される構成となっている。
【００７３】
図１１の回路において、ＮＡＮＤゲートＧ１１には、入力信号Ａ０と、入力信号Ａ１をインバータＩＮＶ１２によって反転した信号とが入力される。ＮＡＮＤゲートＧ１３には、入力信号Ａ２をインバータＩＮＶ１４によって反転した信号と、ＮＯＲゲートＧ１５からの出力信号とが入力される。ＮＯＲゲートＧ１５には、制御信号Ｅ１をインバータＩＮＶ１６によって判定した信号と、制御信号Ｅ２とが入力される。ＮＯＲゲートＧ１７には、ＮＡＮＤゲートＧ１１，Ｇ１３からの各出力信号が入力される。
【００７４】
ここで、図１１の回路に対して、図１０に示したデコーダ認識処理を適用した場合について説明する。まず、１番目のワード線を認識処理の始点としたとき（ステップＳ３１）、論理素子としてＮＯＲゲートＧ１１が認識されるが、ＮＯＲゲートは、ＯＲゲートの出力側にインバータを接続したものと等価である。そこで、デコーダ認識部１１３は、まず、インバータを認識して（ステップＳ３３）、変数ｆを“０”に反転し（ステップＳ３４）、次に、ＯＲゲートを認識する（ステップＳ３７）。このとき、変数ｆは“０”であるので（ステップＳ３８）、認識対象がＯＲゲートの入力ノード（すなわち、ＮＯＲゲートＧ１７の入力ノード）に移動される（ステップＳ３９）。
【００７５】
ここで、ＮＯＲゲートＧ１７の入力ノードのうち、例として下位ビット側（図中上側）のノードを認識対象とする。このとき、デコーダ認識部１１３は、論理素子としてＮＡＮＤゲートＧ１１を認識するが、ＮＡＮＤゲートは、ＡＮＤゲートの出力側にインバータを接続したものと等価である。そこで、デコーダ認識部１１３は、まず、インバータを認識して（ステップＳ３３）、変数ｆを“１”に反転し（ステップＳ３４）、次に、ＡＮＤゲートを認識する（ステップＳ３５）。このとき、変数ｆは“１”であるので（ステップＳ３６）、認識対象がＯＲゲートの入力ノード（すなわち、ＮＡＮＤゲートＧ１１の入力ノード）に移動される（ステップＳ３９）。
【００７６】
ここで、ＮＡＮＤゲートＧ１１の入力ノードのうち、例として下位ビット側（図中上側）のノードを認識対象とすると、このノードには論理素子が認識されない。従って、デコーダ認識部１１３は、ＮＡＮＤゲートＧ１１の下位ビット側の入力ノードを、アドレス信号の最下位ビット、すなわち入力信号Ａ０の入力端子と認識するとともに、その論理値として“１”を登録する（ステップＳ４０）。
【００７７】
このようにして、入力側からすべての論理ゲートが順次認識されていく。これにより、インバータＩＮＶ１２，ＩＮＶ１４，ＩＮＶ１６のそれぞれの入力ノードが、入力信号Ａ１，Ａ２、制御信号Ｅ１の入力端子と認識され、ＮＯＲゲートＧ１５の上位ビット側（図中下側）の入力ノードが、制御信号Ｅ２の入力端子と認識される。また、入力信号Ａ１，Ａ２、制御信号Ｅ１，Ｅ２にそれぞれ対応する論理値として、“０”、“０”、“１”、“０”が登録される。そして、デコーダ認識部１１３は、これらの登録情報を基に、出力信号ＷＬ１とこれに対応する入力信号との関係を示す論理式として、図１１中の下段に示す論理式を出力する（ステップＳ４１）。
【００７８】
なお、論理素子の認識にあたっては、例えば、入力信号Ｓ１，Ｓ２を仮定したとき、（Ｓ１＆Ｓ２）｜（Ｓ１＆Ｓ２）の論理式を示す構成を、この論理式と等価なＳ１＆Ｓ２に置き換えて、論理素子を認識していってもよい。このように論理式を適宜簡略化しながら論理素子を認識していくことで、処理負荷を軽減することができる。
【００７９】
次に、検証処理部１２０の処理について説明する。
次に、図１２は、検証処理部の処理手順の例を示すフローチャートである。
検証処理部１２０は、デコーダ認識部１１３から出力された論理式情報１３２を基に、認識されたアドレスデコーダの論理構成が正しいか否かを検証する。デコーダ認識部１１３は、まず、論理式情報１３２の中から、すべての選択信号線に対応する論理式を読み込む（ステップＳ５１）。なお、回路認識部１１０の処理により、複数の種類の選択信号線（本実施の形態では、ワード線とビット選択線）が認識されている場合には、以下の処理は、１つの種類の選択信号線ごとに実行される。
【００８０】
次に、デコーダ認識部１１３は、すべての選択信号線において偶奇が共通している入力信号が存在するか否かを判定し、存在した場合には、これらの入力信号を論理式から除外する（ステップＳ５２）。このような入力信号は、アドレス信号ではなく、例えば、アドレスデコーダ全体を選択するための制御信号などと考えられるので、このステップにおいて検証処理から除外する。
【００８１】
次に、デコーダ認識部１１３は、各選択信号線に対応する論理式がすべて異なっているか否かを判定する（ステップＳ５３）。アドレスデコーダでは、１つの入力信号に対してただ１つの選択信号線が選択されるため、アドレスデコーダが正しく構成されていれば、入出力の関係を表す論理式はすべて異なるものとなる。
【００８２】
ステップＳ５３の判定処理で、論理式がすべて異なっていた場合、検証処理部１２０はさらに、出力側の信号線の数に対して、入力信号の数が正しくなっているか否かを判定する（ステップＳ５４）。ここで、アドレスデコーダにより選択される選択信号線が２n本（ただし、ｎは自然数）であるとき、入力されるアドレス信号のビット数はｎビットとなり、入力信号の数はｎ個となる。例えば、図９のように、アドレスデコーダにより選択されるワード線が８本である場合には、３ビットのアドレス信号が入力される。ステップＳ５４では、論理式がこのような条件を満たしているか否かを判定している。
【００８３】
ステップＳ５４の判定処理で、入力信号の数が正しかった場合、検証処理部１２０は、アドレスデコーダの論理構成が正しかったことを記述した検証結果情報１３３を出力する（ステップＳ５５）。
【００８４】
一方、ステップＳ５３の判定処理で、論理式の一部が重複していた場合、および、ステップＳ５４の判定処理で、入力信号の数が正しくなかった場合には、検証処理部１２０は、アドレスデコーダの論理構成にエラーがあると判定して、エラーの内容を記述した検証結果情報１３３を出力する（ステップＳ５６）。
【００８５】
なお、以上のフローチャートにおいて、ステップＳ５３，Ｓ５４の判定処理の順序は逆であってもよい。
ここで、具体的な論理式情報１３２の例を挙げ、それらに基づくエラーの判定処理について説明する。
【００８６】
図１３は、論理式情報の第１の例を示す図である。
図１３において、矢印の左側の論理式は、８本のワード線のそれぞれを始点としたデコーダ認識処理により生成されたものを示す。また、矢印の右側の論理式は、左側の論理式を基に、図１２のステップＳ５２の処理を適用して、偶奇が共通している入力信号を除外したものである。なお、この点は、後の図１３〜図１７でも同様である。図１３の例では、左側の各論理式では、制御信号Ｅ１と、制御信号Ｅ２の反転値とが共通に含まれているため、右側の論理式ではこれらの制御信号Ｅ１，Ｅ２が除外され、アドレス信号に対応する入力信号のみが残されている。
【００８７】
右側の論理式に着目すると、これらの論理式はすべて異なっている。また、ワード線が８本であるので、アドレス信号のビット数は“３”となるが、右側の論理式には、入力信号Ａ０，Ａ１，Ａ２の３種類の入力信号が含まれている。従って、これらの論理式情報１３２からは、行アドレスデコーダの論理構成が正しいと判定される。
【００８８】
図１４は、論理式情報の第２の例を示す図である。
図１４の例では、左側の論理式を基に、偶奇が共通している入力信号を除外すると、図中右側に示すように、入力信号が２種類のみとなってしまう。このため、上記の論理検証によってエラーと判定される。なお、この例では、例えば、入力信号ＷＬ０，ＷＬ４にそれぞれ対応する論理式が重複しているため、このことからエラーと判定することもできる。
【００８９】
図１５は、論理式情報の第３の例を示す図である。
図１５の例では、入力信号ＷＬ０，ＷＬ１にそれぞれ対応する論理式が重複している。また、入力信号ＷＬ４，ＷＬ５にそれぞれ対応する論理式も重複している。従って、上記の論理検証によりエラーと判定される。
【００９０】
図１６は、論理式情報の第４の例を示す図である。
図１６では、回路構成に間違いがあるために、論理式の中に、アドレス信号や制御信号とは関係のない別の入力信号Ｃが出現した場合の例を示している。このとき、図中右側の論理式には、入力信号Ａ０，Ａ１，Ａ２と入力信号Ｃの４種類の信号が含まれていることから、上記の論理検証によりエラーと判定される。
【００９１】
図１７は、論理式情報の第５の例を示す図である。
図１７では、認識したアドレスデコーダの領域において、論理ゲートの種類に間違いがあった場合の例を示している。例えば、入力信号Ａ１と、入力信号Ａ０の反転信号とを受け付けて、信号ｔ１を出力するＡＮＤゲートを、ＯＲゲートと間違った場合などに、図１７のような論理式が出現し得る。この例の場合には、右側の論理式において、入力信号Ａ０と、信号ｔ０，ｔ１，ｔ２，ｔ３の５種類の信号が含まれていることから、上記の論理検証によりエラーと判定される。
【００９２】
図１８は、検証結果情報に記述されるエラー情報の例を示す図である。
図１８では、上記の論理検証の結果、エラーと判定された場合に、検証結果情報１３３に記載されるエラー情報の例として、６種類の文字情報の記載例を示している。第１行目（エラー番号“０１２４”）は、セルアレイにおける列の数または各列での回路の接続が間違っていたことを示している。また、第２行目（エラー番号“０１２５”）は、セルアレイにおける行の数または各行での回路の接続が間違っていたことを示している。また、第３行目（エラー番号“０１２６”）は、選択信号線の接続に間違いがあったことを示している。これらの第１行目〜第３行目の情報は、例えば、セルアレイ認識部１１２による認識処理の過程において判定されて出力される。
【００９３】
第４行目（エラー番号“０１２７”）は、アドレスデコーダが認識されなかったことを示している。この情報は、例えば、デコーダ認識部１１３の処理において、認識の始点とした選択信号線の入力側に、条件を満たす論理素子が存在しなかった場合などに出力される。
【００９４】
第５行目および第６行目の情報は、検証処理部１２０による検証結果として出力されるものである。第５行目（エラー番号“０１２０”）は、認識されたデコーダの入力信号の数が正しくなかったことを示している。また、第６行目（エラー番号“０１２２”）は、各選択信号線に対応する論理式の中に重複するものがあったことを示している。
【００９５】
なお、以上の実施の形態では、ビット線がＭＵＸに接続された構成のＲＡＭにおける論理検証について説明したが、例えばＭＵＸが設けられておらず、各ビット線が列アドレスデコーダに直接接続された構成の場合には、各ビット線を始点として図１０のデコーダ認識処理を行った後、図１２の検証処理を行えばよい。
【００９６】
以上説明した論理検証装置１では、ＲＡＭの回路設計情報を基に、アドレスデコーダの回路領域を認識し、その回路領域内の論理構成を検証する処理を、アドレスデコーダの構成上の特徴を用いた簡単な処理によって実行できる。また、この処理では、論理シミュレーションやシンボリックシミュレーションのように、リファレンスモデルやテストベンチを作成する必要がないので、設計者に特に高いスキルが要求されない。従って、ＲＡＭの論理検証の工程のうちの大部分の工程を、処理負荷が軽く、しかも設計者の操作が必要でない自動的な処理によって、実行できるようになる。
【００９７】
また、アドレスデコーダ以外の回路領域には、論理シミュレーションやシンボリックシミュレーションなどの他の論理検証法を用いればよい。この場合でも、全体としてＲＡＭの論理検証作業を短時間で実行できるようになり、その作業コストを軽減することができる。
【００９８】
なお、上記の論理検証装置が有する機能の少なくとも一部は、コンピュータによって実現することができる。その場合には、上記機能の処理内容を記述したプログラムが提供される。そして、そのプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。
【００９９】
プログラムを流通させる場合には、例えば、そのプログラムが記録された光ディスクなどの可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、そのプログラムを、サーバコンピュータからネットワークを介して他のコンピュータに転送することもできる。
【０１００】
プログラムを実行するコンピュータは、例えば、可搬型記録媒体に記録されたプログラムまたはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、そのプログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムに従った処理を実行することもできる。
【図面の簡単な説明】
【０１０１】
【図１】実施の形態に係る論理検証装置の概要を示す図である。
【図２】ＲＡＭ検証用の論理検証装置のハードウェア構成例を示すブロック図である。
【図３】ＲＡＭ検証用の論理検証装置の機能を示すブロック図である。
【図４】検証対象とするＲＡＭの回路構成例を概略的に示す図である。
【図５】ビットセルの回路構成例を示す図である。
【図６】図５の回路構成に対応する設計情報の例を示す図である。
【図７】ビットセル認識部の処理手順の例を示すフローチャートである。
【図８】セルアレイ認識部の処理手順の例を示すフローチャートである。
【図９】デコーダ認識部の処理について説明するための図である。
【図１０】デコーダ認識部の処理手順の例を示すフローチャートである。
【図１１】アドレスデコーダの回路構成の一部を示す図である。
【図１２】検証処理部の処理手順の例を示すフローチャートである。
【図１３】論理式情報の第１の例を示す図である。
【図１４】論理式情報の第２の例を示す図である。
【図１５】論理式情報の第３の例を示す図である。
【図１６】論理式情報の第４の例を示す図である。
【図１７】論理式情報の第５の例を示す図である。
【図１８】検証結果情報に記述されるエラー情報の例を示す図である。
【符号の説明】
【０１０２】
１  論理検証装置
１１  信号線認識部
１２  デコーダ認識部
１３  判定部
【図１】
2010055212.tif 000003
【図２】
2010055212.tif 000004
【図３】
2010055212.tif 000005
【図４】
2010055212.tif 000006
【図５】
2010055212.tif 000007
【図６】
2010055212.tif 000008
【図７】
2010055212.tif 000009
【図８】
2010055212.tif 000010
【図９】
2010055212.tif 000011
【図１０】
2010055212.tif 000012
【図１１】
2010055212.tif 000013
【図１２】
2010055212.tif 000014
【図１３】
2010055212.tif 000015
【図１４】
2010055212.tif 000016
【図１５】
2010055212.tif 000017
【図１６】
2010055212.tif 000018
【図１７】
2010055212.tif 000019
【図１８】
2010055212.tif 000020
【手続補正書】
【提出日】平成20年9月3日(2008.9.3)
【手続補正１】
【補正対象書類名】明細書
【補正対象項目名】００３５
【補正方法】変更
【補正の内容】
【００３５】
デコーダ認識部１１３は、認識されたワード線、ビット線、ビット選択信号線などの選択信号線の情報を基に、アドレスデコーダを認識する。この処理では、認識された選択信号線を始点として回路設計情報をバックトレース、すなわち、信号の入力側にトレースし、回路上の論理素子を順に認識していくことで、アドレスデコーダの領域を認識する。そして、認識されたアドレスデコーダの領域において実現される論理式を示す論理式情報１３２を、検証処理部１２０に対して出力する。
【手続補正２】
【補正対象書類名】明細書
【補正対象項目名】００５０
【補正方法】変更
【補正の内容】
【００５０】
図７は、ビットセル認識部の処理手順の例を示すフローチャートである。
ビットセル認識部１１１は、まず、ネットリストから、ループ接続されたインバータを抽出する（ステップＳ１１）。図５の例では、インバータＩＮＶ１，ＩＮＶ２が抽出される。次に、抽出したループ回路の両側に接続された転送トランジスタを抽出する（ステップＳ１２）。図５の例では、トランジスタＴＲ３，ＴＲ４が抽出される。次に、抽出した転送トランジスタのゲート端子に共通に接続された信号線を抽出する（ステップＳ１３）。図５の例では、ワード線ｗｌが抽出される。
【手続補正３】
【補正対象書類名】明細書
【補正対象項目名】００６０
【補正方法】変更
【補正の内容】
【００６０】
次に、図１０は、デコーダ認識部の処理手順の例を示すフローチャートである。
デコーダ認識部１１３は、まず、セルアレイ認識部１１２によって認識された選択信号線の１つを選択して、トレースの始点に設定する（ステップＳ３１）。本実施の形態では、ワード線またはビット選択線が選択される。次に、認識処理に用いる変数ｆの値を“１”に初期化する（ステップＳ３２）。なお、この変数ｆの値は、始点に設定した選択信号線への出力値が“１”となる場合の、現在認識しているノードの信号値を示すものである。
【手続補正４】
【補正対象書類名】明細書
【補正対象項目名】００７９
【補正方法】変更
【補正の内容】
【００７９】
次に、検証処理部１２０の処理について説明する。
次に、図１２は、検証処理部の処理手順の例を示すフローチャートである。
検証処理部１２０は、デコーダ認識部１１３から出力された論理式情報１３２を基に、認識されたアドレスデコーダの論理構成が正しいか否かを検証する。デコーダ認識部１１３は、まず、論理式情報１３２の中から、すべての選択信号線に対応する論理式を読み込む（ステップＳ５１）。なお、回路認識部１１０の処理により、複数の種類の選択信号線が認識されている場合には、以下の処理は、１つの種類の選択信号線ごとに実行される。なお、本実施の形態では、ワード線およびビット選択線の２種類の選択信号線が、回路認識部１１０によって認識されている。