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

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14350178
• Research Institution: The University of Tokyo
• Principal Investigator: 藤田 昌宏 東京大学, 大学院・工学系研究科, 教授 (70323524)
• Co-Investigator(Kenkyū-buntansha): 小松 聡 東京大学, 大規模集積システム設計教育研究センター, 助手 (90334325)
• Keywords: システムLSI / 形式的検証技術 / デバッグ

Research Abstract

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

Research Products

• [Publications] M.Kubo, T.Matsumoto, M.Fujita: "Debug Methodology for Arithmetic Circuits based on Architecture Library Mapping"Proc.of International Workshop on Logic and Synthesis. 73-80 (2003)
• [Publications] 田辺 健, 齋藤 寛, 小松 聡, 藤田 昌宏: "SpecC言語によるハードウェア・ソフトウェア混在システム記述を対象としたプログラムスライシング手法の提案"電子情報通信学会技術研究報告 VLSI設計技術 VLD2003-149. 103・702. 79-84 (2004)