時相理論を用いた形式的論理設計検証に関する研究

基于时态理论的形式逻辑设计验证研究

• 批准号: 07680374
• 负责人: 平石 裕実
• 金额: $ 1.6万
• 依托单位: Kyoto Sangyo University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-07680374/
• 关键词: 形式的検証; 設計検証; 論理設計; 時相論理; 記号モデル検査; 順序機械

本年度は、主として時空間様相論理と並列検証アルゴリズムの基礎的研究を行なった。1.時空間様相論理の基礎的研究: 同一の回路を一次元的に繰り返し接続するビットスライス的な回路の設計検証において、回路の動作を、時間方向と空間方向の2つの遷移関係を持つ時空間Kripke構造としてモデル化する方法を提案した。これにより、任意長のビット幅を持つビットスライスALU回路などをコンパクトにモデル化出来る。また、この時空間Kripke構造に対する仕様記述のために、時間方向と空間方向の変化を記述できる時空間様相理論体系を示した。そらに、検証アルゴリズムとして、時空間様相論理の記号モデル検査アルゴリズムを示し、実際に簡単なALUの設計検証に適用し、本検証手法が有効であることを示した。2.並列検証アルゴリズムの基礎的研究: 現在、CPUの個数が数個から十数個程度の高性能ワークステーションが比較的安価に入手可能となってきている。そこで、このようなワークステーション上での実行に適した並列検証アルゴリズムの研究を行なった。とくに、設計検証で用いる記号モデル検査アルゴリズムの中心的な役割を担う共有二分決定グラフ(BDD)による論理関数処理の並列化を行なうために、BDD演算のマルチレッドアルゴリズムを開発した。このマルチスレッドアルゴリズムでは、並列処理の正当性を確保するために、内部の節点テーブルや演算結果テーブルのアクセスの際にロックをかける必要があるが、ロックの方法やロックをかける範囲が効率に大きな影響を及ぼすことが判明し、今後引続き研究を進める必要がある。

This year, the basic research of spatial phase logic and parallel detection is carried out. 1. A study on the basis of time-space phase logic: the design and verification of the same loop, the movement of the loop, the time direction and the spatial direction, the migration relationship between the time-space Kripke structure and the transformation method of the loop. The length of the ALU loop is determined by the length of the loop. A description of the temporal and spatial Kripke structure is presented. The design of ALU is applicable to the test method. 2. The basic research of parallel test system: the number of CPU is several, the number of CPU is more than ten, the performance of CPU is more than ten, and the security of CPU is more than ten. A study on the implementation of the system of evaluation and evaluation was carried out. In addition, the design of the system is based on the design of the system, and the design of the system. To ensure the legitimacy of parallel processing, internal nodes should be used to calculate the results of parallel processing. To determine the impact of parallel processing on the efficiency of parallel processing, it is necessary to make further research.

项目成果

H. Hiraishi: "Towards Verification of Bit-Slice Circuits- Time-Space Model Model Checking Approach-" IEICE Trans. Information and Systems. E78-D(7). 791-795 (1995)

H. Hiraishi：“走向位片电路的验证——时空模型模型检查方法——”IEICE Trans。

S. V. Campos: "Temporal Verification of Real-Time Systems" IEICE Trans. Information and Systems. E78-D(7). 796-801 (1995)

S. V. Campos：“实时系统的时间验证”IEICE Trans。

H. Hiraishi: "Time-Space Modal Logic for Verification of Bit-Slice Circuits" Proc. 4th Computer-Aided Design and Computer Graphics. 675-680 (1995)

H. Hiraishi：“用于验证位片电路的时空模态逻辑”Proc。