(57)【要約】【課題】マルチサイクルパスや非同期パスを有する論理回路のハザードをチェックする。【解決手段】論理回路中の全ブロックの連言標準形が予め埋め込まれていないなら、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換する手段、論理回路から信号情報で記述された各終点についてトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、数字をアサインする手段、論理回路から、信号情報で記述された各終点について、トレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力する手段、論理回路から、信号情報で記述された各終点について、各ネットに対して、数字に相当する論理を回路連言標準形に追加する手段と、境界条件設定部と判定部を備える。【選択図】図１
2007304699.tif 000002
【特許請求の範囲】
【請求項１】
論理回路を読み込むステップと、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、
論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、
を備えることを特徴とする回路連言標準形生成方法。
【請求項２】
論理回路を読み込むステップと、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、
論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、
前記回路連言標準形を充足可能性判定することによりハザードチェックするステップと、
を備えることを特徴とするハザードチェック方法。
【請求項３】
論理回路を読み込む手段と、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換する手段と、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインする手段と、
論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力する手段と、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加する手段と、
を備えることを特徴とする回路連言標準形生成装置。
【請求項４】
論理回路を読み込む手段と、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換する手段と、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインする手段と、
論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力する手段と、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加する手段と、
前記回路連言標準形を充足可能性判定することによりハザードチェックする手段と、
を備えることを特徴とするハザードチェック装置。
【請求項５】
請求項１又は２に記載の方法をコンピュータに行わせるためのプログラム。
【請求項６】
請求項５に記載のプログラムを記録したことを特徴とするコンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、論理回路のハザードをチェックするためのハザードチェック方法及びハザードチェック装置並びに該ハザードチェック方法及びハザードチェック装置で利用する回路連言標準形を生成するための回路連言標準形生成方法及び回路連言標準形生成装置に関する。
【背景技術】
【０００２】
論理合成システムは、機能記述されたハードウエア記述と、論理的に等価な回路を合成するが、１相同期回路を前提に開発されているので、グリッチ発生に関する考慮は全く行われていない。
【非特許文献１】「計算論理入門」  法政大学名誉教授    田中尚夫  著  １１８〜１２４頁  １９９７年１０月刊行  ＩＳＢＮ４−７８５３−１５０５−９  ５  命題論理に関する計算量問題  ５．１  充足可能性問題
【非特許文献２】「計算理論とオートマトン言語理論−コンピュータの原理を明かす−」  東北大学教授    丸岡  章  著  ２３４〜２４１頁  ＩＳＢＮ４−７８１９−１１０４−８  ２００５年１１月刊行  サイエンス社刊行  ９．６  回路の充足可能性問題の式充足可能性問題への帰着
【非特許文献３】GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, Vol.48, No.5, 1999, pp.506-521
【発明の開示】
【発明が解決しようとする課題】
【０００３】
ただ、１相同期で全ての回路を設計することは少なく、実際は、マルチサイクルパスや非同期パスが部分的に存在している。この部分において、ハザードが発生していることをチェックする方法が無かった。
【０００４】
ハードウエア記述言語で書かれた機能を、論理回路として生成する論理合成では、ハードウエア記述言語で書かれた論理通りの回路を生成するが、論理最適化の際にグリッチは考慮していない。そこで、非同期パスやマルチサイクルパスのようなタイミング例外のパスの合成において、グリッチが発生し、かつフリップ・フロップがデータを取り込むタイミングで伝わると、ハザードとなり、回路が誤動作してしまう。しかしながら、このハザードを検出する方法が無かった。
【０００５】
タイミング例外におけるハザードの発生は、次のようなケースに代表される。まず、ハードウエア記述言語としては、図２のように、タイミング例外のパスからデータを取り込んで良いかどうかを制御する制御信号（ストローブ信号）を設け、その信号が０の時は、タイミング例外のパスは確定していないので取り込まず、逆に１の時に取り込むという記述を行う。図２では、制御信号が０の時は、フリップ・フロップに非同期、マルチサイクルパスの信号の変化が必ず伝播しないように設計している。
【０００６】
しかし、論理合成システムが図３の回路を生成してしまう可能性がある。この回路は論理的には図２と等価であるが、タイミング例外のパスの影響が、制御信号が０の時であってもフリップ・フロップにデータの変化が伝播してしまう。この変化している時に、フリップ・フロップのクロック信号が立ち上がると、論理誤動作（ハザード）が発生する。
【０００７】
尚、本例では、制御信号とタイミング例外信号のＡＮＤ論理で、信号伝播を制御する方式を示したが、ＡＮＤ以外に、ＯＲやセレクタ論理で制御する方法も存在する。
【０００８】
本発明は、マルチサイクルパスや非同期パスを有する論理回路のハザードをチェックするためのハザードチェック方法及びハザードチェック装置並びに該ハザードチェック方法及びハザードチェック装置で利用する回路連言標準形を生成するための回路連言標準形生成方法及び回路連言標準形生成装置を提供することを目的とする。
【課題を解決するための手段】
【０００９】
本発明の第１の観点によれば、論理回路を読み込むステップと、もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、を備えることを特徴とする回路連言標準形生成方法が提供される。
【００１０】
本発明の第２の観点によれば、論理回路を読み込むステップと、もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、前記回路連言標準形を充足可能性判定することによりハザードチェックするステップと、を備えることを特徴とするハザードチェック方法が提供される。
【発明の効果】
【００１１】
第１の効果は、ハザードの発生を網羅的にチェックできることにある。
【００１２】
その理由は、ハザード発生の可能性を充足可能性問題に変換し、それを網羅的に確認しているためである。
【発明を実施するための最良の形態】
【００１３】
以下、図面を参照して本発明を実施するための最良の形態について詳細に説明する。
【００１４】
本発明では、非同期パスやマルチサイクルパスのようなタイミング例外のパスにおいて、論理合成システムが合成した回路に、ハザードが発生していないかどうかを、網羅的にチェックする。
【００１５】
図１を用いて説明を行う。入力装置１から、本方式の起動が行われる。論理抽出部２１は、論理合成の結果である論理合成後の論理回路３１を読み込み、信号情報３３で記述された検証対象のフリップ・フロップの入力ピンや回路の出力から、その入力側を、フリップ・フロップまたは回路の入力までをトレースし、論理ライブラリ３２に格納されている各ブロックの論理情報を参照して、対象部分の回路の論理動作を、３値（０，１，Ｘ）の回路動作で表現したものを回路連言標準形３４として出力する。
【００１６】
境界条件設定部２２は、信号情報３３を読み、タイミング例外信号（非同期信号やマルチサイクル信号）にはＸ値を、制御信号にはタイミング例外信号が伝播しないように設定された論理値（指定された値）を、その他の信号（通常の同期信号）には０、または１の両方の論理値が取れるという指定を、回路連言標準形３４へ追加する。
【００１７】
充足可能性判定部２３は、回路連言標準形３４を読み、これを満足する解があるかを網羅的に探索を行う。
【００１８】
なお、充足可能性判定部２３は、従来からある部分であり、回路連言標準形を生成するまでの部分が本発明に従った部分である。回路連言標準形は、従来からの充足可能性判定部２３が読めるものであるが、本発明に従ったものである。
【００１９】
結果出力部２４は、充足可能性判定部２３が、充足解を発見すればハザードがあり、充足解が無ければハザードが存在しないことを検証結果３５へレポートする。
【００２０】
次に、本発明の実施形態の構成について図面を参照して詳細に説明する。
【００２１】
図１を参照して構成を説明する。
【００２２】
本発明は、キーボード等の入力装置１と、プログラム制御により動作するデータ処理装置２と、情報を記憶する記憶装置３とを含む。
【００２３】
記憶装置３は、論理回路３１、論理ライブラリ３２、信号情報３３、回路連言標準形３４、検証結果３５をデータとして格納している。
【００２４】
論理回路３１は、チェック対象の論理回路である。
【００２５】
論理ライブラリ３２は、各ゲートの論理を表現したライブラリである。
【００２６】
信号情報３３は、タイミング例外のパスの始点終点信号名と、タイミング例外信号を制御するストローブ信号名と、その信号がタイミング例外信号を伝播しない時の論理値の一覧である。
【００２７】
回路連言標準形３４は、検証対象部分を、連言標準形で表した式である。なお、回路連言標準形とは、図１１に示すような形式であり、和積のブール式の形式を有する。
【００２８】
検証結果３５は、ハザードが発生するかどうかのチェック結果である。
【００２９】
データ処理装置２は、論理抽出部２１と、境界条件設定部２２と、充足可能性判定部２３と、結果出力部２４を備える。
【００３０】
論理抽出部２１は、論理回路３１を読み込み、信号情報３３に記載されたタイミング例外信号の終点となるフリップ・フロップや回路の出力を１つずつ取り出し、その入力側をフリップ・フロップまたは回路の入力までトレースし、その入力側の論理を、論理ライブラリ３２を参照し、回路連言標準形３４へ変換を行う。
【００３１】
境界条件設定部２２は、信号情報３３を参照し、タイミング例外信号の始点、終点に関してはＸ値を、ストローブ信号に関しては指定された論理値を、その他の入力信号に関しては１サイクル信号である指定を回路連言標準形３４に追加出力する。
【００３２】
充足可能性判定部２３は、回路連言標準形３４を読み込み、その連言標準形を満足する解、つまりは終点にＸ値が伝播する場合が存在するかどうかを網羅的に判定する。
【００３３】
結果出力部２４は、充足解が存在すれば、この回路はハザード発生の可能性あり、解が存在しなければハザードの可能性が無しと、検証結果３５へレポートする。
【００３４】
次に、図１を参照して本発明の第１の実施形態の動作について詳細に説明する。
【００３５】
まず、図４が入力となる論理回路３１の例である。
【００３６】
また、図５が信号情報３３の例である。ここで、１行目では、multi_async という入力（図４に存在）から、A_regというレジスタ（図４に存在）のパスが、非同期パスであり、１サイクル動作でないタイミング制約のないフォルスパスであることを示している。２行目では、strbという入力（図４に存在）が制御信号であり、その値が０の時に、前述のパスが活性化されない（信号が伝播しない）はずであることを示している。
【００３７】
詳細説明の前に、本方式で扱う、論理表現を説明する。本方式では、回路の動作を０、１、Ｘの３値で扱うが、一般の充足可能性問題は、０、１の２値しか扱えないので、０、１、Ｘを２つの変数を用いた内部表現で行う。その例を図６に示す。０は（０，０）, １は（０，１）, Ｘは（１，１）で表現する。尚、（１，０）は存在しない（ここでは、この割り当てを用いたが、他の組み合わせも可能）。
【００３８】
この論理値を使用した場合に、簡単な例として、図７のＮＯＲゲートの入力と出力の関係を表であらわすと、図８のようになる。例えば、一方の入力である（ｉ１，ｉ２）と他方の入力である（ｊ１，ｊ２）がそれぞれ（０，０）と（０，１）の場合は（０，０）が出力されることを示している。これは、２値論理でいう、０と１が入力された時は、０が出力されることと等価である。この結果から、図９のような真理値表が導かれる（この真理値表も一意ではない）。
この真理値表から、図１０の上式で示されたような、Ａ−＞Ｂ（式1）（Ａが成立すれば、Ｂも成立すること示す。）という関係に変換する。また、図１０に示されたように、Ａ−＞Ｂは、Ａ’＋Ｂ＝１  （式2）というブール式に変換できる。ここで「’」は論理反転を示す。
【００３９】
図１１の各式は、図９の真理値表の各行をＡ−＞Ｂ形式に変換し、更に、それを（式２）の形式に変換した結果を示している。例えば、
ｉ１’＊ｉ２→ｏ１’＊ｏ２’
は、図９の第１行を（式１）の形式で表したものであり、
（ｉ１＋ｉ２’＋ｏ１’）（ｉ１＋ｉ２’＋ｏ２’）
は、図９の第１行を（式２）の形式で表したものである。
【００４０】
２入力ＮＯＲゲートにおいては、常に図１１中の式が成り立たつはずなので、まとめると以下の式３が常に成り立つことになる。
【００４１】
（ｉ１＋ｉ２’＋ｏ１’）×（ｉ１＋ｉ２’＋ｏ２’）
×（ｊ１＋ｊ２’＋ｏ１’）×（ｊ１＋ｊ２’＋ｏ２’）
×（ｉ１＋ｉ２＋ｊ１＋ｊ２＋ｏ１’）×（ｉ１＋ｉ２＋ｊ１＋ｊ２＋ｏ２）
×（ｉ１’＋ｉ２’＋ｊ１＋ｊ２＋ｏ１）
×（ｉ１’＋ｉ２’＋ｊ１＋ｊ２＋ｏ２）
×（ｉ１＋ｉ２＋ｊ１’＋ｊ２’＋ｏ１）
×（ｉ１＋ｉ２＋ｊ１’＋ｊ２’＋ｏ２）
×（ｉ１’＋ｉ２’＋ｊ１’＋ｊ２’＋ｏ１）
×（ｉ１’＋ｉ２’＋ｊ１’＋ｊ２’＋ｏ２）
＝１                        （式３）
すなわち、図９の各行を（式２）の形式で表したものの積が（式３）の左辺である。
【００４２】
これを、データ処理装置（コンピュータ）２が扱いやすい形式に変換するために、次のような変換を行う。すなわち、ｉ１を１、ｉ２を２、ｊ１を３、ｊ２を４、ｏ１を５、ｏ２を６と表し、各々の否定（論理反転）をマイナスで表す。また、（式３）において、括弧（各項）内の式を１行で表し、＋  （ｏｒ）は省略し（表示せず）、ブランクとする。この結果を、図１２に示す。すなわち、（式３）を、図１２に示すような形式で表すことにより、充足可能性判定部２３が入力できるようになる。なお、各行の最後の０は項の終端であることを示している。このフォーマットは一般に当業者の間でＣＮＦとも呼ばれることがあるが、本発明では、連言標準形と呼ぶ。本システムでは、論理回路で使用される組み合わせ論理回路素子の連言標準形を内部に予め埋め込んでおく。
【００４３】
次に、動作の説明を行う。
【００４４】
論理回路抽出部２１は、次のステップから構成される。
【００４５】
ステップ１：論理回路３１を読み込む。もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換する。一般に、インバータと２入力ＮＯＲゲートがあれば、全ての論理回路を等価変換できることが知られている。
【００４６】
ステップ２：論理回路３１から、信号情報３３で記述された終点を順次１つ選択する。全ての終点に対し、以下のステップを行う。
【００４７】
ステップ３：選択された終点から、入力側をトレースし、各ネットに対して、１から順番に２つの数字（ｎ１，ｎ２）をアサインする（終点から遡及して最初のネットは、（１，２）となり、以下（３，４）（５，６）と続く。トレースは、回路の入力、フリップ・フロップまで行う）。
【００４８】
ステップ４：再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリ３２を参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形３４として出力する。
【００４９】
ステップ５：各ネットに対して、（１，０）の組み合わせはありえないので、 ｎ１’＋ｎ２（式４）に相当する論理を回路連言標準形３４に追加する。
【００５０】
上記のステップを、図４、図５の例を参考に説明する。
【００５１】
ステップ１：論理回路３１を読み込む。図４を読み込んだことになるが、この例では組み合わせ回路のブロックは２入力のＮＯＲしか存在しないので、次のステップへ進む。
【００５２】
ステップ２：信号情報３３（図５）を読み、終点はＡ＿ｒｅｇ１つであることを設定する。
【００５３】
ステップ３：Ａ＿ｒｅｇから、入力方向にトレースを行い、ネットＮ００１に（１，２）、Ｎ００３に（３，４）、ｍｕｌｔｉ＿ａｓｙｎｃに（５，６）、ｏｔｈｅｒに（７，８）、Ｎ００２に（９，１０）、ｓｔｒｂに（１１，１２）をアサインする。本例では、ブロックの下の入力ＰＩＮから順にトレースしているが、上のＰＩＮからトレースしても良い。
【００５４】
ステップ４：再度、Ａ＿ｒｅｇから、入力側をトレースする。まず、Ｕ０１の論理ライブラリ３２を参照すると、２入力ＮＯＲゲートであるので、埋め込まれている２入力ＮＯＲゲートの連言標準形を取り出す。これは図１２である。ただし、番号は、ノードの番号に合わせる。すなわち、図１２は入力が（１，２）（３，４）で出力が（５，６）の場合であるが、Ｕ０１の入力はＮ００３の（３，４）と、Ｎ００２の（９，１０）、出力はＮ００１の（１，２）なので、それに置き換えて、回路連言標準形３４へ出力する。その結果は、図１３の１行目から１２行目にあたる。
【００５５】
以下、全ゲートに対して同様な処理を行うと、図１３の３６行目までが生成される。
【００５６】
ステップ５：全ネットに対して、式４に当てはまる論理を出力する。例えば、ネットＮ００１は、−１  ２  であり、その結果は、図１３の３７行目から４２行目にあたる。なお、図１３においては、１行目から２４行目までを左側に描き、２５行目以降を右側に描いている。
【００５７】
境界条件設定部２２は、信号情報２２を読み、終点にＸに相当する（１，１）を、回路連言標準形３４に追加出力する。但し、式１より、（１，？）という指定でも、（１，１）と等価になるので、（１，１）の代わりに（１，？）を出力する。
【００５８】
制御信号には指定された論理値を、追加出力する。すなわち、０が指定されていれば（０，０）を回路連言標準形３４に追加出力し、１が指定されていれば（０，１）を追加出力する。
【００５９】
タイミング例外信号の始点に関しては、Ｘに相当する（１，１）を、回路連言標準形３４に追加出力する。但し、式１より、（１，？）という指定でも、（１，１）と等価になるので、（１，１）の代わりに（１，？）を出力する。
【００６０】
その他の信号は、０か１のどちらかを取りえるので、（０，？）を回路連言標準形３４に追加出力する。（？は指定しない事を意味する）。
【００６１】
図５の場合は、Ａ＿ｒｅｇ．に対して、Ｘに相当する（１，？）を設定するが、そのネットはＮ００１で（１，２）にアサインされているので、１を出力する（図１３の４３行目）。
【００６２】
multi_asyncはタイミング例外信号なので（１，？）を与える。その際、multi_asyncのネットは（５，６）にアサインされているので、５を出力する（図１３の４４行目）。
【００６３】
制御信号として、ｓｔｒｂに０が与えられているので、（０，０）を設定する。ｓｔｒｂネットは、（１１，１２）にアサインされているので、−１１と−１２を出力する（図１３の４５、４６行目）。
【００６４】
その他の信号ｏｔｈｅｒは０か１であり、ネットｏｔｈｅｒは（７，８）にアサインされているので、−７を出力する（図１３の４７行目）。
【００６５】
以上で、回路連言標準形３４には、制御信号が与えられた論理値の場合で、かつタイミング例外信号の始点をＸとした条件で、他の入力信号を０、１全ての組み合わせを網羅的に考えた上で、タイミング例外信号の終点がＸになる場合があるかどうかを充足判定する式になっている。
【００６６】
充足可能性判定部２３は、回路連言標準形３４を読み、これを満足する場合が存在するかどうかを網羅的に探索し、充足解があればその解を、無ければ充足解なしと判定する。今回の例の場合は、充足解なしと判定される。
【００６７】
結果出力部２４は、充足解が無ければハザードがなし、充足解があればハザードの可能性ありと、検証結果３５へレポートする。
【００６８】
次に、本発明の第１の実施形態の効果について説明する。
【００６９】
本発明の第１の実施形態では、論理抽出部２１と境界条件設定部２２で作成された回路連言標準形３４を、充足可能性判定部２３で網羅的にハザードの発生する可能性を探索するというように構成されているため、ハザード伝播の可能性を完全にチェックできる。
【図面の簡単な説明】
【００７０】
【図１】本発明の実施形態１によるハザードチェック装置の構成を示すブロック図である。
【図２】論理合成する前の回路例を示す回路図である。
【図３】図２に示す回路を論理合成装置にかけた場合に生成される回路例を示す回路図である。
【図４】本発明の実施形態によるハザードチェック装置がチェックの対象とする回路の例を示す回路図である。
【図５】図４に示す回路における信号情報の例を示す図である。
【図６】本発明の実施形態による３値表現を示す図である。
【図７】本発明の実施形態による３値表現をＮＯＲゲートに適用した場合に現れるパラメータを示す図である。
【図８】本発明の実施形態による３値表現によりＮＯＲゲートの入出力関係を表した表である。
【図９】本発明の実施形態による３値表現によりＮＯＲゲートの入出力関係を表した別の表である。
【図１０】本発明の実施形態で利用する論理変換を示す図である。
【図１１】本発明の実施形態においてＮＯＲゲートを回路連言標準形で表現した式を表す図である。
【図１２】図１１に示す式を充足可能性判定部が入力できるように変換した数列を示す図である。
【図１３】図４に示す回路のハザードをチェックするための回路連言標準形を表す数列を示す図である。
【符号の説明】
【００７１】
２１  論理抽出部
２２  境界条件設定部
２３  充足可能性判定部
２４  結果出力部
３１  論理回路
３２  論理ライブラリ
３３  信号情報
３４  回路連言標準形
３５  検証結果
【図１】
2007304699.tif 000003
【図２】
2007304699.tif 000004
【図３】
2007304699.tif 000005
【図４】
2007304699.tif 000006
【図５】
2007304699.tif 000007
【図６】
2007304699.tif 000008
【図７】
2007304699.tif 000009
【図８】
2007304699.tif 000010
【図９】
2007304699.tif 000011
【図１０】
2007304699.tif 000012
【図１１】
2007304699.tif 000013
【図１２】
2007304699.tif 000014
【図１３】
2007304699.tif 000015
【手続補正書】
【提出日】平成19年5月25日(2007.5.25)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
論理回路を読み込むステップと、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップ（始点）まで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、
論理回路から、信号情報で記述された各終点について、再度、終点から始点まで入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、
を備えることを特徴とする回路連言標準形生成方法。
【請求項２】
論理回路を読み込むステップと、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップ（始点）まで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、
論理回路から、信号情報で記述された各終点について、再度、終点から始点まで入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、
論理回路から、信号情報で記述された各始点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、
前記回路連言標準形を充足可能性判定することによりハザードチェックするステップと、
を備えることを特徴とするハザードチェック方法。
【請求項３】
論理回路を読み込む手段と、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換する手段と、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップ（始点）まで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインする手段と、
論理回路から、信号情報で記述された各終点について、再度、終点から始点まで入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力する手段と、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加する手段と、
を備えることを特徴とする回路連言標準形生成装置。
【請求項４】
論理回路を読み込む手段と、
もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換する手段と、
論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップ（始点）まで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインする手段と、
論理回路から、信号情報で記述された各終点について、再度、終点から始点まで入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力する手段と、
論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加する手段と、
論理回路から、信号情報で記述された各始点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加する手段と、
前記回路連言標準形を充足可能性判定することによりハザードチェックする手段と、
を備えることを特徴とするハザードチェック装置。
【請求項５】
請求項１又は２に記載の方法をコンピュータに行わせるためのプログラム。
【請求項６】
請求項５に記載のプログラムを記録したことを特徴とするコンピュータ読み取り可能な記録媒体。
【手続補正２】
【補正対象書類名】明細書
【補正対象項目名】０００９
【補正方法】変更
【補正の内容】
【０００９】
本発明の第１の観点によれば、論理回路を読み込むステップと、もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップ（これらを始点と呼ぶ）まで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、を備えることを特徴とする回路連言標準形生成方法が提供される。
【手続補正３】
【補正対象書類名】明細書
【補正対象項目名】００１０
【補正方法】変更
【補正の内容】
【００１０】
本発明の第２の観点によれば、論理回路を読み込むステップと、もし、論理回路中の全ブロックの連言標準形が予め埋め込まれていない場合は、連言標準形が予め埋め込まれているブロックだけの論理回路に等価変換するステップと、論理回路から、信号情報で記述された各終点について、終点から入力側をトレースし、回路の入力、フリップ・フロップまで、各ネットに対して、２つの数字（ｎｉ，ｎｊ）をアサインするステップと、論理回路から、信号情報で記述された各終点について、再度、終点から入力側をトレースし、各ブロックに対して、論理ライブラリを参照し、それと同じ論理の連言標準形を検索し、接続されているネットにアサインされた数字に連言標準形を置き換えて、回路連言標準形として出力するステップと、論理回路から、信号情報で記述された各終点について、各ネットに対して、ｎｉ’＋ｎｊ（「’」は論理否定を示す。）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各終点について、終点のハザードｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、タイミング例外信号が存在するネットに対して、ｎｉに相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、論理値０が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ’）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、論理値１が指定された信号が存在するネットに対して、（ｎｉ’、ｎｊ）に相当する論理を回路連言標準形に追加するステップと、論理回路から、信号情報で記述された各始点について、論理値が指定されない信号が存在するネットに対して、ｎｉ’に相当する論理を回路連言標準形に追加するステップと、前記回路連言標準形を充足可能性判定することによりハザードチェックするステップと、を備えることを特徴とするハザードチェック方法が提供される。
【手続補正４】
【補正対象書類名】明細書
【補正対象項目名】００１５
【補正方法】変更
【補正の内容】
【００１５】
図１を用いて説明を行う。入力装置１から、本方式の起動が行われる。論理抽出部２１は、論理合成の結果である論理合成後の論理回路３１を読み込み、信号情報３３で記述された検証対象のフリップ・フロップの入力ピンや回路の出力から、その入力側を、フリップ・フロップまたは回路の入力（始点）までをトレースし、論理ライブラリ３２に格納されている各ブロックの論理情報を参照して、対象部分の回路の論理動作を、３値（０，１，Ｘ）の回路動作で表現したものを回路連言標準形３４として出力する。
【手続補正５】
【補正対象書類名】明細書
【補正対象項目名】００３６
【補正方法】変更
【補正の内容】
【００３６】
また、図５が信号情報３３の例である。ここで、１行目では、multi_async という入力（始点）（図４に存在）から、A_regというレジスタ（終点）（図４に存在）のパスが、非同期パスであり、１サイクル動作でないタイミング制約のないフォルスパスであることを示している。２行目では、strbという入力（図４に存在）が制御信号であり、その値が０の時に、前述のパスが活性化されない（信号が伝播しない）はずであることを示している。
【手続補正６】
【補正対象書類名】明細書
【補正対象項目名】００５７
【補正方法】変更
【補正の内容】
【００５７】
境界条件設定部２２は、信号情報２２を読み、終点にＸに相当する（１，１）を、回路連言標準形３４に追加出力する。但し、式１より、（１，？）という指定でも、（１，１）と等価になるので、（１，１）の代わりに（１，？）を出力する。
【手続補正７】
【補正対象書類名】明細書
【補正対象項目名】００５８
【補正方法】変更
【補正の内容】
【００５８】
制御信号（始点）には指定された論理値を、追加出力する。すなわち、０が指定されていれば（０，０）を回路連言標準形３４に追加出力し、１が指定されていれば（０，１）を追加出力する。
【手続補正８】
【補正対象書類名】明細書
【補正対象項目名】００５９
【補正方法】変更
【補正の内容】
【００５９】
タイミング例外信号の始点に関しては、Ｘに相当する（１，１）を、回路連言標準形３４に追加出力する。但し、式１より、（１，？）という指定でも、（１，１）と等価になるので、（１，１）の代わりに（１，？）を出力する。
【手続補正９】
【補正対象書類名】明細書
【補正対象項目名】００６０
【補正方法】変更
【補正の内容】
【００６０】
その他の始点の信号は、０か１のどちらかを取りえるので、（０，？）を回路連言標準形３４に追加出力する。（？は指定しない事を意味する）。