文献

J-GLOBAL ID：201302257633382544   整理番号：13A1479958

全プレフィックス和演算を用いた整数加算器の形式的証明

Formal proof of integer adders using all-prefix-sums operation

著者 (3件)： Liu Feng (School of Computer Sci.,National Univ. of Defense Technol., Changsha) ,  Tan QingPing (School of Computer Sci.,National Univ. of Defense Technol., Changsha) ,  Mohamed Otmane Ait (Dep. of Electrical and Computer Engineering,Concordia Univ., Canada, Montreal)
資料名： Science China. Information Sciences  (Science China. Information Sciences)
巻： 55  号： 9  ページ： 1949-1960  発行年： 2012年 
JST資料番号： C2579A  ISSN： 1674-733X  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 中国 (CHN)  言語： 英語 (EN)

抄録/ポイント： 2つの二進数の加算は,電子回路における基本動作である。いくつかの整数加算器アーキテクチャを提案してきた。それらの形式的特性は良く知られているが,証明の発見が不完全あるいは困難である。この論文は,接頭部分列加算器の正当性のための形式的証明を提示する。逐次および並列アルゴリズムの両方を形式化し,証明する。高次汎関数や書換システムを使用する以前の証明とは対照的に,この研究は一次再帰方程式に基づいており,それはコンピュータ演算応用分野で良く知られており,従ってVLSI回路設計に取組む人々によって理解可能である。この研究は,コンピュータ演算アルゴリズムの形式的証明に関する更なる研究の基盤を提示する。Data from the ScienceChina, LCAS. Translated by JST

シソーラス用語： 加算器 ,  *並列アルゴリズム ,  計算機アーキテクチャ ,  コンピュータ ,  LSI【IC】 ,  超LSI ,  回路設計 ,  電子回路 ,  動作
準シソーラス用語： プレフィックス ,  アーキテクチャ ,  LSI回路 ,  VLSI ,  基本動作

分類 (1件)： 数値計算  (JE02000J)

タイトルに関連する用語 (4件)： プレフィックス ,  整数 ,  加算器 ,  証明