講演名 1999/3/3
プルーフチェッカーを用いた論理演算器の設計検証
和崎 克己, 不破 泰, 中村 八束, 師玉 康成,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 論理演算器の計算を多ソート代数でモデル化し, 証明はプルーフチェッカーを用いて検証する. 論理演算子, 演算子とハードウェアゲートとの関係, ゲート同士の信号線による接続等の定義・定理を基に, n-bit全加算・減算回路を例とし, 演算回路が正しく動作することを数学的に証明する. 信頼性の高い演算器実装に関する数理的手法を確立することが本研究の主眼である.
抄録(英) We propose the calculation models of the logical arithmetic unit based on the many sorted algebra, and verify the circuit's design by using a proof checker. The stability of circuits (n-bit full adder/subtracter examples) are proved based on the definitions and theorems about the logic operator, the hardware gates and the connection by signal lines. The insistence of this research is to establish the mtathematical principle technique concerning the calculation circuits with high reliability.
キーワード(和) プルーフチェッカー / 論理演算器 / ハードウエア記述 / 設計検証
キーワード(英) Proof Cheker / Arithmetic Logical Unit / hardware description / design verification
資料番号 VLD98-139
発行日

研究会情報
研究会 VLD
開催期間 1999/3/3(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 VLSI Design Technologies (VLD)
本文の言語 JPN
タイトル(和) プルーフチェッカーを用いた論理演算器の設計検証
サブタイトル(和)
タイトル(英) A Design Verification for the Arithmetie Logical Unit by using a Proof Cheker
サブタイトル(和)
キーワード(1)(和/英) プルーフチェッカー / Proof Cheker
キーワード(2)(和/英) 論理演算器 / Arithmetic Logical Unit
キーワード(3)(和/英) ハードウエア記述 / hardware description
キーワード(4)(和/英) 設計検証 / design verification
第 1 著者 氏名(和/英) 和崎 克己 / Katsumi WASAKI
第 1 著者 所属(和/英) 信州大学工学部
Faculty of Engineering, Shinshu University
第 2 著者 氏名(和/英) 不破 泰 / Yasushi FUWA
第 2 著者 所属(和/英) 信州大学工学部
Faculty of Engineering, Shinshu University
第 3 著者 氏名(和/英) 中村 八束 / Yatsuka NAKAMURA
第 3 著者 所属(和/英) 信州大学工学部
Faculty of Engineering, Shinshu University
第 4 著者 氏名(和/英) 師玉 康成 / Yasunari SHIMADA
第 4 著者 所属(和/英) 信州大学工学部
Faculty of Engineering, Shinshu University
発表年月日 1999/3/3
資料番号 VLD98-139
巻番号(vol) vol.98
号番号(no) 624
ページ範囲 pp.-
ページ数 8
発行日