(57)【要約】【課題】本発明は、シーケンシャル回路の、ある期間にわたる入力の関数としての出力における変動が、検査及び確認を妨げる虞を抑制することを目的とする。【解決手段】本発明による処理システムは、これらシステムの二進時間フレーム展開を利用してシーケンシャルシステムの分析を行う。この展開手法は、入力及び時間についての値が、様々な出力及び状態を生成する変数として取り扱われるモデルを与える。【選択図】　図１
2004046821.tif 000002
【特許請求の範囲】
【請求項１】
シーケンシャルシステムを分析する方法であって：
シーケンシャルシステムの分析のための最大時間フレームを決定するステップであって、前記最大時間フレームがｎビット二進値を利用して表現することが可能であるところのステップ；
前記シーケンシャルシステムの二進時間フレーム展開されたモデルを作成するステップであって、前記二進時間フレーム展開されたモデルが、カスケード接続されたｎ個の二進時間フレームクローズを有するところのステップ；
前記二進時間フレーム展開されたモデルを利用して前記シーケンシャルシステムを分析するステップ；及び
分析報告を作成するステップ；
を有することを特徴とする方法。
【請求項２】
クローズの各々が、ゼロに等しいｐ値を有するクローズの先頭からカウントされる相対的な位置ｐを有し；及び
前記クローズの各々が、前記シーケンシャルシステムの一連の２ｐ個の同一物より成ることを特徴とする請求項１記載の方法。
【請求項３】
前記クローズの各々が：
初期状態及び２ｐ個の入力一式を受信し；及び
前記初期状態及び２ｐ個の入力一式を利用して、結果の状態及び２ｐ個の出力一式を生成することを特徴とする請求項２記載の方法。
【請求項４】
前記クローズの各々について：
前記シーケンシャルシステムの第１の同一物が、前記入力一式の第１のもの及び初期状態を受信し、出力一式の第１のもの及び状態を生成し；及び
前記シーケンシャルシステムの後続の各同一物が、その系列におけるシーケンシャルシステムの同一物の先行するものから入力一式の後続のもの及び状態を受信し、出力一式の後続のもの及び状態を生成することを特徴とする請求項３記載の方法。
【請求項５】
前記クローズの各々が初期状態を受信し、結果の状態を生成し、該結果の状態は、初期状態及びシーケンシャルシステムの一連の同一物から生成された状態の間で選択されることを特徴とする請求項２記載の方法。
【請求項６】
更に、各クローズに対して、初期状態と、分析中の時間フレームの二進標記におけるｐ番目の数値に基づいて、シーケンシャルシステムの一連の同一物から生成された状態との間で選択が行われることを特徴とする請求項５記載の方法。
【請求項７】
更に、各クローズに対して：
前記二進標記におけるｐ番目の数がゼロの値を有するならば、初期状態を選択し；及び
前記二進標記におけるｐ番目の数が１の値を有するならば、前記シーケンシャルシステムの一連の同一物から生成された状態を選択することを特徴とする請求項６記載の方法。
【請求項８】
前記シーケンシャルシステムを分析するステップが：
前記シーケンシャルシステムについての所望の状態を特定するステップ；及び前記所望の状態になる入力ベクトルを特定するために前記二進時間フレーム展開されたモデルを分析するステップ；
より成ることを特徴とする請求項１記載の方法
【請求項９】
分析報告を作成するステップが：
前記分析が前記所望の状態を与える入力ベクトルを見出したか否かを判定するステップ；
前記分析が前記入力ベクトルを見出したならば、前記分析報告にて前記入力ベクトルを特定するステップ；及び
前記分析が前記入力ベクトルを見出さなかったならば、前記分析報告にて前記所望の状態は実行不可能な問題であることを示すステップ；
より成ることを特徴とする請求項８記載の方法。
【請求項１０】
前記シーケンシャルシステムが、複数の論理要素及び少なくとも１つのメモリ要素を揺する半導体装置より成り、前記メモリ要素が前記論理要素の少なくとも１つによって使用される状態情報を保持することを特徴とする請求項１記載の方法。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、一般にシステムのモデル化及び分析に関連し、特にシーケンシャルシステムの二進時間フレーム展開に関連する。
【０００２】
【従来の技術】
一般に、システム及び回路は、組み合わせ（ｃｏｍｂｉｎａｔｉｏｎａｌ）又はシーケンシャル（ｓｅｑｕｅｎｔｉａｌ）の２つのカテゴリの何れかに分類される。組み合わせ回路は、純粋に入力の関数として出力を生成する。シーケンシャル回路は、時間変化する状態と供に、入力及び現在状態の関数として出力を生成する。組み合わせ回路については、アルゴリズムは、その論理を迅速に検査及び確認することが可能である。
【０００３】
【発明が解決しようとする課題】
しかしながら、シーケンシャル回路については、期間にわたる入力の関数としての出力における変動が、検査及び確認を妨げる虞がある。
【０００４】
【課題を解決するための手段】
本発明によれば、シーケンシャルシステムの二進時間フレーム展開についての技術が与えられる。特定の実施例による手法は、二進形式で、ある期間にわたるシーケンシャルシステムの分析を可能にする。
【０００５】
一実施例によれば、シーケンシャルシステムを分析する方法は、シーケンシャル回路の分析のための最大時間フレームを決定し、その最大時間フレームはｎビット二進値を利用して表現することが可能であり、前記シーケンシャル回路の二進時間フレーム展開されたモデルを作成し、その二進時間フレーム展開されたモデルは、カスケード接続されたｎ個の二進時間フレームクローズを有する。本方法は、更に、二進時間フレーム展開されたモデルを利用して前記シーケンシャル回路を分析し、及び分析報告を作成する。
【０００６】
本発明の実施例は、様々な技術的優位性を与える。これらの手法は、シーケンシャルシステムの速やかな分析を可能にし、シーケンシャルシステムの分析の間の多数の時間フレームにわたって二進サーチ（ｂｉｎａｒｙ　ｓｅａｒｃｈ）を行うことを可能にする。このことは、論理分析中の計算時間を削減することを可能にし、割り当てられたＣＰＵ時間、シーケンシャルシステムの所与の特定の出力の中で、解又はソリューションを見出す確率を向上させることが可能である。
【０００７】
本発明の他の利点は、以下の明細書、請求の範囲及び図面により、当業者に適切に理解されるであろう。更に、具体的な利点が上記に示されたが、様々な実施例は、列挙された利点の全部若しくは一部を包含する又は包含しない場合もある。
【０００８】
【発明の実施の形態】
本発明及びその利点をより深く理解するために、添付図面と供に詳細な説明が行われる。
【０００９】
図１は、ディスプレイ１２，入力１４，プロセッサ１６及びメモリ１８を包含する、１０にて示される処理システムを示す。図示された例では、メモリ１８は、二進時間展開処理モジュール２０と、システム分析モジュール２２と、動作管理及び監督（ＯＡＭ：ｏｐｅｒａｔｉｏｎｓ　ａｄｍｉｎｉｓｔｒａｔｉｏｎ　ａｎｄ　ｍａｎａｇｅｍｅｎｔ）モジュール２４と、シーケンシャルシステムデザイン２６及びログ（ｌｏｇ）２８を保持する。概して、システム１０は、シーケンシャル回路の分析を支援するために、二進時間フレーム展開（ｂｉｎａｒｙ
ｔｉｍｅ−ｆｒａｍｅ　ｅｘｐａｎｓｉｏｎ）をサポートする。
【００１０】
システム１０は、シーケンシャルシステムの二進時間フレーム展開を実現し、その結果生じる分析用のモデルを利用する要素の、ある適切な組み合わせ及び配置を表現する。従って、デスクトップコンピュータとして図示されているが、システム１０は、その特徴及び機能を実現するのに適切なハードウエア及び／又は論理を包含し得る。ユーザとのインターフェースについては、システム１０はディスプレイ１２及び入力１４を含む。ディスプレイ１２は、ユーザに対する情報の提示を支援し、入力１４はユーザからの情報の受け取りを支援する。例えば、ディスプレイ１２はコンピュータモニタであり、入力１４はキーボード及びマウスであり得る。
【００１１】
プロセッサ１６は、演算する及び処理する機能を与える適切なハードウエア、ファームウエア及び／又はその他の要素を示す。例えば、プロセッサ１６は、１つ又はそれ以上の特定用途の及び／又は汎用のマイクロプロセッサを含むことが可能である。図示された例では、プロセッサ１６は、メモリ１８内に維持される情報にアクセスすることによって、特性及び機能を提供する。
【００１２】
メモリ１８は、任意の適切な局所的な又は分散されたメモリ格納装置を示す。図示された例では、メモリ１８は、二進時間フレーム展開モジュール２０と、システム分析モジュール２２と、ＯＡＭモジュール２４と、シーケンシャルシステムデザイン２６及びログ２８を保持する。展開モジュール２０、システム分析モジュール２２及びＯＡＭモジュール２４は、システム１０の１つ又はそれ以上の要素によって実行されるソフトウエアその他の適切な制御論理を示す。展開モジュール２０は、シーケンシャルシステムの二進時間フレーム展開を実行するよう動作する。システム分析モジュール２２は、回路及び／又はシステムモジュールを分析するように動作する。例えば、システム分析モジュール２２は、その回路を検査及び確認するために、展開モジュール２０によって生成された時間フレーム展開された論理回路についての分析を実行する。ＯＡＭモジュール２４は、システム１０内の要素の動作、管理及び監督を支援する。例えば、ＯＡＭモジュール２４は、プロセッサ１６により実行されるコードを含み、それは、適切な時間に、ディスプレイ１２及び入力１４を通じたユーザとのインターフェースを制御し、展開モジュール２０及びシステム分析モジュール２２を実行させる。
【００１３】
シーケンシャルシステムデザイン２６は、多数のシーケンシャル論理システム及び回路をモデル化するデータを包含する。この説明で使用されるように、シーケンシャルシステム、シーケンシャル論理、シーケンシャル論理回路及びシーケンシャル回路なる用語は、総て、入力及び状態情報に基づく出力の生成を与える、任意の適切なシステム、回路若しくは論理設計、又はこれらのモデルを示す。例えば、シーケンシャルシステムは、多数の組み合わせ論理装置及び１つ又はそれ以上のレジスタ、ラッチ、又は状態情報を出力の計算に導く他のメモリ要素を包含する半導体デザインであり得る。シーケンシャルシステムデザイン２６は、シーケンシャルシステムを形成する要素のモデル化を可能にする情報を包含する。シーケンシャルシステムデザイン２６の特定の１つを利用して、システム１０は、回路内の状態についての回路設定値、及び回路への入力についての値の挙動を決定することが可能である。
【００１４】
ログ２８は、パフォーマンス、及びシステム１０の動作結果を記述する情報を包含する。例えば、ログ２８は、二進時間フレーム展開されたシーケンシャルシステムの分析の際に、システム分析モジュール２２の動作を詳述するパフォーマンス統計を包含し得る。ログ２８は、更に、回路を検査及び確認するために区別される入力のような、この分析の結果を包含し得る。しかしながら、特定の実施例ではメモリ１８に維持される特定の情報を記述するが、システム１０は、任意の適切な形式で維持される任意の適切なデータを利用して、特性及び機能を実現することを想定することが可能である。
【００１５】
図２は、１つの時間フレームの間のシーケンシャル回路の動作を示すブロック図である。この図では、シーケンシャル回路は、所与の入力Ｉ０及び現在の状態Ｙ０に対して関数ｆを実行し、出力Ｏ０を生成する。この動作の結果として、シーケンシャル回路の状態は、新たな状態Ｙ１に変化する。そして、次の時間フレームの間に、このシーケンシャル回路は、その時間フレームの間に受信した入力及び所与の状態Ｙ１に基づいて、ｆを実行する。なお、シーケンシャル回路の入力及び出力として図示されているが、状態情報（Ｙ０及びＹ１）は、回路内のレジスタ、ラッチ、その他の適切な要素を利用して内部的に維持され得る。すなわち、このブロック図は、シーケンシャル回路の１つの時間フレームについての動作を単に図示するに過ぎない。
【００１６】
任意の特定の時間フレームにおけるシーケンシャルシステムの動作は、ｆｔ（数式１）として書き表すことが可能であり、ｔについての値は特定の時間フレームを示す。例えば、１に等しいｔは、１クロックサイクルにおけるシーケンシャル回路を示すので、ｆ１は、第１の時間フレームにおけるシーケンス回路の動作を示す。ｔが［ｔｎ−１．．．ｔｉ．．．ｔ０］によって表現されるｎビット数であるならば、ｔは、
【００１７】
【数１】
2004046821.tif 000003
として表現され得る。数式１及び数式２を組み合わせることで、ｆｔは、
【００１８】
【数２】
2004046821.tif 000004
として表現されることが可能であり、ここで、クロス演算子（×）は、ｆｍ＋ｎ＝ｆｍ×ｆｎとして定義される。ｔｉは二進数を示すので、ｔｉについての値は１又は０であり、数式３における各クローズ（ｃｌａｕｓｅ）についての値は、
【００１９】
【数３】
2004046821.tif 000005
として表現され得る。
【００２０】
図３は、数式４の回路モデルを記述するブロック図であり、それは、初期状態と、シーケンシャル回路の２ｉ個の同一物又はコピー（ｃｏｐｙ）の系列から生じる状態との間で、ｔｉの値に基づいて、選択を行うマルチプレクサを含む。４４によって示される、この二進時間フレーム展開されたクローズは、特定の時間フレームの間に、入力及び変数としてのｔｉについての値を利用して、シーケンシャル回路の動作をモデル化する。クローズ４４の中で、シーケンシャル回路の同一物の各々は、受信した入力及び状態情報に基づいて出力を生成する。
【００２１】
シーケンシャル回路の最初の同一物は、クローズ４４の受信した状態情報と、最初の時間フレームに受信した入力とを利用して、第１時間フレームについての出力を生成するよう動作する。更に、シーケンシャル回路の第１の同一物は、その処理によって生じる状態情報を、シーケンシャル回路の第２の同一物に与える。シーケンシャル回路の第２の同一物は、第１の同一物から受信した状態情報と、動作中の第２時間フレームの間の入力とを利用して、第２時間フレームの間の出力を反映する出力を生成する。シーケンシャル回路の同一物の系列は、マルチプレクサ４６に状態情報を与える最後の同一物に至るまで同様の形式でそれぞれ動作する。
【００２２】
ｔｉについての値に基づいて、マルチプレクサ４６は、シーケンシャル回路の最終段の同一物により生成された状態情報と、クローズ４４により受信された状態情報との間で選択を行う。動作時にあっては、ｔｉがゼロに等しいならば、クローズ４４は状態情報を迂回して通過し、ｔｉが１に等しいならば、クローズ４４は、シーケンシャル回路の同一物の系列によって生成された状態情報を提供する。ｔの間の各ビットについての複数のクローズをカスケード接続することで、システム１０は、シーケンシャル回路の完全な、二進時間フレーム展開されたモデルを形成することができる。したがって、数式４、数式３についてのこの所与のモデルは、ｔ内で使用される各２進数についての時間フレームクローズの系列としてモデル化される。
【００２３】
図４は、時間フレームｔがｎビット数として表現される場合の、全時間フレームについての数式３のモデル５０を示すブロック図である。例えば、８ビットのｔが与えられる場合に、モデル５０は、８つの時間フレームクローズを包含し、２５５時間フレームまでに対して、シーケンシャル回路の動作をモデル化するよう動作する。この図ではその数式に関する最初の２つの時間フレームクローズ及び最後の時間フレームクローズが図示されている。カスケード接続された時間フレームクローズの系列は、ｎビットｔにより表現される最大値より小さい又は等しい総ての時間フレームについて、シーケンシャル回路の挙動のモデル化を可能にする。これは、従来の手法で使用されている線形サーチ（ｌｉｎｅａｒ　ｓｅａｒｃｈ）とは対照的に、時間フレームにわたるバイナリサーチ（ｂｉｎａｒｙ
ｓｅａｒｃｈ）を可能にする。
【００２４】
このモデルの利点を説明するために、カウンタの初期値としてゼロが与えられ、８ビットカウンタの最上位ビットを１に設定するために必要な多数の時間フレームを見出す問題を想定する。従来の手法を利用すると、回路の挙動は、検査される各フレームについて別々にモデル化される必要がある。従って、最初の時間フレームと供に始まると、従来の手法は、問題に対する解を得るまでに、１２８のモデルを検査するであろう。これに対して、二進時間フレーム展開を利用すると、論理分析は、単一のステップにて単独のモデルと供に、８つのゼロビットを有するｔの総ての値に対して、その問題は実行不可能である（即ち、それは解を有しない。）ことを見出すことが可能である。
【００２５】
シーケンシャル回路の二進時間フレーム展開されたモデルを利用すると、システム分析プログラムは、シーケンシャル回路のシミュレーション、妥当性検証（ｖａｌｉｄａｔｉｏｎ）及び確認を行うことが可能である。例えば、状態判定は、シーケンシャル回路の検査及び確認における基本的な問題である。状態判定問題の１つの形式では、論理分析は、初期値から所望の状態にシーケンシャル回路の状態を遷移させる入力ベクトルのシーケンスを判定する必要がある。状態判定問題の他の形式は、特定の状態が、あるクロックサイクル数又は時間フレーム数内の到達可能であるか否かを判定しようとするものである。分析の他の形式は、一組の所与の出力になる入力を判定しようとするものである。
【００２６】
これら多くのプロセスでは、問題が解決可能であるか否か、及び可能である場合には、出力又は状態のような所望の状況になる入力ベクトルを判別する。例えば、特定の出力が与えられる場合に、シーケンシャル回路の分析は、一連の時間フレームにわたる特定の入力を利用して、その出力に到達することが可能であることを判定する。シーケンシャル回路の動作は状態によって駆動されるので、シーケンシャル回路の様々な形式の回路分析の中で、時間は共通するテーマ（ｔｈｅｍｅ）である。開示される手法を利用して生成される、二進時間フレーム展開されたモデルは、期間にわたるバイナリサーチを可能にする。これは、パフォーマンスを顕著に増加させ、システム分析に必要な時間を減少させる。
【００２７】
図５は、６０にて示される、８つの時間フレームにわたるシーケンシャル回路の動作をモデル化する、二進時間フレーム展開されたモデルを示すブロック図である。最初の８つの時間フレーム（０−７）をモデル化するには、ｔについて少なくとも３ビットの二進値を必要とする。回路モデルは、３つの二進時間フレーム展開されたクローズを含む。これら３つの時間フレームクローズの各々は、クローズ４４におけるモデル化のように数式４に従ってモデル化される。
【００２８】
第１クローズは、シーケンシャル回路６２の単独の段階及びマルチプレクサ６４を含む。回路６２は、第１クローズにより受信される初期状態に基づいて、入力を処理し、出力及びその結果生じる状態を生成する。マルチプレクサ６４は、二進数ｔ０に対する値に基づいて、初期状態及びその結果生じる状態の間で選択を行う。マルチプレクサ６４は、ｔ０に対する値に基づいて、第１クローズにより受信された初期状態と第１クローズにおけるシーケンシャル回路の単独の段階の動作から生じる状態との間で選択を行う。マルチプレクサ６４は、選択した状態を初期状態情報として第２時間フレームクローズに与える。
【００２９】
回路モデルの第２クローズは、６６及び６８で示される一連のシーケンシャル回路の２つの同一物と、マルチプレクサ７０とを有する。回路６６は、マルチプレクサ６４から受信した状態情報に基づいて、第２時間フレームの動作中に入力を処理し、出力を生成する。また、回路６６は状態情報を生成し、この状態情報を回路６８に伝達する。回路６８は、回路６６から受信した状態情報に基づいて、第３時間フレームの動作中に入力を処理し、出力を生成する。また、回路６８は、状態情報を生成し、この状態情報をマルチプレクサ７０に伝達する。マルチプレクサ７０は、ｔ１に対する値に基づいて、第２クローズの受信した初期状態と、第２クローズ内の一連のシーケンシャル回路の動作の結果生じる状態との間で選択を行う。ｔ１がゼロに等しいならば、マルチプレクサは、マルチプレクサ６４から与えられた状態情報を選択する。ｔ１が１に等しいならば、マルチプレクサは、回路６８からの状態情報を選択する。従って、第２時間フレームクローズは、ｔ１の値に依存して、状態情報に関与する又はしない。
【００３０】
第３時間フレームクローズでは、一連の４つのシーケンシャル回路の同一物が、入力に関して動作し、回路間に通知される状態値に基づいて出力を生成する。前述のクローズと同様に、ｔ２に対する値は、一連のシーケンシャル回路から生じる状態と、時間フレームクローズ２から与えられた初期状態との間で選択を行うように、マルチプレクサを制御する。
【００３１】
図示されているように、シーケンシャル回路の二進時間フレーム展開されたモデルは、様々な時間フレームにおける入力に対する値と、ｔについての値の両者を変数として受け取る。このモデルを利用して、システム分析ルーチンは、時間フレームにわたって動作する場合の、シーケンシャル回路の様々なシミュレーション、検証、及び確認を実行することが可能になる。例えば、システム分析は、このモデルを利用して、シーケンシャルシステムの状態判定を実行することができる。モデル６０を利用すると、システム分析ルーチンは、シーケンシャル回路の最初の７つの時間フレームの動作にわたって、様々なシミュレーションを実行することが可能である。同様なモデルを利用して、システム１０は任意の時間フレーム数にわたってシーケンシャル回路をモデル化することが可能である。
【００３２】
図６は、シーケンシャル回路をモデル化し、その結果のモデルを利用してシーケンシャル回路を分析するための方法を示すフローチャートである。システム１０は、ステップ８０にてシーケンシャルシステムを見分ける。例えば、ユーザは、回路設計プログラムを利用してシーケンシャル論理を入力し、又はシーケンシャルシステムデザイン２６内の特定のシーケンシャル回路を特定する。システム１０は、ステップ８２にて分析に対する最大の時間フレームを判定する。例えば、システム１０は、シーケンシャル回路を分析する際の最大時間フレーム数についてのデフォルト値を判別し、又は入力１４を通じてユーザから最大時間フレームを特定する命令を受ける。システム１０は、ステップ８４にてシーケンシャルシステムを二進時間フレームに展開する。例えば、ＯＡＭモジュール２４は、展開モジュール２０を利用して、シーケンシャルシステムを処理し、適切な数の時間フレームクローズを有する二進時間フレーム展開されたモデルを生成し、分析用の最大時間フレームに至るまでに解決する。
【００３３】
システム１０は、ステップ８６においてシーケンシャル回路から所望の出力を指定する。例えば、ユーザ又は他の適切なソースは、シーケンシャル回路を利用して取得するための出力又は状態を指定する。システム１０はその後に二進時間フレーム展開されたモデルを利用して、それらの出力及び／又は状態に至るのに適切な入力及び／又は時間フレームを特定する。それらの入力を決定するために、システム１０は、ステップ８８において入力及び時間を変化させる。例えば、システム１０は、システム分析モジュール２２を利用して、任意の適切な分析アルゴリズムに従って入力及び時間を変化させることで、そのモデルを分析することができる。システム１０は、ステップ９０において問題が解けたか否かを判定する。例えば、システム１０は、試行される入力及び時間が所望の出力になるか否かを判定することができる。もしそうであれば、システム１０は、ステップ９２においてその入力解を表示し、ステップ９６においてログエントリ（ｌｏｇ　ｅｎｔｒｙ）を生成する。例えば、システム１０は、所望の出力を得るための特定の入力を指定する分析報告を作成する。例えば、これは、シーケンシャルシステム設計により製造された実際の回路の試験に使用するテスト・ベクトルを与えることが可能である。
【００３４】
シーケンシャル回路の分析は、ステップ９０にて問題が解けるまで、又は分析がステップ９４にて時間切れになるまで続けられる。一実施例によれば、コンフィギュレーション及び／又はユーザ設定は、システム分析モジュール２２が所与の問題を解決するであろう期間を指定する。システム分析モジュール２２が所与のその期間に問題を解くとができなかったならば、時間切れになり、その問題のパラメータ、分析の実効性（パフォーマンス）、及び／又は他の適切な情報を指定する報告がログ２８にて作成される。
【００３５】
しかしながら、上述したフローチャート及び付随する説明は、動作例を示すに過ぎず、システム１０は、シーケンシャル回路の二進時間フレーム展開されたモデルを生成し、その生成されたモデルを利用してシーケンシャル回路を分析する任意の適切な手法を利用して構築することが可能である。従って、フローチャートにおける多くのステップは、同時に及び／又は図示されているものとは異なる順序で実行され得る。更に、システム１０は、本方法が適切に実行される限りにおいて、更なるステップ、より少ないステップ、及び／又は異なるステップを有する方法を利用することができる。
【００３６】
本発明はいくつかの実施例にて説明されてきたが、当業者には多数の変更及び修正が示唆されており、本発明はそのような変更及び修正を本発明の範疇に包含することを意図する。
【００３７】
以下、本発明の教示する手段を列挙する。
【００３８】
（付記１）　シーケンシャルシステムを分析する方法であって：
シーケンシャルシステムの分析のための最大時間フレームを決定するステップであって、前記最大時間フレームがｎビット二進値を利用して表現することが可能であるところのステップ；
前記シーケンシャルシステムの二進時間フレーム展開されたモデルを作成するステップであって、前記二進時間フレーム展開されたモデルが、カスケード接続されたｎ個の二進時間フレームクローズを有するところのステップ；
前記二進時間フレーム展開されたモデルを利用して前記シーケンシャルシステムを分析するステップ；及び
分析報告を作成するステップ；
を有することを特徴とする方法。
【００３９】
（付記２）　クローズの各々が、ゼロに等しいｐ値を有するクローズの先頭からカウントされる相対的な位置ｐを有し；及び
前記クローズの各々が、前記シーケンシャルシステムの一連の２ｐ個の同一物より成ることを特徴とする付記１記載の方法。
【００４０】
（付記３）　前記クローズの各々が：
初期状態及び２ｐ個の入力一式を受信し；及び
前記初期状態及び２ｐ個の入力一式を利用して、結果の状態及び２ｐ個の出力一式を生成することを特徴とする付記２記載の方法。
【００４１】
（付記４）　前記クローズの各々について：
前記シーケンシャルシステムの第１の同一物が、前記入力一式の第１のもの及び初期状態を受信し、出力一式の第１のもの及び状態を生成し；及び
前記シーケンシャルシステムの後続の各同一物が、その系列におけるシーケンシャルシステムの同一物の先行するものから入力一式の後続のもの及び状態を受信し、出力一式の後続のもの及び状態を生成することを特徴とする付記３記載の方法。
【００４２】
（付記５）　前記クローズの各々が初期状態を受信し、結果の状態を生成し、該結果の状態は、初期状態及びシーケンシャルシステムの一連の同一物から生成された状態の間で選択されることを特徴とする付記２記載の方法。
【００４３】
（付記６）　更に、各クローズに対して、初期状態と、分析中の時間フレームの二進標記におけるｐ番目の数値に基づいて、シーケンシャルシステムの一連の同一物から生成された状態との間で選択が行われることを特徴とする付記５記載の方法。
【００４４】
（付記７）　更に、各クローズに対して：
前記二進標記におけるｐ番目の数がゼロの値を有するならば、初期状態を選択し；及び
前記二進標記におけるｐ番目の数が１の値を有するならば、前記シーケンシャルシステムの一連の同一物から生成された状態を選択することを特徴とする付記６記載の方法。
【００４５】
（付記８）　前記シーケンシャルシステムを分析するステップが：
前記シーケンシャルシステムについての所望の状態を特定するステップ；及び前記所望の状態になる入力ベクトルを特定するために前記二進時間フレーム展開されたモデルを分析するステップ；
より成ることを特徴とする付記１記載の方法
（付記９）　分析報告を作成するステップが：
前記分析が前記所望の状態を与える入力ベクトルを見出したか否かを判定するステップ；
前記分析が前記入力ベクトルを見出したならば、前記分析報告にて前記入力ベクトルを特定するステップ；及び
前記分析が前記入力ベクトルを見出さなかったならば、前記分析報告にて前記所望の状態は実行不可能な問題であることを示すステップ；
より成ることを特徴とする付記８記載の方法。
【００４６】
（付記１０）　前記シーケンシャルシステムが、複数の論理要素及び少なくとも１つのメモリ要素を揺する半導体装置より成り、前記メモリ要素が前記論理要素の少なくとも１つによって使用される状態情報を保持することを特徴とする付記１記載の方法。
【００４７】
（付記１１）　媒体中で具現化され、実行時に動作することの可能な、シーケンシャルシステムを分析するためのソフトウエアであって：
シーケンシャルシステムの分析のための最大時間フレームを決定するステップであって、前記最大時間フレームがｎビット二進値を利用して表現することが可能であるところのステップ；
前記シーケンシャルシステムの二進時間フレーム展開されたモデルを作成するステップであって、前記二進時間フレーム展開されたモデルが、カスケード接続されたｎ個の二進時間フレームクローズを有するところのステップ；
前記二進時間フレーム展開されたモデルを利用して前記シーケンシャルシステムを分析するステップ；及び
分析報告を作成するステップ；
を実行させることを特徴とするソフトウエア。
【００４８】
（付記１２）　クローズの各々が、ゼロに等しいｐ値を有するクローズの先頭からカウントされる相対的な位置ｐを有し；及び
前記クローズの各々が、前記シーケンシャルシステムの一連の２ｐ個の同一物より成ることを特徴とする付記１１記載のソフトウエア。
【００４９】
（付記１３）　前記クローズの各々が：
初期状態及び２ｐ個の入力一式を受信し；及び
前記初期状態及び２ｐ個の入力一式を利用して、結果の状態及び２ｐ個の出力一式を生成することを特徴とする付記１２記載のソフトウエア。
【００５０】
（付記１４）　前記クローズの各々について：
前記シーケンシャルシステムの第１の同一物が、前記入力一式の第１のもの及び初期状態を受信し、出力一式の第１のもの及び状態を生成し；及び
前記シーケンシャルシステムの後続の各同一物が、その系列におけるシーケンシャルシステムの同一物の先行するものから入力一式の後続のもの及び状態を受信し、出力一式の後続のもの及び状態を生成することを特徴とする付記１３記載のソフトウエア。
【００５１】
（付記１５）　前記クローズの各々が初期状態を受信し、結果の状態を生成し、該結果の状態は、初期状態及びシーケンシャルシステムの一連の同一物から生成された状態の間で選択されることを特徴とする付記１２記載のソフトウエア。
【００５２】
（付記１６）　更に、各クローズに対して、初期状態と、分析中の時間フレームの二進標記におけるｐ番目の数値に基づいて、シーケンシャルシステムの一連の同一物から生成された状態との間で選択が行われることを特徴とする付記１５記載のソフトウエア。
【００５３】
（付記１７）　更に、各クローズに対して：
前記二進標記におけるｐ番目の数がゼロの値を有するならば、初期状態を選択し；及び
前記二進標記におけるｐ番目の数が１の値を有するならば、前記シーケンシャルシステムの一連の同一物から生成された状態を選択することを特徴とする付記１６記載のソフトウエア。
【００５４】
（付記１８）　前記シーケンシャルシステムを分析するステップが：
前記シーケンシャルシステムについての所望の状態を特定するステップ；及び前記所望の状態になる入力ベクトルを特定するために前記二進時間フレーム展開されたモデルを分析するステップ；
より成ることを特徴とする付記１１記載のソフトウエア
（付記１９）　分析報告を作成するステップが：
前記分析が前記所望の状態を与える入力ベクトルを見出したか否かを判定するステップ；
前記分析が前記入力ベクトルを見出したならば、前記分析報告にて前記入力ベクトルを特定するステップ；及び
前記分析が前記入力ベクトルを見出さなかったならば、前記分析報告にて前記所望の状態は実行不可能な問題であることを示すステップ；
より成ることを特徴とする付記１８記載のソフトウエア。
【００５５】
（付記２０）　シーケンシャルシステムの二進時間フレーム展開されたモデルであって：
連続的に接続された複数の二進時間フレームクローズであって、該クローズの各々が、ゼロに等しいｐ値を有するクローズの先頭からカウントされる、その系列における相対的な位置ｐを有し、前記クローズの各々がシーケンシャルシステムの一連の２ｐ個の同一物及びマルチプレクサより成るところの複数の二進時間フレームクローズ；
を有し、前記クローズの各々において、前記同一物の各々が入力一式及び入力状態情報を受信し、出力一式及び出力状態情報を作成し、前記系列の第１の同一物が、前記クローズに対する初期状態情報を、前記第１の同一物に対する入力状態情報として受信し、前記系列における他の同一物が、前記系列における先行する同一物のものからの出力状態情報を、前記他の同一物に対する入力状態情報として受信し、前記系列における最終的な同一物が、前記最終的な同一物から前記マルチプレクサに出力状態情報を与え；及び
前記最終的な同一物からの出力状態情報及び前記クローズについての前記初期状態情報の間で選択を行うための分析の下に、前記クローズの各々が、前記クローズについての前記初期状態情報を受信し、前記クローズについての初期状態情報を前記マルチプレクサに与え、時間フレームの二進標記におけるｐ番目の数値に基づいて前記マルチプレクサを制御し、及び選択された状態情報を前記マルチプレクサから次のクローズに与えることを特徴とする二進時間フレーム展開されたモデル。
【００５６】
【図面の簡単な説明】
【図１】図１は、本発明の様々な実施例によるシーケンシャルシステムの二進時間フレーム展開を実行するための処理システム図を示す。
【図２】図２は、単独の時間フレームの間のシーケンシャルシステムの動作を示すブロック図である。
【図３】図３は、二進時間フレーム展開の間に処理システムによって生成された、一般的な、二進時間フレーム展開されたクローズを示すブロック図である。
【図４】図４は、期間にわたってシーケンシャルシステムの分析を可能にするための、互いに連結された一般的なクローズの系列を示すブロック図である。
【図５】図５は、時間フレームゼロから７までにわたる動作の分析を可能にするための、時間フレーム展開されたシーケンシャルシステムの具体例を示すブロック図である。
【図６】図６は、シーケンシャルシステムを展開し、その結果生じる二進時間フレーム展開されたモデルを分析するための方法を示すフローチャートである。
【符号の説明】
１０　処理システム
１２　ディスプレイ
１４　入力
１６　プロセッサ
１８　メモリ
２０　二進時間展開処理モジュール
２２　システム分析モジュール
２４　ＯＡＭモジュール
２６　シーケンシャルシステムデザイン
２８　ログ
４４　クローズ
４６　マルチプレクサ
５０　モデル
６０　モデル
６２，６６，６８　シーケンシャル回路
６４，７０　マルチプレクサ
【図１】
2004046821.tif 000006
【図２】
2004046821.tif 000007
【図３】
2004046821.tif 000008
【図４】
2004046821.tif 000009
【図５】
2004046821.tif 000010
【図６】
2004046821.tif 000011