設計検証技術(総論) : 現在の設計検証技術はペンティアムのバグを見つけることができるか

概要

論文の詳細を見る
集積回路技術の進歩に支えられて、ディジタルシステムの大規模化・複雑化が進むにつれ、設計の正しさを検証することがますます困難になってきている。最近では、インテル社のマイクロプロセッサであるペンティアムの設計誤りが大きな問題となった。設計検証でもっとも一般的に用いられてきている技術は、シミュレーションであるが、より厳密な検証結果を求めて、設計工程のいくつかの場面では、シミュレーションに代わる手法が実用化されつつある。本チュートリアルでは、ディジタルシステムの設計検証について、特に、近年急速に実用化が進んでいる新しい技術として、形式的検証(formal verification、フォーマルベリフィケーション)と、タイミング検証(timing verification)を取り上げ、その基本原理と実適用例を示す。また、現在の検証技術を用いて、ペンティアムの算術演算回路(除算回路)で発見された設計誤りを見つけることができるかどうかについて、いくつかの試みが行われており、これについても合わせて報告する。
社団法人電子情報通信学会の論文
1995-09-05