特許
J-GLOBAL ID：200903011920049645
論理装置の検証方法、検証装置及び記録媒体
発明者：
出願人/特許権者：
代理人 (1件)：
大菅 義之 (外1名)
公報種別：公開公報
出願番号（国際出願番号）：特願平10-358695
公開番号（公開出願番号）：特開2000-181939
出願日： 1998年12月17日
公開日（公表日）： 2000年06月30日
要約：
【要約】【課題】状態数の大きい論理装置を検証装置のメモリ容量や計算時間を適切に調整しながら有効に検証しうる論理装置の検証方法及び装置を提供する。【解決手段】 最初に、論理装置をモデル化した有限状態機械が満たすべきプロパティを表現する遷移系列集合のグラフを作成する。次に、処理すべき節点を該グラフから選択し、その節点に接続している枝の1つを選ぶ。選んだ枝の始点側の節点の状態集合に写像を施し、結果を終点側の節点の状態集合に追加する。そして、写像の結果、目的のプロパティを満たしている状態集合が得られたか否か、すなわち、遷移系列の実例を発見したか否かを判断する。該実例を発見した場合には、遷移系列ありとして処理を終了する。該実例が発見されなかった場合には、当該節点に接続されている未処理の枝があるか否かを判断し、ある場合には上記処理を繰り返す。未処理の枝がない場合は、遷移系列なしとして処理を終了する。
請求項（抜粋）：
(a)検証対象の論理装置をモデル化した有限状態機械が満たすべき目的のプロパティを表す、有限長または無限長の遷移系列の集合を、遷移関係式でラベル付けされた、有向枝グラフに変換し、該有向枝グラフの構成情報を第1のメモリに記憶し、(b)該有向枝グラフ上の各節点に属する状態集合を第2のメモリに記憶し、(c)該有向枝グラフ状の始点側とする節点に属する状態集合を該第2のメモリから読み出し、該第1のメモリに記憶されている有向枝グラフの構成情報を参照して、写像演算を行うべき枝を選択した後、該読み出した状態集合に対して該枝に対応する写像演算を施し、(d)該写像演算の結果を該枝の終点側の節点に属する状態集合に追加して、該第2のメモリに記憶し、(e)ステップ(c)及び(d)を繰り返し実行し、該第2のメモリに記憶された状態集合を基に、該有向枝グラフの示す遷移系列の集合が実際に要素を持つか否かを判定することによって、検証対象の論理装置が目的のプロパティを満たしているか否かを検証する、ことを特徴とする論理装置の検証方法。
Fターム (4件)：
5B046AA08
, 5B046DA01
, 5B046DA06
, 5B046JA01
