算術演算回路検証の技術

概要

論文の詳細を見る
ペンティアムの4進SRT法に基づく除算回路での設計誤りは、ルックアップ・テーブルの内容に書き間違いがあるというものであった。こうした設計誤りを通常のシミュレーションで網羅的に調べることは、膨大な時間を要するため、非現実的である。これに対して、BryantはOBDDによる組合せ回路の等価性判定の手法を用いて、網羅的な検証を試みており、SPARCstation10上で主記憶112MByte、CPU時間10分で検証に成功したと報告している。また、Bryantの手法の場合、等価性判定の比較対象として、ピットレベルの論理式を記述する必要があって、これは必ずしも容易ではないが、Zhaoらは、二分モーメントグラフ(Binary Moment Diagram)と呼ばれる新しいデータ構造を用いて、レジスタに対する加算や不等号などを許した仕様記述を、ビットレベルに変換せず、直接扱う検証手法を考案・実装して、検証に成功している。これらの手法は、算術演算回路の検証技術として現在盛んに研究されている。本チュートリアルでは、その最新の研究動向を報告する予定である。
社団法人電子情報通信学会の論文
1995-09-05