マイクロプロセッサの形式的論理設計検証システムの試作研究

1995 Fiscal Year Annual Research Report

• Project/Area Number: 07558155
• Research Category: Grant-in-Aid for Developmental Scientific Research (B)
• Research Institution: Kyoto University
• Principal Investigator: 矢島 脩三 京都大学, 工学研究科, 教授 (20025901)
• Co-Investigator(Kenkyū-buntansha): 平石 裕実 京都産業大学, 工学部, 教授 (40093299) ; 荻野 博幸 京都大学, 工学研究科, 助手 (40144323) ; 武永 康彦 京都大学, 工学研究科, 助手 (20236491) ; 浜口 清治 京都大学, 工学研究科, 講師 (80238055)
• Keywords: 形式的設計検証 / マイクロプロセッサ / 調理関数処理 / 二分決定グラフ / 二分モーメントグラフ / 三分決定グラフ / 機能レベル検証 / 算術演算回路検証

Research Abstract

実用規模のマイクロプロセッサは、一般に極めて大規模な回路として設計されるため、部分回路を抽象化した機能レベルの記述に対する設計検証と、各部分回路の機能の設計検証を個別に行う手法が有効であると考えられる。本年度は、この観点から次の研究を行った。
(1)機能レベルで記述された回路の設計検証技術
機能レベルの設計検証では、例えば、算術演算回路の機能を抽象的に関数記号と表現する必要があるが、これを形式的に取り扱うためには本研究では、等式を含む第一階述語論理のサブクラスに着目している。検証問題は、この論理における恒真性判定問題に帰着することができ、決定可能であることが知られているが、従来効率の良いアルゴリズムが知られていなかった。これに対して、本研究では二分決定グラフを用いた、実用的に有効と考えられるアルゴリズムを作成した。現在、このアルゴリズムの評価を行うため実装に取りかかっている。
(3)算術演算回路の設計検証技術
機能レベルにおいて抽象化される部分回路、例えば算術演算回路については個別に検証する必要がある。しかし、特に乗算器については、従来の手法では指数時間を要していた。これに対して、本研究では、二分モーメントグラフと呼ばれる関数の新しい表現手法を用いたアルゴリズムを新たに作成・実装して、多項式時間での検証が可能であることを実証した。
(3)論理関数処理手法に関する研究
各部分回路の形式的設計検証のためには、論理関数の効率的処理が必須である。本研究では、二分決定グラフを拡張した∧(∨)二分決定グラフや三分決定グラフについて、その表現能力の理論的な解析を行っている。

Research Products

• [Publications] K. Hamaguchi: "Efficient Construction of Binary Moment Digarams for Verifying Arithmefic Circuits." 1995 IE^3/ACM International Conference an Computer-Aided Design. 78-82 (1995)
• [Publications] H. Hiraishi: "Towands Verifaccition of Bit-Slice Circuits-Time-Space Model Checlcrg Approach-" IEICE Trans. Information and Systems. E78-D. 791-795 (1995)
• [Publications] H. Hiraishi: "Time-Space Modal Logic for Verification of Biy-Slice Circuits" Proc. 4th Computer-Aidal Design and Computar Graphics. 675-680 (1995)