(57)【要約】【課題】不定値の伝播に関する、ＲＴＬ記述とネットリストとの論理シミュレーション結果の不一致を取り除くことができる論理シミュレーション方法を提供する。【解決手段】この論理シミュレーション方法は、従来と比べて、不定値に関する〜ｘ＝ｘの関係式を無くし、その代わりに、不定値の反転信号をＡＮＤ回路およびＯＲ回路の演算を規定する代数式に組み込むことにより、不定値、その不定値の反転信号、真理値“０”、真理値“１”の４個の数値間のブール代数関係を正確に取り扱うことを実現し、不定値伝播に関する、ＲＴＬ記述とネットリストとの論理シミュレーション結果の不一致を取り除く様にしたものである。【選択図】なし【特許請求の範囲】
【請求項１】
不定値を出力するフリップフロップ回路を１つ含む論理回路を論理シミュレーションする論理シミュレーション方法であって、
前記不定値を“ｘ”とし、前記不定値の否定を“〜ｘ”として、
前記論理回路に含まれるＡＮＤ回路において、
不定値“〜ｘ”と不定値“〜ｘ”とが入力したときの出力を不定値“〜ｘ”とし、
また不定値“〜ｘ”と不定値“ｘ”とが入力したときの出力を真理値“０”とし、
また不定値“〜ｘ”と真理値“１”とが入力したときの出力を不定値“〜ｘ”とし、
また不定値“〜ｘ”と真理値“０”とが入力したときの出力を真理値“０”とし、
また不定値“ｘ”と不定値“ｘ”とが入力したときの出力を不定値“ｘ”とし、
また不定値“ｘ”と真理値“０”とが入力したときの出力を真理値“０”とし、
また不定値“ｘ”と真理値“１”とが入力したときの出力を不定値“ｘ”とし、
前記論理回路に含まれるＯＲ回路において、
不定値“〜ｘ”と不定値“〜ｘ”とが入力したときの出力を不定値“〜ｘ”とし、
また不定値“〜ｘ”と不定値“ｘ”とが入力したときの出力を真理値“１”とし、
また不定値“〜ｘ”と真理値“１”とが入力したときの出力を真理値“１”とし、
また不定値“〜ｘ”と真理値“０”とが入力したときの出力を不定値“〜ｘ”とし、
また不定値“ｘ”と不定値“ｘ”とが入力したときの出力を不定値“ｘ”とし、
また不定値“ｘ”と真理値“０”とが入力したときの出力を不定値“ｘ”とし、
また不定値“ｘ”と真理値“１”とが入力したときの出力を真理値“１”とすることを特徴とする論理シミュレーション方法。
【請求項２】
不定値を出力するフリップフロップ回路を複数含む論理回路を論理シミュレーションする論理シミュレーション方法であって、
異なるフリップフロップ回路から出力される不定値を“ｘ[i]”，“ｘ[j]”（但しi≠j）とし、それらの否定を“〜ｘ[i]”，“〜ｘ[j]”として、 
前記論理回路に含まれるＡＮＤ回路において、
不定値“〜ｘ[i]”と不定値“〜ｘ[i]”とが入力したときの出力を不定値“〜ｘ[i]”とし、
また不定値“〜ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を真理値“０”とし、
また不定値“〜ｘ[i]”と真理値“１”とが入力したときの出力を不定値“〜ｘ[i]”とし、
また不定値“〜ｘ[i]”と真理値“０”とが入力したときの出力を真理値“０”とし、
また不定値“ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を不定値“ｘ[i]”とし、
また不定値“ｘ[i]”と真理値“０”とが入力したときの出力を真理値“０”とし、
また不定値“ｘ[i]”と真理値“１”とが入力したときの出力を不定値“ｘ[i]”とし、
また不定値“ｘ[i]”と不定値“ｘ[j]”とが入力したときの出力を不定値“ｘ”（“ｘ”は、〜ｘ＝ｘの関係を満たす不定値とする（以下同様））とし、
また不定値“〜ｘ[i]”と不定値“ｘ[j]”とが入力したときの出力を不定値“ｘ”とし、  
また不定値“〜ｘ[i]”と不定値“〜ｘ[j]”とが入力したときの出力を不定値“ｘ”とし、  
前記論理回路に含まれるＯＲ回路において、
不定値“〜ｘ[i]”と不定値“〜ｘ[i]”とが入力したときの出力を不定値“〜ｘ[i]”とし、
また不定値“〜ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を真理値“１”とし、
また不定値“〜ｘ[i]”と真理値“１”とが入力したときの出力を真理値“１”とし、
また不定値“〜ｘ[i]”と真理値“０”とが入力したときの出力を不定値“〜ｘ[i]”とし、
また不定値“ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を不定値“ｘ[i]”とし、
また不定値“ｘ[i]”と真理値“０”とが入力したときの出力を不定値“ｘ[i]”とし、
また不定値“ｘ[i]”と真理値“１”とが入力したときの出力を真理値“１”とし、
また不定値“ｘ[i]”と不定値“ｘ[j]”とが入力したときの出力を不定値“ｘ”とし、  また不定値“〜ｘ[i]”と不定値“ｘ[j]”とが入力したときの出力を不定値“ｘ”とし、
また不定値“〜ｘ[i]”と不定値“〜ｘ[j]”とが入力したときの出力を不定値“ｘ”とすることを特徴とする論理シミュレーション方法。
【請求項３】
ＲＴＬ（Register Transfer Level）記述に対して論理シミュレーションを行って論理シミュレーション結果を得る工程と、
前記ＲＴＬ記述を論理合成してネットリストを作成する工程と、
前記ネットリストに対して、請求項１または請求項２に記載の論理シミュレーション方法を用いた論理シミュレーションを行って論理シミュレーション結果を得る工程と、
前記ＲＴＬ記述の前記論理シミュレーション結果と前記ネットリストの前記論理シミュレーション結果とが一致しているか否かを判定する工程と、
を備えることを特徴とする半導体回路の設計検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、不定値を出力するフリップフロップ回路を含む論理回路を論理シミュレーションする技術に関する。
【背景技術】
【０００２】
Verilog や ModelSim など従来の論理シミュレータにおいては、不定値の伝播についてＲＴＬ（Register Transfer Level）記述の論理シミュレーションとそのＲＴＬ記述から論理合成された等価なネットリストの論理シミュレーションとの間で論理シミュレーション結果が異なる場合がある。
【０００３】
以下では一例として、図１のＲＴＬ記述とそのＲＴＬ記述から論理合成されたネットリストの各動作（従来の論理シミュレータを用いたときの動作）について考察する。図２は、図１のＲＴＬ記述を視覚的に分かり易いように回路図にしたものである。また図３は、図１のＲＴＬ記述を論理合成して得られたネットリストの回路図を示したものである。
【０００４】
また下記の式５〜式１０および式１５〜式２０は、従来の論理シミュレータで使用される代数式（ＡＮＤ回路およびＯＲ回路の演算を規定する代数式）を示したものである。各式中の＝は等号、∧は論理積、＋は論理和、〜は値の反転を示す記号であり、ｘは、〜ｘ＝ｘの関係を満たす不定値であり、０，１は〜１＝０、〜０＝１を満たす真理値である。尚、各式の左辺は全て可換とする。
【０００５】
ｘ∧ｘ＝ｘ    ・・・式５
ｘ∧０＝０    ・・・式６
ｘ∧１＝ｘ    ・・・式７
１∧１＝１    ・・・式８
１∧０＝０    ・・・式９
０∧０＝０    ・・・式１０
ｘ＋ｘ＝ｘ    ・・・式１５
ｘ＋０＝ｘ    ・・・式１６
ｘ＋１＝１    ・・・式１７
１＋１＝１    ・・・式１８
１＋０＝１    ・・・式１９
０＋０＝０    ・・・式２０。
【０００６】
まず最初に、図１のＲＴＬ記述の動作について考察する。図２と図１は先に述べたように同一の回路をあらわすので、以下では、図２を用いてＲＴＬの動作を説明する。
【０００７】
時刻０の初期状態の時および時刻１の時、信号ａ、信号ｂはそれぞれ値“０”であるとする。また、フリップフロップ回路Ｓ２には例えば時刻１でクロックが入力されるものとする。時刻０のとき、図２のセレクタＳ１においては、図１のセレクタ記述からわかるように選択信号ｂは値“０”となるので、セレクタＳ１の入力信号ａが選択され、セレクタＳ１の出力信号Ｙは信号ａの値と同一となり、その値は“０”である。この時、フリップフロップ回路Ｓ２の入力信号の値は“０”となり、時刻１からのクロックの立ち上がりエッジに同期してフリップフロップ回路Ｓ２の出力からは“０”が出力され、信号ｄの値は“０”となる。そして、信号ｂ＝０及び信号ｄ＝０より、信号ｃの値は“０”となる。
【０００８】
この動作を数式で書くと以下のようになる。即ち時刻０で、セレクタ選択信号ｂの値は“０”（即ち信号ａを選択）なので、信号Ｙの値は、Ｙ＝ａ＝０より“０”となる。また時刻１でクロックが入力されて、Ｓ２の入力ＤであるＹが“０”なので、Ｓ２の出力Ｑである信号ｄの値は“０”となる。
【０００９】
また時刻１では、信号ｃの値は、下記の計算により“０”になる。
【００１０】
ｃ＝ｄ∧（〜ｂ）
＝０∧（〜０）  （∵時刻１でｂ＝０）
＝０∧１        （∵〜０＝１）
＝０            （∵式９）。
【００１１】
次に時刻０での図３のネットリストの動作について説明する。まず、ＡＮＤ回路Ｒ１に注目すると、入力信号ｂの値は“０”であるが、入力信号ｄの値は不定値“ｘ”である。なぜなら、時刻０ではまだフリップフロップ回路Ｒ６にクロックが入力されておらず、その出力は不定だからである。よって、このＡＮＤ回路Ｒ１から出力される信号ｃは、不定値“ｘ”となる。
【００１２】
次に時刻０でのＡＮＤ回路Ｒ３に注目する。このＡＮＤ回路Ｒ３の入力信号はｄとｃであるが、信号ｄも信号ｃも先に述べたように不定値なので、ＡＮＤ回路Ｒ３の出力信号ｅは不定値となる。次にＯＲ回路Ｒ５に注目する。このＯＲ回路Ｒ５の入力信号はｅとａであるが、信号ｅが不定値でかつ信号ａが“０”であるので、ＯＲ回路Ｒ５の出力信号ｆは不定値となる。
【００１３】
次に時刻１でクロックが入力された時のフリップフロップ回路Ｒ６について注目する。先に述べたようにこの時、フリップフロップ回路Ｒ６の入力信号ｆは不定値となるので、クロックに同期してフリップフロップ回路Ｒ６の出力信号ｄは不定値となる。
【００１４】
この動作を数式で書くと以下のようになる。
【００１５】
時刻０で、信号ｃは、下記の計算により不定値“ｘ”になる。
【００１６】
ｃ＝ｄ∧（〜ｂ）
＝ｘ∧（〜０）（∵時刻０でｂ＝０）
＝ｘ∧１      （∵〜０＝１）
＝ｘ          （∵式７）。
【００１７】
また信号ｅは、下記の計算により不定値“ｘ”になる。
【００１８】
ｅ＝ｄ＋（〜ｃ）
＝ｘ＋（〜ｘ）（∵上記の計算結果ｃ＝ｘ）
＝ｘ＋ｘ      （∵〜ｘ＝ｘ）
＝ｘ          （∵式１５）。
【００１９】
また信号ｆは、下記の計算により不定値“ｘ”になる。
【００２０】
ｆ＝ｅ＋ａ  
＝ｘ＋０  （∵時刻０でａ＝０）
＝ｘ      （∵式１６）。
【００２１】
従って時刻１で、Ｒ６の入力であるｆが“ｘ”なので、Ｒ６の出力Ｑである信号ｄの値は“ｘ”となる。
【００２２】
以上のように、時刻１でのＲＴＬ記述の論理シミュレーション結果とネットリストの論理シミュレーション結果には以下のような違いがある。即ち、ＲＴＬ記述の論理シミュレーション結果では、時刻１の時、信号ｄ及び信号ｃの値はどちらも“０”となる。一方、ネットリストの論理シミュレーション結果では、時刻１の時、信号ｄ及び信号ｃの値はどちらも不定値“ｘ”となる。即ち、ネットリストは適切に（即ちＲＴＬ記述と等価となる様に）論理合成されているにも拘わらず、ＲＴＬ記述とネットリストとの論理シミュレーション結果が一致しない場合がある。
【発明の開示】
【発明が解決しようとする課題】
【００２３】
通常、ＲＴＬ設計時には、そのＲＴＬ記述の論理が正しいことを検証するためのテストベンチを作成し、そのＲＴＬ記述に対してテストベンチを適用して論理シミュレーションを実行する。そして、その論理シミュレーションが正常に実行されれば、ＲＴＬ記述が正しく設計されたことが保証される。
【００２４】
次に、そのＲＴＬ記述を論理合成してネットリストを得るが、その論理合成が正しく実行されたかどうかは（即ち論理合成によって得られたネットリストがＲＴＬ記述と等価であるかどうかは）、先のテストベンチを用いてそのネットリストの論理シミュレーションを実行することにより判定することができる。すなわち、そのテストベンチをネットリストに適用して論理シミュレーションを実行した結果が、そのテストベンチを元のＲＴＬ記述に適用した結果と同じになれば、論理合成によって得られたネットリストは、ＲＴＬ記述と等価なものであると判定できるわけである。
【００２５】
しかしながら、上記で述べたように、従来の論理シミュレータでは、不定値の取り扱いが適切でないために、不定値の伝播に関してＲＴＬ記述とネットリストとの論理シミュレーション結果が異なる場合がある。もし、このような現象が発生した場合、設計者は可読性の悪い複雑なネットリストを解析してその原因を見つけ出す必要があり、設計時間の増大を招く。また、上記で述べたような原因を見つけ出した場合、ＲＴＬ記述とネットリストとの論理シミュレーション結果を一致させるためにＲＴＬ記述を書き直したり、あるいはネットリストにＥＣＯ（Engineering Change Order）と呼ばれる論理変更を実施する必要あり、これも設計時間の増大を招いていた。
【００２６】
そこで、この発明の課題は、不定値の伝播に関する、ＲＴＬ記述とネットリストとの論理シミュレーション結果の不一致を取り除くことができる論理シミュレーション方法および半導体回路の設計検証方法を提供することにある。
【課題を解決するための手段】
【００２７】
上記課題を解決する為に、本発明の一実施形態は、不定値を出力するフリップフロップ回路を１つ含む論理回路を論理シミュレーションする論理シミュレーション方法であって、前記不定値を“ｘ”とし、前記不定値の否定を“〜ｘ”として、前記論理回路に含まれるＡＮＤ回路において、不定値“〜ｘ”と不定値“〜ｘ”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“〜ｘ”と不定値“ｘ”とが入力したときの出力を真理値“０”とし、また不定値“〜ｘ”と真理値“１”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“〜ｘ”と真理値“０”とが入力したときの出力を真理値“０”とし、また不定値“ｘ”と不定値“ｘ”とが入力したときの出力を不定値“ｘ”とし、また不定値“ｘ”と真理値“０”とが入力したときの出力を真理値“０”とし、また不定値“ｘ”と真理値“１”とが入力したときの出力を不定値“ｘ”とし、前記論理回路に含まれるＯＲ回路において、不定値“〜ｘ”と不定値“〜ｘ”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“〜ｘ”と不定値“ｘ”とが入力したときの出力を真理値“１”とし、また不定値“〜ｘ”と真理値“１”とが入力したときの出力を真理値“１”とし、また不定値“〜ｘ”と真理値“０”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“ｘ”と不定値“ｘ”とが入力したときの出力を不定値“ｘ”とし、また不定値“ｘ”と真理値“０”とが入力したときの出力を不定値“ｘ”とし、また不定値“ｘ”と真理値“１”とが入力したときの出力を真理値“１”とするものである。
【発明の効果】
【００２８】
本発明の一実施形態によれば、論理回路が不定値を出力するフリップフロップ回路を１つ含む場合に、ＡＮＤ回路およびＯＲ回路での演算で前記不定値が適切に扱われるので、不定値の伝播に関する、ＲＴＬ記述とネットリストとの論理シミュレーション結果の不一致を取り除く事ができる。
【発明を実施するための最良の形態】
【００２９】
実施の形態１．
この実施の形態に係る半導体回路の設計検証方法は、ＲＴＬ（Register Transfer Level）記述を論理合成して得られるネットリストを、本発明の論理シミュレーション方法を用いて、ＲＴＬ記述と等価なものになっているかを検証するものである。
【００３０】
まず本発明に係る論理シミュレーション方法について説明する。この論理シミュレーション方法は、不定値（その不定値を“ｘ”、その否定を“〜ｘ”で表記する）を出力するフリップフロップ回路を１つ含む論理回路を論理シミュレーションするものである。
【００３１】
この論理シミュレーション方法では、前記論理回路に含まれるＡＮＤ回路において、不定値“〜ｘ”と不定値“〜ｘ”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“〜ｘ”と不定値“ｘ”とが入力したときの出力を真理値“０”とし、また不定値“〜ｘ”と真理値“１”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“〜ｘ”と真理値“０”とが入力したときの出力を真理値“０”とし、また不定値“ｘ”と不定値“ｘ”とが入力したときの出力を不定値“ｘ”とし、また不定値“ｘ”と真理値“０”とが入力したときの出力を真理値“０”とし、また不定値“ｘ”と真理値“１”とが入力したときの出力を不定値“ｘ”とする様に設定されている。
【００３２】
またＡＮＤ回路において、従来通り、真理値“１”と真理値“１”とが入力したときの出力は真理値“１”となり、真理値“１”と真理値“０”とが入力したときの出力は真理値“０”となり、真理値“０”と真理値“０”とが入力したときの出力は真理値“０”となる様に設定されている。
【００３３】
上記のＡＮＤ回路の演算の設定を代数式で表すと、下記の式１〜式１０の様になる。
【００３４】
（〜ｘ）∧（〜ｘ）＝〜ｘ    ・・・式１
（〜ｘ）∧ｘ＝０            ・・・式２
（〜ｘ）∧１＝〜ｘ          ・・・式３
（〜ｘ）∧０＝０            ・・・式４
ｘ∧ｘ＝ｘ                ・・・式５
ｘ∧０＝０                ・・・式６
ｘ∧１＝ｘ                ・・・式７
１∧１＝１                ・・・式８
１∧０＝０                ・・・式９
０∧０＝０                ・・・式１０。
【００３５】
尚、上記の式において、＝は等号、∧は論理積、＋は論理和、〜は値の反転を表す記号である（以下同様）。また上記の式の右辺は全て可換とする。また０，１は〜１＝０、〜０＝１の関係を満たす真理値とする（以下同様）。
【００３６】
また前記論理回路に含まれるＯＲ回路において、不定値“〜ｘ”と不定値“〜ｘ”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“〜ｘ”と不定値“ｘ”とが入力したときの出力を真理値“１”とし、また不定値“〜ｘ”と真理値“１”とが入力したときの出力を真理値“１”とし、また不定値“〜ｘ”と真理値“０”とが入力したときの出力を不定値“〜ｘ”とし、また不定値“ｘ”と不定値“ｘ”とが入力したときの出力を不定値“ｘ”とし、また不定値“ｘ”と真理値“０”とが入力したときの出力を不定値“ｘ”とし、また不定値“ｘ”と真理値“１”とが入力したときの出力を真理値“１”とする様に設定されている。
【００３７】
またＯＲ回路において、従来通り、真理値“１”と真理値“１”とが入力したときの出力は真理値“１”となり、真理値“１”と真理値“０”とが入力したときの出力は真理値“１”となり、真理値“０”と真理値“０”とが入力したときの出力は真理値“０”となる様に設定されている。
【００３８】
上記のＯＲ回路の演算の設定を代数式で表すと、下記の式１１〜式２０の様になる。
【００３９】
（〜ｘ）＋（〜ｘ）＝〜ｘ   ・・・式１１
（〜ｘ）＋ｘ＝１           ・・・式１２
（〜ｘ）＋１＝１           ・・・式１３
（〜ｘ）＋０＝〜ｘ         ・・・式１４
ｘ＋ｘ＝ｘ               ・・・式１５
ｘ＋０＝ｘ               ・・・式１６
ｘ＋１＝１               ・・・式１７
１＋１＝１               ・・・式１８
１＋０＝１               ・・・式１９
０＋０＝０               ・・・式２０。
【００４０】
即ち本発明に係る論理シミュレーション方法は、従来と比べて、不定値に関する〜ｘ＝ｘの関係式を無くし、その代わりに、不定値の反転信号をＡＮＤ回路およびＯＲ回路の演算を規定する代数式に組み込むことにより（即ちＡＮＤ回路およびＯＲ回路での不定値の演算を上記の様に設定することにより）、不定値“ｘ”、その不定値の反転信号“〜ｘ”、真理値“０”、真理値“１”の４個の数値間のブール代数関係を正確に取り扱うことを実現し、不定値の伝播に関する、ＲＴＬ記述とネットリストとの論理シミュレーション結果の不一致を取り除く様にしたものである。
【００４１】
次に、この論理シミュレーション方法を用いた半導体回路の設計検証方法を説明する。
【００４２】
ここでは、図１のＲＴＬ記述を一例に用いて説明する。図２の回路Ｓは、図１のＲＴＬ記述を視覚的に分かり易いように図示したものである。この回路Ｓは、セレクタＳ１と、Ｄ（ディレイ）フリップフロップ回路Ｓ２と、ＡＮＤ回路Ｓ３と、ＮＯＴ回路Ｓ４とで構成されている。即ちこの回路Ｓは、不定値を出力するフリップフロップ回路を１つ含む構成となっている。セレクタＳ１は、その入力部０にＤフリップフロップ回路Ｓ２の出力信号ｄが入力され、その入力部０に外部からの信号ａが入力され、信号ｂに応じて、その入力部０に入力された信号ａまたはその入力部１に入力された信号ｄを選択的に出力信号Ｙとして出力する。Ｄフリップフロップ回路Ｓ２は、その入力部ＤにセレクタＳ２の出力信号Ｙが入力され、その入力部Ｔにクロック信号ＣＬＫが入力され、その入力部Ｄされた入力信号Ｙを、その入力部Ｔに入力されたクロック信号ＣＬＫに応じて遅延させて、その出力部Ｑから出力信号ｄとして出力する。ＡＮＤ回路Ｓ３は、その一方の入力部にＤフリップフロップ回路Ｓ２の出力信号ｄが入力され、その他方の入力部にＮＯＴ回路Ｓ４を介して外部からの信号ｂが入力され、その出力部から出力信号ｃを出力する。
【００４３】
まず、図１のＲＴＬ記述を論理シミュレーションして論理シミュレーション結果（ここでは時刻１での信号ｃ，ｄの値）を求める。
【００４４】
その際使用する論理シミュレーションとしては、背景技術の欄で説明した従来の論理シミュレーションでも上記の本発明に係る論理シミュレーション方法を用いた論理シミュレータでも、どちらの論理シミュレーションを使用してもよい。なぜならば、ＲＴＬ記述の論理シミュレーションでは、不定値の取り扱いが問題となることは無いので、どちらの論理シミュレータを使用しても同じ論理シミュレーション結果が得られるからである。
【００４５】
ここでは、背景技術の欄で示したＲＴＬ記述の論理シミュレーション結果から、ＲＴＬ記述の時刻１での信号ｃ，ｄの値は、どちらも“０”となる。
【００４６】
次に、周知の論理合成ツールを用いて、図１のＲＴＬ記述を論理合成してネットリストを作成する。そして、上記の本発明に係る論理シミュレーション方法を用いて、当該ネットリストを論理シミュレーションして論理シミュレーション結果（ここでは時刻１での信号ｃ，ｄの値）を求める。
【００４７】
ここでは、本発明に係る論理シミュレーション方法を当該ネットリストに適用した場合に、当該ネットリストがどのような動作をするか（即ちどのような論理シミュレーション結果が得られるか）を、図３の当該ネットリストの回路図を用いて説明する。
【００４８】
図３のネットリストの回路Ｒは、ＡＮＤ回路Ｒ１，Ｒ３と、ＮＯＴ回路Ｒ２，Ｒ４と、ＯＲ回路Ｒ５と、Ｄフリップフロップ回路Ｒ６とで構成されている。ＡＮＤ回路Ｒ１は、その一方の入力部にＤフリップフロップ回路Ｒ６の出力信号ｄが入力され、その他方の入力部にＮＯＴ回路Ｒ２を介して外部からの信号ｂが入力され、その出力部から信号ｃを出力する。ＡＮＤ回路Ｒ３は、その一方の入力部にＤフリップフロップ回路Ｒ６の出力信号ｄが入力され、その他方の入力部にＮＯＴ回路Ｒ４を介してＡＮＤ回路Ｒ１の出力信号ｃが入力され、その出力部から信号ｅを出力する。ＯＲ回路Ｒ５は、その一方の入力部に外部からの信号ａが入力され、その他方の入力部にＡＮＤ回路Ｒ３の出力信号ｅが入力され、その出力部から信号ｆを出力する。Ｄフリップフロップ回路Ｒ６は、その入力部ＤにＯＲ回路Ｒ５の出力信号ｆが入力され、その入力部Ｔにクロック信号ＣＬＫが入力され、その入力部Ｄされた入力信号ｆを、その入力部Ｔに入力されたクロック信号ＣＬＫに応じて遅延させて、その出力部Ｑから信号ｄとして出力する。
【００４９】
図３の信号ａ，ｂおよびクロック信号ＣＬＫの入力条件は、背景技術の欄で述べたものと同一とする（即ち時刻０の初期状態では、各信号ａ，ｂの値はそれぞれ“０”であり、Ｄフロップフロップ回路Ｒ６には、時刻１でクロック信号ＣＬＫが入力されるものとする）。
【００５０】
図３のネットリストの回路Ｒでは、まず時刻０では、クロック信号ＣＬＫが入力されていないため、信号ｄは不定値となる。
【００５１】
次に信号ｃの値は、下記の計算により不定値“ｘ”になる。
【００５２】
ｃ＝ｄ∧（〜ｂ）  
＝ｘ∧（〜０）（∵時刻０でｂ＝０）
＝ｘ∧１      （∵〜０＝１）
＝ｘ          （∵式７）。
【００５３】
次に信号ｅの値は、下記の計算により“０”になる。
【００５４】
ｅ＝ｄ∧（〜ｃ）
＝ｘ∧（〜ｘ） （∵上記の計算結果ｃ＝ｘ）
＝０           （∵式２）。
【００５５】
次に信号ｆの値は、下記の計算により“０”になる。
【００５６】
ｆ＝ａ＋ｅ
＝０＋０       （∵時刻０でａ＝０且つ上記の計算結果ｅ＝０）
＝０           （∵式２０）。
【００５７】
次に時刻１でクロック信号ＣＬＫが入力されると、信号ｄの値は、ｄ＝ｆ＝０より“０”になる。
【００５８】
従って時刻１以降での信号ｃの値は、下記の計算により“０”になる。
【００５９】
ｃ＝ｄ∧（〜ｂ）
＝０∧（〜０） （∵時刻１でｂ＝０）
＝０∧１       （∵〜０＝１）
＝０           （∵式９）。
【００６０】
以上の様に、時刻１での信号ｃ，ｄの値は、どちらも“０”となる。
【００６１】
そして次に、上記で求めたＲＴＬ記述の論理シミュレーション結果（時刻１での信号ｃ，ｄの値）とネストリストの論理シミュレーション結果（時刻１での信号ｃ，ｄの値）とを比較し、一致すれば、ネットリストはＲＴＬ記述と等価なものと判定され、一致しなければ、ネットリストはＲＴＬ記述と等価なものでないと判定される。
【００６２】
ここでは、ＲＴＬ記述の論理シミュレーション結果は、時刻１でｃ＝ｄ＝０であり、ネットリストの論理シミュレーション結果も、時刻１でｃ＝ｄ＝０であり、両者は一致するので、ネットリストはＲＴＬ記述と等価なものと判定される。
【００６３】
以上の様に本発明に係る論理シミュレーション方法によれば、論理回路が不定値を出力するフリップフロップ回路を１つ含む場合に、ＡＮＤ回路およびＯＲ回路の演算で前記不定値が適切に扱われるので、不定値伝播に関する、ＲＴＬ記述とネットリストとの論理シミュレーション結果の不一致を取り除く事ができる。
【００６４】
また本発明に係る半導体回路の設計検証方法によれば、ネットリストの論理シミュレーションに本発明に係る論理シミュレーション方法を用いるので、ネットリストがＲＴＬ記述と等価になっているかの判定を適切に行える。
【００６５】
実施の形態２．
上記の実施の形態１では、本発明に係る論理シミュレーション方法は、不定値を出力するフリップフロップ回路を１つだけ含む論理回路を対象とするものであったが、不定値を出力するフリップフロップ回路を複数含む（即ち発生原因の異なる不定値が複数存在する）論理回路を対象とする場合には、ＡＮＤ回路およびＯＲ回路の演算を以下の様に設定すればよい。
【００６６】
尚、この実施の形態では、複数のフリップフロップ回路から出力される各不定値は、識別子ｉを用いてｘ[i]と表記される。即ち、識別子ｉが異なれば、異なるフリップフロップ回路から出力された不定値（即ち別の発生原因を持つ不定値）として扱われる。
【００６７】
即ち、異なるフリップフロップ回路から出力される不定値をｘ[i]，ｘ[j]（但しi≠j）とし、それらの否定を“〜ｘ”[i]，“〜ｘ[j]”として、前記論理回路に含まれるＡＮＤ回路において、不定値“〜ｘ[i]”と不定値“〜ｘ[i]”とが入力したときの出力を不定値“〜ｘ[i]”とし、また不定値“〜ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を真理値“０”とし、また不定値“〜ｘ[i]”と真理値“１”とが入力したときの出力を不定値“〜ｘ[i]”とし、また不定値“〜ｘ[i]”と真理値“０”とが入力したときの出力を真理値“０”とし、また不定値“ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を不定値“ｘ[i]”とし、また不定値“ｘ[i]”と真理値“０”とが入力したときの出力を真理値“０”とし、また不定値“ｘ[i]”と真理値“１”とが入力したときの出力を不定値“ｘ[i]”とし、また不定値“ｘ[i]”と値“ｘ”[j]とが入力したときの出力を不定値“ｘ”とし、また不定値“〜ｘ[i]”と不定値“ｘ”[j]とが入力したときの出力を不定値“ｘ”とし、また不定値“〜ｘ[i]”と不定値“〜ｘ[j]”とが入力したときの出力を不定値“ｘ”とする様に設定する。
【００６８】
またＡＮＤ回路において、従来通り、真理値“１”と真理値“１”とが入力したときの出力は真理値“１”となり、真理値“１”と真理値“０”とが入力したときの出力は真理値“０”となり、真理値“０”と真理値“０”とが入力したときの出力は真理値“０”となる様に設定されている。
【００６９】
尚、上記の不定値“ｘ”は、〜ｘ＝ｘの関係および下記の代数式（式５〜式７および式１５〜式１７）を満たすものとする（以下同様）。
【００７０】
ｘ∧ｘ＝ｘ  ・・・式５
ｘ∧０＝０  ・・・式６
ｘ∧１＝ｘ  ・・・式７
ｘ＋ｘ＝ｘ  ・・・式１５
ｘ＋０＝ｘ  ・・・式１６
ｘ＋１＝１  ・・・式１７。
【００７１】
上記のＡＮＤ回路の演算の設定を代数式で表すと、下記の式２６〜式３５および式８〜式１０の様になる。
【００７２】
（〜ｘ[i]）∧（〜ｘ[i]）＝〜ｘ[i] ・・・式２６
（〜ｘ[i]）∧（〜ｘ[i]）＝０      ・・・式２７
（〜ｘ[i]）∧１＝〜ｘ[i]          ・・・式２８
（〜ｘ[i]）∧０＝０               ・・・式２９
ｘ[i]∧ｘ[i]＝ｘ[i]             ・・・式３０
ｘ[i]∧０＝０                   ・・・式３１
ｘ[i]∧１＝ｘ[i]                ・・・式３２
ｘ[i]∧ｘ[j]＝ｘ                ・・・式３３
（〜ｘ[i]）∧ｘ[j]＝ｘ            ・・・式３４
（〜ｘ[i]）∧（〜ｘ[j]）＝ｘ      ・・・式３５
１∧１＝１                      ・・・式８
１∧０＝０                      ・・・式９
０∧０＝０                      ・・・式１０。
【００７３】
また前記論理回路に含まれるＯＲ回路において、不定値“〜ｘ[i]”と不定値“〜ｘ[i]”とが入力したときの出力を不定値“〜ｘ[i]”とし、また不定値“〜ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を真理値“１”とし、また不定値“〜ｘ[i]”と真理値“１”とが入力したときの出力を真理値“１”とし、また不定値“〜ｘ[i]”と真理値“０”とが入力したときの出力を不定値“〜ｘ[i]”とし、また不定値“ｘ[i]”と不定値“ｘ[i]”とが入力したときの出力を不定値“ｘ[i]”とし、また不定値“ｘ[i]”と真理値“０”とが入力したときの出力を不定値“ｘ[i]”とし、また不定値“ｘ[i]”と真理値“１”とが入力したときの出力を真理値“１”とし、また不定値“ｘ[i]”と不定値“ｘ[j]”とが入力したときの出力を不定値“ｘ”とし、また不定値“〜ｘ[i]”と不定値“ｘ[j]”とが入力したときの出力を不定値“ｘ”とし、また不定値“〜ｘ[i]”と不定値“〜ｘ[j]”とが入力したときの出力を不定値“ｘ”とする様に設定する。
【００７４】
またＯＲ回路において、従来通り、真理値“１”と真理値“１”とが入力したときの出力は真理値“１”となり、真理値“１”と真理値“０”とが入力したときの出力は真理値“１”となり、真理値“０”と真理値“０”とが入力したときの出力は真理値“０”となる様に設定されている。
【００７５】
上記のＯＲ回路の演算の設定を代数式で表すと、下記の式３９〜式４８および式１８〜式２０の様になる。
【００７６】
（〜ｘ[i]）＋（〜ｘ[i]）＝〜ｘ[i]   ・・・式３９
（〜ｘ[i]）＋ｘ[i]＝１              ・・・式４０
（〜ｘ[i]）＋１＝１                 ・・・式４１
（〜ｘ[i]）＋０＝〜ｘ[i]            ・・・式４２
ｘ[i]＋ｘ[i]＝ｘ[i]               ・・・式４３
ｘ[i]＋０＝ｘ[i]                  ・・・式４４
ｘ[i]＋１＝１                     ・・・式４５
ｘ[i]＋ｘ[j]＝ｘ                  ・・・式４６
（〜ｘ[i]）＋ｘ[j]＝ｘ              ・・・式４７
（〜ｘ[i]）＋（〜ｘ[j]）＝ｘ        ・・・式４８
１＋１＝１                        ・・・式１８
１＋０＝１                        ・・・式１９
０＋０＝０                        ・・・式２０。
【００７７】
以上の本発明に係る論理シミュレーション方法によれば、論理回路が不定値を出力するフリップフロップ回路を複数含む場合でも、ＡＮＤ回路およびＯＲ回路の演算で前記不定値が適切に扱われるので、不定値の伝播に関する、ＲＴＬ記述とネットリストとの論理シミュレーション結果の不一致を取り除く事ができる。そして、この論理シミュレーション方法を用いた半導体回路の設計検証方法によれば、論理回路が不定値を出力するフリップフロップ回路を複数含む場合でも、ネットリストがＲＴＬ記述と等価になっているかの判定を適切に行える。
【図面の簡単な説明】
【００７８】
【図１】ＲＴＬ記述の一例を示した図である。
【図２】図１のＲＴＬ記述を視覚的にわかりやすいように回路図にした図である。
【図３】図１のＲＴＬ記述を論理合成して得られたネットリストの回路図を示した図である。
【符号の説明】
【００７９】
Ｓ１，Ｒ６  セレクタ、Ｓ２  Ｄフリップフロップ回路、Ｓ３，Ｒ１，Ｒ２  ＡＮＤ回路、Ｓ４，Ｒ２，Ｒ４  ＮＯＴ回路、Ｒ５  ＯＲ回路。  
【図１】
2008158652.tif 000002
【図２】
2008158652.tif 000003
【図３】
2008158652.tif 000004