プレスブルガー文真偽判定手続きを用いた算術演算回路の正しさの証明
スポンサーリンク
概要
- 論文の詳細を見る
加算器, 乗算器, ALUなど, 算術演算を行う組み合わせ論理回路が, そのワードレベル仕様F (整数上の論理式として書かれた入出力関係の記述) を正しく実現している事を, プレスブルガー文真偽判定手続きを用いて自動証明する方法と, 証明例について述べる. 証明は, いわゆるビットレベル検証 (各回路モジュールM_jごと, そのワードレベル仕様F_jがゲートレベルで正しく実現されていることの証明) とワードレベル検証 (各M_jの接続関係および各ワードレベル仕様F_jのもとで, Fが満たされることの証明) に分けて行う. 乗算など, プレスブルガー算術で直接扱えない演算を行う回路についても, その演算に関して数学的に成り立つ性質等を仮定することにより, 証明できる場合がある. 本手法の特徴は, 幾つかの工夫を行ったプレスブルガー真偽判定ルーチンを用いることにより, 各モジュールの演算ビット長 n が増えても, 回路中のモジュールの数や組合せ方が同じで, かつ仕様記述のサイズが n 依存していなければ, ワードレベル検証にかかる時間がほとんど増加しないことである. 例えば n ビット乗算器から 2n ビット乗算器を構成した場合のワードレベル検証を, 2分程度のCPU時間で行えた. ビットレベル検証についても, 演算ビット長が4ビット程度であれば, 例えば加減算・論理演算を行うALU (74382) について6分程度のCPU時間で行えた.
- 社団法人電子情報通信学会の論文
- 1996-10-18
著者
-
柴田 直樹
大阪大学大学院基礎工学研究科情報数理系専攻
-
東野 輝夫
大阪大学基礎工学部情報科学科
-
谷口 健一
大阪大学基礎工学部情報科学科
-
森岡 澄夫
大阪大学基礎工学部情報学科
-
東野 輝夫
大阪大学大学院情報科学研究科|独立行政法人科学技術振興機構 Crest
-
柴田 直樹
大阪大学基礎工学部情報工学科
-
森岡 澄夫
大阪大学大学院基礎工学研究科情報数理系専攻:(現)日本アイ・ビー・エム株式会社
-
谷口 健一
大阪大学基礎工学部情報工学科
-
森岡 澄夫
日本電気株式会社システムipコア研究所
関連論文
- 2-III-19 B_補酵素関与エタノールアミンアンモニアリアーゼの立体構造と変異導入に基づく触媒機構の解析(一般演題,日本ビタミン学会第62回大会発表要旨)
- 移動センサノードを用いたデータ収集型WSNでのk重被覆時間の最大化手法
- 指向性アンテナおよび車車間通信を用いた歩行者位置追跡手法とその評価(セッション2)
- 12.B_補酵素関与エタノールアミンアンモニアリアーゼの性質とタンパク質工学的改変および結晶構造解析(第415回研究協議会研究発表要旨,ビタミンB研究委員会)
- 車車間通信による交差点鳥瞰映像ストリーミング手法の提案(セッション2)
- 各車両の予定経路情報を利用した車車間通信による情報取得手法の提案(セッション1)
- 被災地におけるDTNに基づいた情報収集・共有方式の提案(セッション1-C:マルチメディアシステム)
- 2-II-32 エタノールアミンアンモニアリアーゼのタンパク質工学的改変と結晶構造解析および変異導入(一般研究発表,日本ビタミン学会第61回大会研究発表要旨)
- 遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証
- 通信プロトコルのLOTOS仕様から並行EFSM群への変換の一手法
- 遷移の選択が状態訪問回数に依存する有限状態機械対からなる通信系に対する生存性検証システム
- 携帯電話端末への低コスト動画広告配信を目的としたWiFi併用協調ダウンロード方式
- 都市や観光地における混雑状況を考慮した多数ユーザ同時巡回スケジューリング手法
- 無線センサネットワーク長寿命化のためのノード集合の分割に基づくスリープスケジューリング手法
- 無線センサネットワーク長寿命化のためのノード集合の分割に基づくスリープスケジューリング手法
- 天気変化を考慮した観光スケジュール群の探索アルゴリズム
- 利用者の状況に応じて画面レイアウトが変更可能な遠隔教育支援システムの提案
- グループワークを考慮した協調計算システムにおける動作プログラム群の生成と分散実行
- 遷移条件が状態訪問回数に依存する有限状態機械の生存性検証
- 凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
- 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 多面体分割を用いた有理数プレスブルガー文真偽判定アルゴリズムとその実装
- 1G-6 有理数プレスブルガー文真偽判定のための多面体分割を用いたアルゴリズムとその実装
- 冠頭標準形有理数プレスブルガー文の真偽判定アルゴリズムの提案
- 組合わせ幾何を用いた有理数プレスブルガー文真偽判定アルゴリズムにおける投影操作の高速化
- 共有メモリ型並列計算機上での正則な項書換え系の一実装法
- Tarski算術における冠頭標準形の閉論理式の真偽判定アルゴリズムの提案
- 拡張有限状態機械とペトリネットを表示編集できるGUIツールの作成と応用例 (第54回全国大会 (平成9年前期 於 : 千葉工大) 大会優秀賞受賞論文 (11件)
- レジスタ付きペトリネットを用いた全体動作仕様から分散動作仕様の自動合成とその応用 (コンカレント・コラボレーション技術論文小特集)
- レジスタ付き時間ペトリネットで記述された分散システムの時間制約付き全体仕様からその時間制約を満たす各ノードの動作記述の自動導出(並列・分散)
- あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法
- 関係データベースを用いた在庫管理プログラムの記述とその詳細化の正しさの証明
- リンクの故障を考慮に入れた分散システムの動作仕様の自動導出
- ペトリネットモデルを用いたソフトウェアプロセスの記述とその分散実行制御
- レジスタを持つ自由選択ネットで記述された分散システムの要求仕様から各ノードの動作仕様の導出
- 協調計算システムの動作仕様群の分散実行系
- ASLプログラム開発システムにおける検証の自動化について
- 拡張有限状態機械で記述された協調計算プログラムとその実行系
- 順序機械型プログラムの階層的設計法と在庫管理プログラムの開発例
- 拡張有限状態機械モデルを用いた分散システムの要求仕様から各ノードの動作仕様の自動導出
- 部分項の評価順が指定できる項書換え系とその性質について(計算機構とアルゴリズム)
- 代数的言語ASLを用いた酒屋在庫管理の要求仕様記述
- モバイルアンカノードを用いた低コストな水中センサノードの位置推定法
- 移動センサノードを用いたデータ収集型WSNでのk重被覆時間の最大化手法
- 水面を移動可能なアンカーノードを用いた水中センサネットワークのノード位置推定手法の提案
- 天気変化を考慮した観光スケジュール群の探索アルゴリズム
- リクエストに応じた交差点映像配信を目的とした車車間通信プロトコルの提案と評価
- 無線通信網のリンクスケジューリング問題に対する二段階近似解法の提案
- VANET における車両の経路情報を利用した情報伝播プロトコルの提案と評価
- in-order実行パイプラインCPUの正しさの自動証明例
- FDTって何?(コンピュータと通信)
- すべての変数が存在記号で束縛された冠頭標準形プレスブルガー文の真偽判定の高速化手法
- プレスブルガー文真偽判定手続きを用いた算術演算回路の正しさの証明
- プレスブルガー文真僞判定手続きを用いた算術演算回路の正しさの証明
- プレスブルガー文真偽判定手続きにおける多元連立1次合同式の求解処理の高速化
- 時間拡張LOTOSの処理系を用いたSMIL記述の実行とQoS制御
- 時間拡張LOTOSの処理系を用いたSMIL記述の実行とQoS制御
- マルチランデブを用いたLOTOS仕様の実行の可視化 (マルチメディア通信と分散処理)
- LOTOSで記述されたプロトコルの実行の可視化
- イベントとアニメーション表示の対応付けによるLOTOSプログラムの実行の可視化
- 入力が競合する有限状態機械群からなる通信ソフトウェアの適合性試験に一手法
- 複数個のFSMからなるプロトコル機械に対する適合性試験の一手法
- あるクラスの時間オートマトンに対する適合性試験系列生成の一手法(マルチメディア通信と分散処理)
- 並行EFSM群でモデル化された通信プロトコル動作仕様のハードウェア実現とマルチランデブ制御機構
- 代数的手法を用いたCPU KUE-CHIP2の段階的設計の正しさの自動証明
- 代数的手法を用いたパイプライン方式CPUの設計検証
- 代数的手法を用いたCPU KUE-CHIP2の段階的設計およびその正しさの証明
- 代数的言語ASLによる回路設計支援システムにおけるSFL記述への詳細化とその変更及びそれらの正しさの検証
- 交差点鳥瞰映像の協調撮影と共有を目的とした車車間通信プロトコル
- 3D仮想空間を用いた情報家電のためのリモコンフレームワーク
- FORTE/PSTV'97(形式記述技法と通信プロトコルに関する合同国際会議)報告
- プログラムの処理速度調整に基づいたデータセンタ向け省電力タスクスケジューリング法
- 過去に観測された品質からのオーバレイリンク品質の推定手法
- 過去に観測された品質からのオーバレイリンク品質の推定手法
- 出庫予測に基づき入店所要時間を最小化する駐車場ナビゲーションの提案
- ユーザのアクティビティと体重変化履歴に基づいた継続性の高い健康支援手法の提案
- ユーザのアクティビティと体重変化履歴に基づいた継続性の高い健康支援手法の提案
- 駐車待ち所要時間を最小化する駐車場ナビゲーションの提案
- 駐車待ち所要時間を最小化する駐車場ナビゲーションの提案
- 駐車待ち所要時間を最小化する駐車場ナビゲーションの提案
- 過去に観測された品質からのオーバレイリンク品質の推定手法
- 13.B_補酵素関与エタノールアミンアンモニアリアーゼの精密触媒機構と立体化学経路(第423回研究協議会研究発表要旨,ビタミンB研究委員会)
- SumiTag :あまり目立たないARマーカーとGPGPUを利用した読み取り方法
- 過去に観測された品質からのオーバレイリンク品質の推定手法(モバイルコンピューティング,モバイルアプリケーション,ユビキタス通信,モバイルマルチメディア通信及び一般)
- 3Da01 アミド化合物の酵素合成 : 高効率触媒の形成要件(酵素学・酵素工学,一般講演)
- 3Da12 6-アミノヘキサン酸環状二量体加水分解酵素(NylA)の基質結合部位の解析(酵素学・酵素工学,一般講演)
- 2Dp14 ナイロンオリゴマー分解酵素(NylC)の高度耐熱化(酵素学・酵素工学,一般講演)
- 2Dp13 ナイロンオリゴマー加水分解酵素(NylC)の自己分断機構(酵素学・酵素工学,一般講演)
- 穿孔部封鎖処置における歯科用コーンビームCTとマイクロスコープの応用
- ターボブースト・ハイパースレッディングを考慮したマルチコアプロセッサ向けタスクスケジューリング
- 歯内療法領域における歯科用CTを用いた画像診断に関するクリニカルパスの構築
- 12.B_補酵素関与ジオールデヒドラターゼのグリセロールによる不活性化の機構と不活性化抵抗性酵素の再設計(第427回研究協議会研究発表要旨,ビタミンB研究委員会)
- 照明点灯パターンの切り替えによる高精度な屋内位置推定法とその評価(モバイルアドホックネットワーク,モバイル時代を支える次世代無線技術,フィールドセンシング及び一般)
- 4Ca02 ナイロン加水分解酵素(NylC)の耐熱化機構(酵素学,酵素工学/タンパク質工学,一般講演)
- 運転者に対する交通安全支援のための指向性アンテナおよび車車間通信を用いた歩行者の位置推定手法
- 4Ca01 ナイロン加水分解酵素(NylC)前駆体の自己分断に及ぼすアミノ酸置換効果(酵素学,酵素工学/タンパク質工学,一般講演)
- 移動アンカノードを用いた三辺測量による水中センサノードの低コスト位置推定手法
- 2P-045 高解像度X線結晶構造解析を基盤としたナイロン加水分解酵素(NylC)の耐熱化機構の解明(酵素学,酵素工学,一般講演)
- 2P-044 分子動力学シミュレーションによるナイロン加水分解酵素(NylC)の自己分断機構の解析(酵素学,酵素工学,一般講演)
- BalloonNet:無線ネットワークノードを用いた建物包囲型三次元配置手法