システム設計レベルにおける回路の性質検証のための整数データを処理可能なCTLモデル検査法の提案と実装

• Item type: SIG Technical Reports(1)
• 公開日: 2000-09-07
• タイトル: システム設計レベルにおける回路の性質検証のための整数データを処理可能なCTLモデル検査法の提案と実装
• タイトル / 言語: en
• タイトル: Proposal and Implementation of CTL Model Checking Algorithm Using Integer Data for Property Verification of Circuits on System Design Level
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 大阪大学大学院基礎工学研究科
• 著者所属: 大阪大学サイバーメディアセンター
• 著者所属: 大阪大学大学院基礎工学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Cybermedia Center, Osaka University
• 著者所属(英): en
• 著者所属(英): Graduate School of Engineering Science, Osaka University
• 著者名: 佐藤友哉; 北道, 淳司; 東野, 輝夫
• 著者名(英): Tomoya, Satoh; Junji, Kitamichi; Teruo, Higashino
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: NTTが開発したハードウェア記述言語であるSFLを用いて設計された回路に対し，その回路上で充足すべき性質が満足されているかどうかを形式的に検証する方法を提案する．論理設計レベルで用いられるCTLモデル検査法に対し，システム設計レベルにおいて用いられるレジスタを整数とみなし，整数データのままでCTLモデル検査法を行うことを考える．本研究では扱う整数データのクラスとしてプレスブルガー算術と呼ばれるクラスを採用する．本研究では回路モデルとして，上下限のある整数データを保持できるレジスタを有する拡張有限状態機械EFSMを採用し，回路記述言語SFLからEFSMへの変換手順を示し，EFSMに対するCTLモデル検査アルゴリズムを提案する．アルゴリズムの実現においては，我々が開発したプレスブルガー算術処理用ライブラリを用いた．SFLで記述した例題回路に対して実現した検証系を用いて実際に検証を行った結果について報告する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: For designed circuits described with SFL ; hardware description language developed by NTT, we propose a formal verification method which determines whether the properties that circuits should satisfy is actually true or not. Against CTL model checking in general applied on logic design level, we regard a register on system design level as an integer and execute CTL model checking using integer data. In our research, we adopt Presburger arithmetic, a class of integer. As a circuit model we introduce extended finite state machine(EFSM) with registers that can hold integer data, give the translation algorithm to EFSM from SFL, and propose CTL model checking algorithm on proposed EFSM. For implementation of the algorithm, the library we developed for the operation of Presburger arithmetic is used. Finally we describe the results of verification for example SFL circuits.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 2000, 号 79(2000-SLDM-097), p. 17-24, 発行日 2000-09-07
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会