Arithmetic Circuit Verification Based on Symbolic Computer Algebra
スポンサーリンク
概要
- 論文の詳細を見る
This paper presents a formal approach to verify arithmetic circuits using symbolic computer algebra. Our method describes arithmetic circuits directly with high-level mathematical objects based on weighted number systems and arithmetic formulae. Such circuit description can be effectively verified by polynomial reduction techniques using Gröbner Bases. In this paper, we describe how the symbolic computer algebra can be used to describe and verify arithmetic circuits. The advantageous effects of the proposed approach are demonstrated through experimental verification of some arithmetic circuits such as multiply-accumulator and FIR filter. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits.
- (社)電子情報通信学会の論文
- 2008-10-01
著者
-
樋口 龍雄
東北工業大学工学部電子工学科
-
HOMMA Naofumi
Department of Computer and Mathematical Sciences, Graduate School of Information Sciences, Tohoku Un
-
AOKI Takafumi
Department of Computer and Mathematical Sciences, Graduate School of Information Sciences, Tohoku Un
-
HIGUCHI Tatsuo
Department of Electronics, Tohoku Institute of Technology
-
Homma Naofumi
Department Of Computer And Mathematical Sciences Graduate School Of Information Sciences Tohoku Univ
-
Aoki T
The Department Of Computer And Mathematical Sciences Graduate School Of Information Sciences Tohoku
-
Aoki Takafumi
Graduate School Of Information Sciences Tohoku University:(present Address)presto Jst.
-
Aoki Takafumi
The Department Of System Information Sciences Graduate School Of Information Sciences Tohoku Univers
-
Higuchi Tatsuo
Tohoku Inst. Technol. Sendai‐shi Jpn
-
Higuchi Tatsuo
Department Of Electronics Tohoku Institute Of Technology
-
Higuchi Tatsuo
Department Of Electronic Engineering Tohoku Institute Of Technology
-
Higuchi Tatsuo
The Department Of Electronics Faculty Of Engineering Tohoku Institute Of Technology
-
Higuchi Tatsuo
The Department Of System Information Sciences Graduate School Of Information Sciences Tohoku Univers
-
Higuchi Tatsuo
Hitachi Ltd. Central Research Laboratory
-
Aoki Takafumi
Department Of Computer And Mathematical Sciences Graduate School Of Information Science Tohoku Unive
-
WATANABE Yuki
Department of Computer and Mathematical Sciences, Graduate School of Information Sciences, Tohoku Un
-
Homma Naofumi
Tohoku Univ. Sendai‐shi Jpn
-
羽生 貴弘
東北大 電通研
-
Homma Naofumi
Department Of Computer And Mathematical Sciences Graduate School Of Information Sciences Tohoku Univ
-
Aoki Takafumi
Department Of Chemistry Graduate School Of Science Osaka University
-
Watanabe Yuki
Department Of Computer And Mathematical Sciences Graduate School Of Information Sciences Tohoku Univ
関連論文
- 受動型ステレオビジョンを用いた2D・3D複合顔認証
- 位相限定相関法とそのバイオメトリクス認証への応用(チュートリアル講演,通信品質,メディア・インタフェース及び一般)
- 位相情報を用いた主成分分析による掌紋認証アルゴリズム(テーマセッション,手,顔,身体表現の認識,理解)
- 位相情報を用いた主成分分析による掌紋認証アルゴリズム(テーマセッション4)
- 位相情報に基づく画像マッチング技術とその応用展開 : 3Dビジョンからバイオメトリクスまで
- 大規模災害のための歯科X線画像認識システムと性能評価(若葉研究者の集い2,サマーセミナー(若葉研究者の集い))
- 位相限定相関法に基づく画像マッチングのGPU実装とその応用(若葉研究者の集い4,サマーセミナー(若葉研究者の集い))
- 位相限定相関法を用いた3次元計測の高精度化と性能評価(若葉研究者の集い3,サマーセミナー(若葉研究者の集い))
- 位相限定相関法を用いた超解像デインタレーシング(ディジタル信号処理)
- プロジェクタ・カメラシステムを用いた投影画像の幾何補正に関する実験的検討
- Systematic Interpretation of Redundant Arithmetic Adders in Binary and Multiple-Valued Logic(Novel Device Architectures and System Integration Technologies)
- Multiple-Valued Constant-Power Adder and Its Application to Cryptographic Processor
- フォトニック結晶偏光子を用いた偏光イメージングカメラの開発(ナノ光技術・電子技術,次世代ナノテクノロジー論文)
- 位相限定相関法を用いた顔認証アルゴリズムの検討
- 一次元位相限定相関法に基づくステレオ画像の高精度サブピクセル対応付け手法(画像認識,コンピュータビジョン)
- 歯科X線写真のための位相限定相関法を用いた高精度位置合せアルゴリズム(画像処理・表示,医用画像論文)
- B-18-1 位相限定相関法を用いた指紋認証アルゴリズムのFPGA実装(B-18. バイオメトリクス・セキュリティ,一般セッション)
- 位相限定相関法に基づく虹彩認証アルゴリズムとその高性能化--低画質な虹彩画像に対してもロバストな認証を実現
- 位相限定相関法を用いた掌紋認証アルゴリズムとその高性能化 (第21回 回路とシステム軽井沢ワークショップ論文集)
- 受動型3次元顔認証システムとその性能評価(システムLSIの応用と要素技術,専用プロセッサ,プロセッサ,DSP,画像処理技術及び一般)
- 映像のサブピクセル動き推定の実験的検討(システムLSIの応用と要素技術,専用プロセッサ,プロセッサ,DSP,画像処理技術及び一般)
- 位相限定相関法を用いた掌紋認証アルゴリズムとその性能評価 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (画像応用)
- 1次元位相限定相関法に基づく画像の高精度回転計測アルゴリズムとその評価 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (画像処理)
- 表情変化にロバストな3次元顔認証アルゴリズムの検討 (第21回 回路とシステム軽井沢ワークショップ論文集) -- (インタラクティブセッション)
- A Single-Electron-Transistor Logic Gate Family for Binary, Multiple-Valued and Mixed-Mode Logic(New System Paradigms for Integrated Electronics)
- A Simulation Methodology for Single-Electron Multiple-Valued Logics and Its Application to a Latched Parallel Counter
- 位相限定相関法に基づく指紋照合アルゴリズムとその評価(画像処理(2), 信号処理, LSI, 及び一般)
- 位相限定相関法に基づく指紋照合技術 : 一般住宅向け指紋照合装置のためのアルゴリズム設計と実現
- 並列プレフィックス加算器を用いた算術演算モジュールの自動生成(信号処理,LSI,及び一般)
- 並列プレフィックス加算器を用いた算術演算モジュールの自動生成(信号処理,LSI,及び一般)
- 並列プレフィックス加算器を用いた算術演算モジュールの自動生成(信号処理,LSI,及び一般)
- 算術演算回路の形式的検証手法とその評価(デザインガアイ2006-VLSI設計の新しい大地を考える研究会)
- 算術演算回路の形式的検証手法とその評価(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 算術演算回路の形式的検証手法とその評価(検証,デザインガイア2006-VLSI設計の新しい大地を考える研究会)
- 算術演算回路の形式的検証手法とその評価
- Free Oligosaccharides with Lewis x Structure Expressed in the Segmentation Period of Zebrafish Embryo
- 算術アルゴリズム記述言語ARITHに基づく算術演算回路の形式的設計(ハードウェア/ソフトウェア設計技術, 信号処理, LSI, 及び一般)
- 算術アルゴリズム記述言語ARITHに基づく算術演算回路の形式的設計(ハードウェア/ソフトウェア設計技術, 信号処理, LSI, 及び一般)
- 算術アルゴリズム記述言語ARITHに基づく算術演算回路の形式的設計(ハードウェア/ソフトウェア設計技術, 信号処理, LSI, 及び一般)
- I-022 位相限定相関法と特徴点マッチングの組み合わせに基づく指紋照合アルゴリズム(I分野:画像認識・メディア理解)
- 位相限定相関法に基づく指紋照合アルゴリズムとその評価(画像処理(2), 信号処理, LSI, 及び一般)
- 位相限定相関法に基づく指紋照合アルゴリズムとその評価(画像処理(2), 信号処理, LSI, 及び一般)
- A High-Resolution Phase-Based Waveform Matching and Its Application to Side-Channel Attacks
- SC-11-14 電流モード多値論理に基づくプログラマブルディジタルフィルタLSIの性能評価(SC-11.新概念VLSI : 先進アーキテクチャ,新回路,デバイス技術)
- A Dental Radiograph Recognition System Using Phase-Only Correlation for Human Identification
- Score-Level Fusion of Phase-Based and Feature-Based Fingerprint Matching Algorithms
- A Robust 3D Face Recognition Algorithm Using Passive Stereo Vision
- SC-11-8 分子コンピューティング集積回路のための多チャンネルポテンショスタットの試作(SC-11.新概念VLSI : 先進アーキテクチャ,新回路,デバイス技術)
- A-2-9 人工触媒素子に基づく画像処理の検討
- A Redox Microarray : An Experimental Model for Molecular Computing Integrated Circuits(New System Paradigms for Integrated Electronics)
- An Image Completion Algorithm Using Occlusion-Free Images from Internet Photo Sharing Sites
- 冗長数系に基づく高速加算器の最適設計(ハードウェア/ソフトウェア設計技術, 信号処理, LSI, 及び一般)
- 冗長数系に基づく高速加算器の最適設計(ハードウェア/ソフトウェア設計技術, 信号処理, LSI, 及び一般)
- 冗長数系に基づく高速加算器の最適設計(ハードウェア/ソフトウェア設計技術, 信号処理, LSI, 及び一般)
- 算術アルゴリズム記述言語を用いた乗算器モジュールジェネレータの構築(アルゴリズム)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会)
- 算術アルゴリズム記述言語を用いた乗算器モジュールジェネレータの構築(アルゴリズム)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 算術アルゴリズム記述言語を用いた乗算器モジュールジェネレータの構築(アルゴリズム)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- 算術アルゴリズム記述言語を用いた乗算器モジュールジェネレータの構築(アルゴリズム)(VLSIの設計/検証/テスト及び一般)(デザインガイア2004-VLSI設計の新しい大地を考える研究会-)
- Counter Tree Diagramに基づく冗長加算器の系統的設計手法 : 冗長2進加算器設計の例(演算回路)(システムLSIの設計技術と設計自動化)
- A-3-10 Counter Tree Diagram に基づく冗長2進加算器の設計(A-3. VLSI設計技術)
- Arithmetic Circuit Verification Based on Symbolic Computer Algebra
- Formal Design of Arithmetic Circuits Based on Arithmetic Description Language(Circuit Synthesis,VLSI Design and CAD Algorithms)
- A Shortest Path Search Algorithm Using an Excitable Digital Reaction-Diffusion System (Signal Processing Algorithm, Multidimensional Signal Processing and Its Application)
- High-Accuracy Estimation of Image Rotation Using 1D Phase-Only Correlation
- A Passive 3D Face Recognition System and Its Performance Evaluation
- A Palmprint Recognition Algorithm Using Phase-Only Correlation
- A Fingerprint Matching Algorithm Using Phase-Only Correlation(Digital Signal Processing for Pattern Recognition)(Applications and Implementations of Digital Signal Processing)
- High-Accuracy Subpixel Image Registration Based on Phase-Only Correlation(Digital Signal Processing)
- Signed-Weight Arithmetic and Its Application to a Field-Programmable Digital Filter Architecture (Special Issue on Integrated Electronics and New System Paradigms)
- A Sub-Pixel Correspondence Search Technique for Computer Vision Applications(Image/Visual Signal Processing)(Digital Signal Processing)
- Counter Tree Diagrams : A Unified Framework for Analyzing Fast Addition Algorithms(IP Design)(VLSI Design and CAD Algorithms)
- Design of a Field-Programmable Digital Filter Chip Using Multiple-Valued Current-Mode Logic(Digital Signal Processing)
- Fingerprint Restoration Using Digital Reaction-Diffusion System and Its Evaluation(Digital Signal Processing)
- Parallel Evolutionary Graph Generation with Terminal-Color Constraint and Its Application to Current-Mode Logic Circuit Design(Nonlinear Theory and Its Applications)
- Parallel Evolutionary Design of Constant-Coefficient Multipliers
- Multiple-Valued Constant-Power Adder and Its Application to Cryptographic Processor
- RX-NAS : A Scalable, Reliable Clustered NAS System(Parallel and Distributed Processing Technology)
- 次世代分子コンピューティングを目指して (特集 次世代化学技術の飛躍)
- Evolutionary Synthesis of Fast Constant-Coefficient Multipliers
- Evolutionary Design of Arithmetic Circuits (Special Section on Discrete Mathematics and Its Applications)
- 基線長変化にロバストなステレオ画像間の高精度対応付け手法(3次元画像処理,多視点画像処理,画像の認識・理解論文)
- 多視点ステレオのための位相限定相関法に基づく画像マッチングの高精度化
- 選択したデータセットを用いた暗号デバイスの電磁情報漏えいの効率的な安全性評価(多様化する電磁環境におけるEMC対策設計・評価技術論文)
- 携帯電話向け非接触掌紋認証アルゴリズム(画像)
- 超音波画像診断のための造影剤検出手法とその性能評価(若葉研究者の集い5,サマーセミナー2013〜画像処理の理論と実際〜)
- レーザ回折光に基づく簡便な3次元計測システムとその応用に関する検討(若葉研究者の集い2,サマーセミナー2013〜画像処理の理論と実際〜)
- ステレオマッチングに最適な動画像のフレーム選択に基づく3次元復元手法の検討(若葉研究者の集い2,サマーセミナー2013〜画像処理の理論と実際〜)
- 災害に役立つ情報通信サービス(ポストIPネットワーキング,新世代ネットワーク,ネットワークモデル,インターネットトラピック,TCP/IP,マルチメディア通信,ネットワーク管理 リソース管理,プライベートネットワーク,NW安全性及び一般)
- 災害に役立っ情報通信サービス(ポストIPネットワーキング,新世代ネットワーク,ネットワークモデル,インターネットトラヒック,TCP/IP,マルチメディア通信,ネットワーク管理,リソース管理,プライベートネットワーク,NW安全性及び一般)
- 8 画像処理技術とオープンイノベーションの展開(東北から明るい未来を創るICT技術)
- 指関節紋画像の変形にロバストな指関節紋認証アルゴリズム(指関節紋認証,バイオメトリクス論文)
- 正確な色再現を目的とした2眼ステレオ式6バンドビデオシステム(テーマセッション,実時間処理実空間センシングと環境理解)
- 災害に役立っ情報通信サービス(ポストIPネットワーキング,新世代ネットワーク,ネットワークモデル,インターネットトラピック,TCP/IP,マルチメディア通信,ネットワーク管理,リソース管理,プライベートネットワーク,NW安全性及び一般)
- A-7-5 漏えい電磁情報を用いた任意の処理への非侵襲な故障注入手法(A-7.情報セキュリティ,一般セッション)
- BI-1-6 意図的な電磁妨害による暗号デバイスからの情報漏えいの脅威とその対策(BI-1.安全・安心な情報通信会社を実現する電磁情報セキュリティ評価・対策技術,依頼シンポジウム,ソサエティ企画)
- AS-6-3 非接触型掌紋認証アプリのユーザインタフェースに関する検討(AS-6.バイオメトリクスの多様性,シンポジウムセッション)
- 正確な色再現を目的とした2眼ステレオ式6バンドビデオシステム(テーマセッション,実時間処理実空間センシングと環境理解)
- 暗号モジュールから漏洩する情報を利用するサイドチャネル攻撃
- 暗号機器に故障を引き起こす妨害電磁波の可視化(PCB,情報セキュリティ,EMC,一般)
- 超音波画像診断のための高精度造影剤検出手法の検討(一般セッション,計算解剖学における数理モデルの深化と応用展開)