タイミング制約を含んだ回路記述方式とその意味論

• Item type: SIG Technical Reports(1)
• 公開日: 2014-11-19
• タイトル: タイミング制約を含んだ回路記述方式とその意味論
• タイトル / 言語: en
• タイトル: A hardware description method and sematics providing a timing constrant
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 回路設計手法
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 熊本大学大学院自然科学研究科
• 著者所属: 熊本大学大学院自然科学研究科
• 著者所属: 熊本大学大学院自然科学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Kumamoto University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Kumamoto University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Kumamoto University
• 著者名: 西村, 俊二; 尼崎, 太樹; 末吉, 敏則
• 著者名(英): Shunji, Nishimura; Motoki, Amagasaki; Toshinori, Sueyoshi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 数学的な理論に基づく厳密な検証が可能となることから，各種の形式検証手法が広がりつつあるが，その検証対象は同期回路に限られている．非同期回路については，遅延値が不明な回路記述のみを対象としての検証は意味をなさないからである．本稿では形式検証の対象を同期回路以外にも広げるべく，タイミング制約を含んだ回路記述方式とその意味論を提案する．提案の記述方式は，プログラミング言語のクラス Arrow の概念を用いて構成要素中心の考え方を可能にする．また，その意味論は様相論理のクリプキ意味論を用い，抽象的な遅延の概念を導入する．提案の回路記述とその意味論により，非同期回路についても形式検証が可能となることを示す．また，実用化に向けた試みとして定理証明言語 Agda 上の実装もあわせて示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Formal verification methods are wide-spreading due to its mathmatical rigorous aspect, although they limited to synchrounous circiut. For an asynchronou circuit, It is almost no meaning in verification along undefined delay values on circuit description phase. In this article, we propose a hardware description method and semantics providing a timing constraint to allow verification of an asynchronous circuit. The description method is componen t-centered by introducing a concept of Arrows that is a class of a programming language. The semantics employs an abstract delay under Kripke semantics of modal logic. Verification of an asynchronous circuit become possible with applying the description method and semantics. We also show an implementation of the description and semantics on theorem prover Agda.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 研究報告システムとLSIの設計技術（SLDM）; 巻 2014-SLDM-168, 号 7, p. 1-6, 発行日 2014-11-19
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会