EVBDDに基づく初等関数回路の設計検証

摘要

本稿では，EVBDD（Edge-Valued Binary Decision Diagram）に基づく初等関数回路の設計検証手法を提案する．提案手法は，検証対象となる回路をEVBDDでコンパクトに表現し，設計仕様を表現するEVBDD（参照モデル）と比較することで回路の最大誤差を算出する．算出した最大誤差が許容範囲内かを確認することで初等関数回路を形式的に検証できる．回路からEVBDDを効率よく自動生成するために，回路内の算術演算に対応したEVBDDの演算アルゴリズムも提案する．計算機実験により，提案検証法の効率を示す．