1997 Fiscal Year Annual Research Report
| Project/Area Number |
09680348
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Kyoto Sangyo University |
|---|
Principal Investigator |
平石 裕美 京都産業大学, 工学部, 教授 (40093299)
|
|---|
| Keywords | 形式的検証 / 論理設計検証 / 様相論理 / 並列アルゴリズム / 分散アルゴリズム / 記号モデル検査 / BDD |
|---|
| Research Abstract |
本年度は、主として拡張時空間様相論理の基礎的研究と、並列/分散検証アルゴリズムの基礎的研究を行った。
1.拡張時空間様相論理:時空間様相論理の拡張として、有限長ビットスライス回路のモデル化と、双方向ビットスライス回路のモデル化を検討した。有限長ビットスライス回路を取り扱うために、無限長ビットスライス回路に対して仮想的にビット位置をカウントするカウンタを設置し、指定されたビット位置で出力を無効にする信号を生成するモデルを構築した。一方、双方向ビットスライス回路に対しては、信号線の方向応じて推論の空間的方向を変更する必要があることが判明した。したがって、空間軸に関しては、これまでのように正方向の空間様相演算子だけでなく、負方向の空間様相演算子をも導入する必要があり、今後このような双方向空間様相演算子の基本的性質について研究を進める必要があると思われる。
2.並列/分散検証アルゴリズム:CPUの個数が2〜20個程度の高性能ワークステーションに対する並列検証アルゴリズムとして、マルチスレッド方式にもとずく並列BDD処理アルゴリズム、並列記号モデル検査アルゴリズム、仕様の並列検証アルゴリズムなど種々のレベルにおける並列化を検討し、その諸性質を考察した。また、高速ネットワークに結合された数十台のワークステーションを用いる分散検証アルゴリズムに関しても、必要な共有データの分散キャッシュ法などについて検討を開始した。
|
