講演名 1996/12/13
高階述語論理によるハードウェアの構造の形式的検証
鈴木 一哉, 吉田 たけお, 三浦 幸也,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 本稿では設計されたハードウェアの構造がその動作仕様を満たしているかどうかを検証する方法を提案する.従来の検証法で用いられている一階述語論理は再帰的な表現ができないため,順序回路を含むようなハードウェアを表現できない.本稿では高階述語論理を用いることによってこの問題を解決する.本稿ではまず仕様である動作記述およびその設計である構造記述をそれぞれ高階述語論理式に変換する方法を示す.仕様記述および設計記述を表す論理式から"設計が仕様を満たしている"という意味を表す論理式を作り,この論理式を証明することによって検証を行なう.さらに本稿ではこの論理式を定理証明系を用いて証明する際の手順も示す.
抄録(英) We propose a method for verifying a correctness of hardware structure. Hardware including structural loops cannot be expressed by first order predicate logic which is used generally, because first order predicate logic cannot express functions recursively. This problem can be solved by using higher order predicate logic. In this method, two models that are formulas of higher order predicate logic are made from both specification description and design description. From these formulas, we make a correctness formulas which means that the design description satisfies with specification description. We show procedure for proving the correctness formulas using a theorem prover.
キーワード(和) 高階述語論理 / 形式的検証 / 動作記述 / 構造記述
キーワード(英) higher order predicate logic / formal verification / behavioral description / structural description
資料番号 VLD96-70,CPSY96-82
発行日

研究会情報
研究会 VLD
開催期間 1996/12/13(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 VLSI Design Technologies (VLD)
本文の言語 JPN
タイトル(和) 高階述語論理によるハードウェアの構造の形式的検証
サブタイトル(和)
タイトル(英) Formal Verification for Hardware Structure by Higher Order Predicate Logic
サブタイトル(和)
キーワード(1)(和/英) 高階述語論理 / higher order predicate logic
キーワード(2)(和/英) 形式的検証 / formal verification
キーワード(3)(和/英) 動作記述 / behavioral description
キーワード(4)(和/英) 構造記述 / structural description
第 1 著者 氏名(和/英) 鈴木 一哉 / Kazuya SUZUKI
第 1 著者 所属(和/英) 東京都立大学工学部
Faculty of Engineering,Tokyo Metropolitan University
第 2 著者 氏名(和/英) 吉田 たけお / Takeo YOSHIDA
第 2 著者 所属(和/英) 東京都立大学工学部
Faculty of Engineering,Tokyo Metropolitan University
第 3 著者 氏名(和/英) 三浦 幸也 / Yukiya MIURA
第 3 著者 所属(和/英) 東京都立大学工学部
Faculty of Engineering,Tokyo Metropolitan University
発表年月日 1996/12/13
資料番号 VLD96-70,CPSY96-82
巻番号(vol) vol.96
号番号(no) 425
ページ範囲 pp.-
ページ数 8
発行日