ハイブリッドモデル状態マシーンにおける到達可能状態を決定するための方法及び装置

発明者： ,
出願人/特許権者：
代理人 (1件)：岡部正夫 (外2名)
公報種別：公開公報
出願番号（国際出願番号）：特願平7-138355
公開番号（公開出願番号）：特開平7-334551
出願日： 1995年06月06日
公開日（公表日）： 1995年12月22日
要約：

【要約】【目的】シーケンシャルデジタルシステムの高級仕様、特にハイブリッドモデルにより表現される高級仕様をより効率的に妥当化する方法と装置を提供する。【構成】システムの高級表現は、直接和EFSMに変換される。操作者あるいはデータファイルが、状態と変数値の初期構成、あるいは初期構成の集合を提供する。この方法は、直接和EFSMのシンボル実行を通して、初期構成から到達可能な構成の集合を決定する。マシーンの遷移関係をブール表現と算術表現のAND積として表現することにより、表現の各クラスが別々に処理される。完了時に、シンボル実行は、到達可能な状態の集合のカバーを作成する。その結果は、ある仕様が予期せぬあるいは互換性のない結果を生じたかどうかを判定するために見直される。

請求項（抜粋）：

シーケンシャル回路の設計の高級仕様を妥当化する方法であって、前記高級仕様は整数変数とブール変数の両方を含み、a)前記高級仕様から拡張された有限の状態マシーンを生成することと、ここで、前記各緒された有限の状態マシーンは1以上の出力端部に接続された少なくとも1つの状態を具備し、前記各出力端部は前記少なくとも1つの状態のうちの1つで終端し、b)前記拡張された有限の状態マシーンを直接和マシーンに変換することと、c)前記直接和マシーンの導かれたグラフを生成することと、ここで、前記導かれたグラフは少なくとも1つの端部により接続された複数の頂点を具備し、d)初期構成を得ることと、e)前記初期構成を用いて前記導かれた和マシーンのシンボル実行を行うことと、ここで、前記シンボル実行は前記初期構成から到達可能な構成の集合を提供し、及びf)到達可能な構成の集合を、前記到達可能な構成の集合を人間に通信するための手段に提供することとを具備する方法。

前のページに戻る