{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00015928","sets":["581:892:895"]},"path":["895"],"owner":"1","recid":"15928","title":["ハードウェア状態遷移表現のPrologによる検証"],"pubdate":{"attribute_name":"公開日","attribute_value":"1984-07-15"},"_buckets":{"deposit":"f05f19ac-e182-4033-90ca-938928774a58"},"_deposit":{"id":"15928","pid":{"type":"depid","value":"15928","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"ハードウェア状態遷移表現のPrologによる検証","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"ハードウェア状態遷移表現のPrologによる検証"},{"subitem_title":"Verification of State - Transition Based Hardware Descriptions with Prolog","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"論文","subitem_subject_scheme":"Other"}]},"item_type_id":"2","publish_date":"1984-07-15","item_2_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"東京大学大学院工学系研究科情報工学専門課程"},{"subitem_text_value":"東京大学工学部電気工学科"},{"subitem_text_value":"東京大学工学部電気工学科"}]},"item_2_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Information Engineering, Couse, Graduate School of Engineering, University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"Department of EIectrical Engineering, Faculty of Engineering, University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"Department of Electrical Engineering, Faculty of Engineering, University of Tokyo.","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/15928/files/IPSJ-JNL2504016.pdf"},"date":[{"dateType":"Available","dateValue":"1986-07-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-JNL2504016.pdf","filesize":[{"value":"615.8 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"8"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"a6e1787c-ef26-464c-a43d-78b752d5344b","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 1984 by the Information Processing Society of Japan"}]},"item_2_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"藤田, 昌宏"},{"creatorName":"田中, 英彦"},{"creatorName":"元岡達"}],"nameIdentifiers":[{}]}]},"item_2_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Masahiro, Fujita","creatorNameLang":"en"},{"creatorName":"Hidehiko, Tanaka","creatorNameLang":"en"},{"creatorName":"Tohru, Moyo-Oka","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_2_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN00116647","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_2_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7764","subitem_source_identifier_type":"ISSN"}]},"item_2_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"近年 素子技術の進歩に伴い 大規模・複雑なシステムの設計を短期間に正確に行う必要が増している.従来のゲートレベルのシミュレーションのみでなく ハードウェアの仕様記述からゲートによる記述まで一貫して設計・検証を支援するシステムが望まれる.そこで われわれは時相論理を用いて仕様記述を行い 階層設計を支援する論理設計検証システムをPrologを用いて作成することを提案し ゲート回路の検証について報告した.本論文では 状態遷移レベルのハードウェア記述言語であるDDLの記述に対する検証について考える.一般にシステムは 各端子間のデータ転送のタイミングを扱う同期部(synchronization part)と ALUのように実際に計算を行う演算部(function part)に分けて考えることができる.ここでは モジュール間のインタフェースを考えるときなどにとくに問題となる同期部を中心に DDL等で状態遷移表現されたものに対する 時相論理による仕様の検証手法について述べる.DDLの記述は 現在と次の時刻の関係の表としてPrologに変換され ゲートのときと同じようにして検証されるこのため DDL ゲートの混在するシステムも検証でき 階層設計を円滑に支援できる.同期部の設計は人間の不得意な分野であり 誤設計も起こりやすく 本システムの実用的価値は大きいと考える.","subitem_description_type":"Other"}]},"item_2_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"654","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌"}],"bibliographicPageStart":"647","bibliographicIssueDates":{"bibliographicIssueDate":"1984-07-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"4","bibliographicVolumeNumber":"25"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"id":15928,"updated":"2025-01-23T00:06:36.645232+00:00","links":{},"created":"2025-01-18T22:49:20.528619+00:00"}