特許

J-GLOBAL ID：200903076203223694

論理装置の検証方法、論理装置の検証装置、及び記録媒体

発明者： 岩下 洋哲 ,  中田 恒夫
出願人/特許権者： 富士通株式会社
代理人 (1件)： 今村 辰夫 (外1名)
公報種別：公開公報
出願番号（国際出願番号）：特願平10-001364
公開番号（公開出願番号）：特開平10-301963
出願日： 1998年01月07日
公開日（公表日）： 1998年11月13日
要約：

【要約】【課題】本発明は論理装置の検証方法、論理装置の検証装置、及び記録媒体に関し、記号モデル検査手法において状態集合分割手法を用いることができるようにして、記憶容量削減を可能とし、複雑な論理装置の検証もできるようにする。【解決手段】同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証する検証装置において、有限状態機械M、Mの状態の部分集合q、及びqの部分集合pが与えられたとき、状態集合pから開始して、M上の像計算およびqとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、p内のある状態から出発し、永遠にqから外に出ない状態遷移のパスが存在するかを判定するように構成する。

請求項（抜粋）：

同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証する論理装置の検証方法において、有限状態機械M、Mの状態の部分集合q、及びqの部分集合pが与えられたとき、状態集合pから開始して、M上の像計算およびqとの集合積の計算を繰り返し、その計算過程の状態集合の関係を調べることで、p内のある状態から出発し、永遠にqから外に出ない状態遷移のパスが存在するかを判定することを特徴とした論理装置の検証方法。