等式論理による機能レベル設計の形式的検証に関する研究

基于方程逻辑的功能级设计形式化验证研究

• 批准号: 08780268
• 负责人: 濱口 清治
• 金额: $ 0.64万
• 依托单位: Osaka University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-08780268/
• 关键词: 形式的設計検証; 第一階述語論理; 等式論理; 機能レベル設計; 時相論理

集積回路技術の発達にともなって、より大規模の回路設計が行われるようになってきており、このため、設計の正しさを保証することが困難となってきている。設計検証のための技術としては、シミュレーションが広く利用されてきているが、より網羅的かつ厳密な手法として、設計工程のいくつかの場面では、形式的検証技術の利用が進んでいる。現在、実用が進んでいる形式的設計検証の技術は論理回路設計を扱っているが、より大規模な回路を扱うためには、より抽象度の高い、機能レベルの記述を直接扱う必要性がある。本研究では、算術演算などを論理回路レベルで扱わず、記号のまま直接取り扱うために、等号付第一階述語論理を取り上げて、論理回路より上位の機能レベルで記述された設計に対する設計検証手法について研究を行った。機能レベル設計の設計検証問題は、この論理体系における恒真性判定問題に帰着することができるが、一般の等号付第一階述語論理を設計検証に用いた場合、恒真性判定問題が決定不能となるため、検証工程を自動化することができない。しかし、限量子を含まない論理式のみを考えた場合には決定可能となる。具体的に、本研究では、二分決定グラフによる論理関数処理を用いた恒真性判定アルゴリズムを考案したほか、限量子のない等号付第一階述語論理に、時間に関する性質を表現するための時相演算子を加えた論理体系をとりあげ、まず、恒真性判定問題の決定可能性を証明し、次に、これに基づいて効率的な恒真性判定アルゴリズムを構築・実装して、機能レベル設計の検証に有効であることを示した。

Integrated circuit technology development, large-scale circuit design and implementation, design and integrity, this is difficult. Design certification technology and application of design engineering certification technology At present, it is necessary to use advanced design methods to prove the technical and logical circuit design, large-scale circuit design, high abstraction, and direct description of functions. In this study, arithmetic calculation, logic circuit, symbol, direct selection, equal sign, first-order predicate logic, logic circuit, upper function, description, design and verification method were studied. The design verification problem of function design is the logical system of constant truth determination problem. The first order predicate logic is used in design verification. The constant truth determination problem is used in automation of verification engineering. A logical expression is used to determine the probability of a failure. In this study, the logical relationship processing of binary decision is used to prove the possibility of decision of constant truth judgment problem. This is the basis for determining the validity of the design, construction, implementation and functional design.

项目成果

S.Tani et al.: "The Complexity of the Optimal Variable Ordering Problems of a Shared Binary Decision Diagram" IEICE Trans. on Information and Systems. D79-D・4. 271-281 (1996)

S.Tani 等人：“共享二元决策图的最优变量排序问题的复杂性”IEICE Trans on 信息和系统。271-281 (1996)

E.M.Clarke et al.: "Another Look at LTL Model Checking" Formal Methods in System Design. 10・1(掲載予定). (1997)

E.M.Clarke 等人：“LTL 模型检查的另一种看法”系统设计中的形式方法 10・1（即将出版）。