プレスブルガー文真偽判定手続きを用いた算術演算回路の正しさの証明

• Item type: SIG Technical Reports(1)
• 公開日: 1996-10-17
• タイトル: プレスブルガー文真偽判定手続きを用いた算術演算回路の正しさの証明
• タイトル / 言語: en
• タイトル: Automatic Verification of Arithmetic Circuits using a Decision Procedure for Presburger Arithmetic
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 大阪大学 基礎工学部 情報工学科
• 著者所属: 大阪大学 基礎工学部 情報工学科
• 著者所属: 大阪大学 基礎工学部 情報工学科
• 著者所属: 大阪大学 基礎工学部 情報工学科
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者名: 森岡, 澄夫; 柴田, 直樹; 東野, 輝夫; 谷口, 健一
• 著者名(英): Sumio, Morioka; Naoki, Shibata; Teruo, Higashino; Kenichi, Taniguchi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 加算器，乗算器，ALUなど，算術演算を行う組み合わせ論理回路が，そのワードレベル仕様F（整数上の論理式として書かれた入出力関係の記述）を正しく実現している事を，プレスブルガー文真偽判定手続きを用いて自動証明する方法と，証明例について述べる．証明は，いわゆるビットレベル炉証（各回路モジュールM_jごと，そのワードレベル仕様F_jがゲートレベルで正しく実現されていることの証明）とワードレベル検証（各M_jの接続関係および各ワードレベル仕様F_jのもとで，Fが満たされることの証明）に分けて行う．乗算など，プレスブルガー算術で直接扱えない演算を行う回路についても，その演算に関して数学的に成り立つ性質等を仮定することにより，証明できる場合がある．本手法の特徴は，幾つかの工夫を行ったプレスブルガー真偽判定ルーチンを用いることにより，各モジュールの演算ビット長nが増えても，回路中のモジュールの数や組合せ方が同じで，かつ仕様記述のサイズがnに依存していなければ，ワードレベル検証にかかる時間がほとんど増加しないことである．例えばnビット乗算器から2nビット乗算器を構成した場合のワードレベル検証を，2分程度のCPU時間で行えた．ビットレベル検証についても，演算ビット長が4ビット程度であれば，例えば加減算・論理演算を行うALU(438)について6分程度のCPU時間で行えた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper we present a method to prove automatically that given arithmetic circuits, such as adders, multipliers and ALUs, correctly implement their overall circuit functionality F, using Presburger arithmetic. The F is given as word-level specifications, that are the descriptions of relations between circuits' inputs and outputs on integer variables and integer operators. We adopt a hierarchical approach to verify arithmetic circuits; first the gate-level component modules M_j in the circuits are shown to implement their world-level specifications F_j (so called "bit-level verification"), and then F is proved on both F_js and the description of connections among all modules (so called "word-level verification"). The feature of our proof method is that the CPU time needed for the word-level verification is almost independent of the word-length (bit number) n of the modules, if both the circuits' architecture and the size of F and F_js are also independent of n. We have recently improved the computation time of a decision algorithm for Presburger arithmetic. Using the improved decision procedure, we have carried out the word-level verification of 2n-bit multipliers within about 2 minutes (CPU time), where each of those 2n-bit multipliers is constructed from four n-bit multipliers. We have also carried out the bit-level verification of a 4-bit ALU (74382) within about 6 minutes.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 1996, 号 101(1996-SLDM-081), p. 81-88, 発行日 1996-10-17
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会