@article{oai:ipsj.ixsq.nii.ac.jp:00015928, author = {藤田, 昌宏 and 田中, 英彦 and 元岡達 and Masahiro, Fujita and Hidehiko, Tanaka and Tohru, Moyo-Oka}, issue = {4}, journal = {情報処理学会論文誌}, month = {Jul}, note = {近年 素子技術の進歩に伴い 大規模・複雑なシステムの設計を短期間に正確に行う必要が増している.従来のゲートレベルのシミュレーションのみでなく ハードウェアの仕様記述からゲートによる記述まで一貫して設計・検証を支援するシステムが望まれる.そこで われわれは時相論理を用いて仕様記述を行い 階層設計を支援する論理設計検証システムをPrologを用いて作成することを提案し ゲート回路の検証について報告した.本論文では 状態遷移レベルのハードウェア記述言語であるDDLの記述に対する検証について考える.一般にシステムは 各端子間のデータ転送のタイミングを扱う同期部(synchronization part)と ALUのように実際に計算を行う演算部(function part)に分けて考えることができる.ここでは モジュール間のインタフェースを考えるときなどにとくに問題となる同期部を中心に DDL等で状態遷移表現されたものに対する 時相論理による仕様の検証手法について述べる.DDLの記述は 現在と次の時刻の関係の表としてPrologに変換され ゲートのときと同じようにして検証されるこのため DDL ゲートの混在するシステムも検証でき 階層設計を円滑に支援できる.同期部の設計は人間の不得意な分野であり 誤設計も起こりやすく 本システムの実用的価値は大きいと考える.}, pages = {647--654}, title = {ハードウェア状態遷移表現のPrologによる検証}, volume = {25}, year = {1984} }