複数の制御部を持つ同期式順序回路の一設計検証法

• Item type: Journal(1)
• 公開日: 1998-07-15
• タイトル: 複数の制御部を持つ同期式順序回路の一設計検証法
• タイトル / 言語: en
• タイトル: A Formal Method of Design and Verification for the Synchronous Sequential Circuit with Plural Controllers
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 設計技術と設計自動化
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属(英): en
• 著者所属(英): Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University
• 著者名: 竹中, 崇; 北道, 淳司; 西川, 清史
• 著者名(英): Takashi, Takenaka; Junji, Kitamichi; Seishi, Nishikawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 複数の制御部を持つ同期式順序回路の設計の正しさを保証するための形式的手法を用いた一設計検証法を提案する．本手法は，抽象度が高く1つの制御部で実現されている回路（以下，上位レベルの回路）が与えられ，より抽象度が低く複数の制御部で実現されている回路（以下，下位レベルの回路）を設計し，上位レベルの回路と下位レベルの回路との間の対応を与えたときに，下位レベルの回路が対応のもとで上位レベルの回路を正しく実現していることを証明する方法である．複数の制御部を持つ回路を検証する場合，各制御部の直積機械を生成するという手法が一般的であるが，この手法では計算時間および計算空間が増大し，大規模な回路の場合は検証が不可能である．本手法では，上位レベルの回路の各状態遷移に対して，状態を持つ部品ごとに下位レベルの回路の状態遷移系列を設計者が対応づけ，上位レベルの回路の状態遷移ごとにレジスタ転送や制御構造などが正しく実現されていることを局所的に証明することにより，各制御部の直積機械を生成することなく検証を行う．本手法をPCIバスを介してCPUモジュールとメモリモジュールを接続する回路に適用した．この例の回路規模は制御部数9，遷移数96であった．証明が成功したときのCPU時間は約20分であった．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper,we propose a formal method of design and verification for the synchronous sequential circuit with plural controllers.When the circuit with one controller at the higher level is given,the circuit design according to our method is proceeded as follows.The designer (1)desegns the more detailed circuit with plural controllers at the lower level and (2)gives the correspondence relation between two levels,and(3)verifies the correctness of this design.In the general verification methods,a product machine is generated for the circuit with plural controllers,and the equivalence between the higher level circuit and the product machine is verified.However,in these methods the extensive time and space for the verification often prevents verifying the large scale circuits.In our method the designer gives the correspondence relation for each circuit component between each state transition of the higher level circuit and a sequence of state transitions of the lower level circuit,and proceeds the verification locally according to this correspondence relation.So the process of verification is able to be carried without generating the product machine.We evaluated the proposed method for verifying the circuit which is connecting between CPU module and memory module.This circuit has 9 controllers and 96 state transitions.The CPU time for the verification was about 20 minutes.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 39, 号 7, p. 2308-2322, 発行日 1998-07-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764