特許

J-GLOBAL ID：200903070267122192

論理設計検証装置

発明者： 伊藤 雅樹 ,  高嶺 美夫
出願人/特許権者： 株式会社日立製作所
代理人 (1件)： 作田 康夫
公報種別：公開公報
出願番号（国際出願番号）：特願平11-115985
公開番号（公開出願番号）：特開2000-305974
出願日： 1999年04月23日
公開日（公表日）： 2000年11月02日
要約：

【要約】【課題】従来の計算木論理に基づく形式的論理設計検証装置では、一台の中央処理装置のみで計算が行われるため、記憶量および計算時間の制約から検証可能な検証対象設計論理の規模が制限されていた。【解決手段】計算木論理に基づく形式的論理設計検証装置の計算の中で、最も計算時間と記憶量を必要とする状態遷移関数と像関数の計算を、複数の中央処理装置とそれに付随する記憶装置に分散して計算する。

請求項（抜粋）：

複数の中央処理装置と各中央処理装置に局所的に利用される記憶装置を持つ分散記憶型並列計算機で実現される形式的論理設計検証装置であり、検証対象記述を読み込み、その状態遷移関数を抽出し、論理関数にて表現・保持する状態遷移関数抽出部と、仕様記述を読み込み、その構造を解析し、仕様構造を保持する仕様構造解析部と、検証対象が仕様を満たしているか否かを判定する証明部と、証明部からの依頼を受け、前記状態遷移関数を用いて、複数の中央処理装置およびその局所的記憶装置に分散して像計算を行う像計算部とを具備することを特徴とする論理設計検証装置。

FI (2件)：

G06F 15/60 664 Z ,  G06F 15/60 664 L

Fターム (4件)：

5B046AA08 ,  5B046BA03 ,  5B046CA03 ,  5B046JA01