形式的検証手法を利用したデジタルシステムの設計デバッグ技術に関する研究

2002 年度 実績報告書

• 研究課題/領域番号: 14350178
• 研究機関: 東京大学
• 研究代表者: 藤田 昌宏 東京大学, 大学院・工学系研究科, 教授 (70323524)
• 研究分担者: 小松 聡 東京大学, 大規模集積システム設計教育研究センター, 助手 (90334325)
• キーワード: システムLSI / デバッグ / 形式的検証

研究概要

集積回路の大規模化、複雑化により設計検証期間がLSI設計工程全体の70〜80%以上を占めるようになっているおり、近年では設計検証技術が設計生産性を決定する重要な要素となっている。また、誤りを修正する「デバッグ工程」を支援する手法やツールにはいまだ実用的なものが無く、それらの技術を確立することで高品質な設計を迅速に行うことが可能になると考えられる。本研究は従来から研究されているレジスタ転送レベル(論理レベル)だけでなく、仕様記述レベルからハードウェア・ソフトウェアが一体となったシステムレベルの設計記述も研究対象としているが、今年度は算術演算回路のデバッグ支援技術に関する研究を重点的に行った。
LSIにおいて算術演算回路、特に乗算回路は多種の回路構成法が存在するため、それらの回路構造が大きく異なるため検証しにくい問題として知られている。また、一般に算術演算回路は遅延や面積が大きくなりがちであり、クリティカルパスを構成する要素となることが多く、設計者は多大な労力をかけて回路最適化を行うため、その回路に設計誤りが発見された際の再設計は設計者の大きな負担となる。本研究では回路修正をできるだけ小さなものにすることでデバッグ工程および設計工程の高速化を支援するデバッグ手法を提案した。本手法は、(1)回路中の設計誤り部分の抽出と(2)誤り部分の正しい回路への置き換え、の2つの部分からなる。前半部では設計誤りを含む回路を全加算器/半加算器のネットワークに対応付け、検証対象範囲を狭めながら誤り部分を抽出する。後半部では、前半部から出力された誤り箇所とその部分に対応する正しい論理をもとに正しい論理回路への置き換えを行う。16ビットのアレイ構造の乗算回路に本手法を適用して実験を行った結果、所望の動作が行えることを確認した。

研究成果

• [文献書誌] Thanyapat Sakunkonchak: "Verification of Synchronization in SpecC Description withthe Use of Difference Decision Diagrams"Proc.of Forum on specification & Design Languages (FDL'02). 2002. (2002)
• [文献書誌] Hiroshi Saito: "An Equivalence Checking Methodology for Hardware Oriented C-based Specifications"Proc.International High Level Design Validation and Test Workshop. 2002. 139-144 (2002)
• [文献書誌] Thanyapat Sakunkonchak: "Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams"Proc.of Formal Techniques for Networked and Distributed Systems (FORTE2002). 2002. 369 (2002)
• [文献書誌] Masao Kubo: "Debug Methodology for Arithmetic Circuits on FPGAs"Proc.of IEEE International Conference on Field-Programmable Technology(FPT-02). 2002. 236-242 (2002)
• [文献書誌] Farzan Fallah: "Coverage Metric for Observability-Based Validation of C Programs"Proc.of Microprocessor Test and Verification (MTV'02). 2002. (2002)
• [文献書誌] Farzan Fallah: "Event-Driven Observability Enhanced Coverage Analysis of C Programs for Functional Validation"Proc.Asia South Pacific Design Automation Conference. 2003. 123-128 (2003)