実行命令数に関する数学的帰納法と再帰帰納法による形式検証

• Item type: SIG Technical Reports(1)
• 公開日: 1993-01-21
• タイトル: 実行命令数に関する数学的帰納法と再帰帰納法による形式検証
• タイトル / 言語: en
• タイトル: Formal Verification Using Mathematical and Recursive Induction on the Number of Instructions Executed
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: （株）日立製作所 中央研究所
• 著者所属: （株）日立製作所 中央研究所
• 著者所属(英): en
• 著者所属(英): Central Research Laboratory, Hitachi, Ltd.
• 著者所属(英): en
• 著者所属(英): Central Research Laboratory, Hitachi, Ltd.
• 著者名: 庄内亨; 清水, 嗣雄
• 著者名(英): Toru, Shonai; Tsuguo, Shimizu
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: プロセッサ等の順序論理回路を再帰関数としてモデル化して行なう形式的論理検証において、実行命令数に関する数学的帰納法を用いる証明法と再帰帰納法を用いる証明法を提案した。この方法では、順序論理回路をモデル化したレジスタトランスファ記述の再帰関数を、動作記述の再帰関数に変換した後、帰納法を適用する。例として、2段パイプライン制御プロセッサを3方法で証明し、比較評価したところ、従来の動作クロック数に関する数学的帰納法に比べ、実行命令数に関する数学的帰納法を用いると証明すべきケース数を約1/2に削減できた。更に、再帰帰納法を用いると証明のための書き換え操作数を減らせる。評価対象の拡大が今後の課題である。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: This paper describes methods using mathematic and recursive induction on the number of instructions executed for formal verification of sequential logic circuits such as processors when modeling these circuits in terms of recursive functions. Register-transfer-type recursive functions modeling sequential circuits are transformed to behavior-type recursive functions, which are then proven with induction. Comparison among three methods for proving the correctness of a 2-stage pipelined processor is given. By using the two new methods based on mathematical and recursive induction on the number of instructions executed, it is found that the number of cases necessary to be proven is reduced by half of that using mathematical induction on the number of cycles executed in the previous approach. The recursive induction method also reduces rewriting operations, further increasing verification speed.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 1993, 号 6(1992-SLDM-065), p. 57-64, 発行日 1993-01-21
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会