代数的手法を用いたハードウェアの仕様記述と実現に関する研究

点击翻译按钮获取中文摘要

1.同期式順序回路の仕様を代数的言語で書くときの記述のスタイルを提案した。そのスタイルはいわゆる抽象的順序機械型の記述であり、動作の実行順序制御部は、その動作を行うべきときの条件を指定するという形で記述する。この記述スタイルによって、回路の抽象的な機能の仕様から、バス・レジスタの接続や、既存のIC等を用いた具体レベルにおける入力論理式まで、同じ言語・同じスタイルで記述することができる。検証等の形式的な議論には、形式的・厳密に定義された同一言語による記述が必要である。また、このスタイルに従って、回路の実現や詳細化問題の定式化を行った。2.マイクロコンピュータとクィックソートIC(後者は日本電子工業振興会のLSI設計用記述言語の標準化の調査研究で用いられたもの)を例題にして、仕様記述・詳細化を行った。前者では、命令の意味定義の記述からレジスタなどの入力線の論理設計まで、後者では、ソーティングの一般的な要求仕様から、クィックソートアルゴリズム採用レベルの記述を経て、同じくレジスタ等の入力論理の設計まで行った。これにより、状態遷移図やレジスタ転送レベルの記述より抽象的なレベルの記述から、論理設計レベルまで段階的に記述できることがわかった。3.上記2.の記述・設計経験によって、設計者は上位レベルと下位レベルの回路動作の対応のみを孝案し、それを基に下位レベルの実行制御部の記述を自動生成するのが実用的であることがわかった。この自動化の問題は、回路動作を詳細化する一般の場合と入力論理式を導出する具体レベルの二つに分かれる。両者に対してアルゴリズムを孝案し、プログラム化し、我々の代数的記述支援系に組み込み、2.の例の一部に適用してみた。仕様記述及び段階的詳細化に代数的手法の有効性が確認できたが、今後は、検証(正しさの証明)手法の確立が望まれる。