大規模論理設計の形式的検証に関する研究

大规模逻辑设计的形式化验证研究

• 批准号: 08680380
• 负责人: 平石 裕実
• 金额: $ 1.41万
• 依托单位: Kyoto Sangyo University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08680380/
• 关键词: 形式的検証; 設計検証; 論理設計; 時相論理; 記号モデル検査; 耐故障設計; セルフテスト; セルフチェック

本年度は、主として時空間様相論理の並列検証アルゴリズムの基礎的研究と、具体的な設計検証問題として耐故障設計の形式的検証を行なった。1.時空間様相論理の並列検証アルゴリズム:時空間様相論理の検証アルゴリズムでは、時間方向と空間方向の逆像計算が中心になる。これらの逆像計算の並列アルゴリズムとして、CPUの個数が数個から十数個程度の高性能ワークステーション上での実行に適したアルゴリズムと、50台程度のワークステーションを高速ネットワークで結合した分散システム上での実行に適したアルゴリズムの基礎的研究を行なった。前者では、マルチスレッドに基づく並列アルゴリズムを種々検討し、後者では、各ワークステーションで共有すべきデータの管理手法を種々検討した。その結果、並列処理の正当性を確保するために、種々の共有データへのアクセスの際にロックをかける必要があるが、ロックの方法やキャッシュの方法が効率に大きな影響を及ぼすことが判明した。今後引続き研究を進める必要があると考えられる。2.耐故障設計の形式的検証:論理回路の耐故障設計では、設計した回路がセルフテスト性やセルフチェック性を持つことが要求される場合が多い。これらの性質は回路内部に故障を仮定した上で満たされるべき性質であり、その検証は煩雑になる。そこで、これらの性質を論理関数で表現し、論理関数処理でこれらの性質の検証を行うアルゴリズムを示し、実際に論理シミュレーションによる検証に比べて数倍高速に検証できることを示した。

This year, we will compare each other in time and space, and list the research papers and specific design questions in the form of fault tolerance design. 1. Time and space phase comparison and listing: time and space phase analysis, time and space direction reverse image calculation center tracking. In addition, the reverse image calculation is used to calculate and list the number of high-performance high-performance customers in more than a dozen levels, such as the reverse image calculation and CPU calculation. There are more than ten levels of high-performance high-performance vehicles, 50 high-speed vehicles, combined with the research bank of the distribution bank, which is the research bank of the local government. Both the former and the latter are listed in the same category as the former, the latter and the other. There is a common agreement on the management practices of the former and the latter. The results are verified, and the results are listed to ensure that the information is properly guaranteed, that the necessary information is available, that the method is effective, and that the accuracy of the method is significant. In the future, it is necessary to conduct a detailed examination of the study. two。 Fault tolerance design in the form of fault design: maintenance loop design, design circuit design, fault tolerance, fault tolerance, fault tolerance There is a fault inside the circuit and there is a fault in the circuit. You need to know that you have a lot of information, you know, you know, you know

项目成果

K.Kawakubo: "Formal Verification of Self-Testing Properties of Combinational Circuits" Proc.5th Asian Test Symposium. 119-122 (1996)

K.Kawakubo：“组合电路自测试特性的形式验证”Proc.5th Asian Test Symposium。