私が属する研究グループでは，設計における高位の形式的設計検証法の提案お
よび検証支援システムの作成を行い，例題回路の設計検証による評価を行って
いる．検証支援システム内部では検証問題をいくつかの部分問題に分割し，各
問題を整数上の制約論理式であるプレスブルガー算術で表し，それらを真偽判
定ルーチンで判定するという手順で検証を行う．今回プレスブルガー算術の処
理のため，BDDの共有構造を取り入れたデータ構造を持つライブラリを作成し，
このライブラリを用いて新たに真偽判定ルーチンを作成した，また例題回路に
対する回路検証を行って従来の真偽判定ルーチンと比較した．これらについて
述べる．
Back