動作合成前後の設計記述に対する記号シミュレーションによる形式的等価性検証の検討(検証・シミュレーション,システム設計及び一般)

概要

論文の詳細を見る
システムレベル設計によって得られた動作記述と制約から、動作合成によってRTL設計を導出する設計フローにおいては、動作合成前後の動作記述とRTL設計の動作の等価性が保証されていることが重要である。しかし、そのための等価性検証手法、特に形式的手法は、実用化されているものははとんどないのが現状である。そこで、本稿では、動作合成前後の設計の等価性を形式的に検証する一手法を提案し、その評価を行う。提案する手法では、RTL設計を解析して抽出された、1サイクルで行われる動作と、合成前の動作記述を記号的に実行して、形式的に等価性を検証する。RTL設計から動作を抽出する作業では、いくつかの変換規則を適用することによって、RTL設計中のピット結合などのピットレベル処理をワードレベルの処理に置き換え、個々の演算を解釈せずに検証が可能になるようにしている。また、いくつかの設計例に対して実験を行い、指定された適当な等価性を検証できることを確認した。
社団法人電子情報通信学会の論文
2006-05-05