高階述語論理によるハードウェアの構造の形式的検証
スポンサーリンク
概要
- 論文の詳細を見る
本稿では設計されたハードウェアの構造がその動作仕様を満たしているかどうかを検証する方法を提案する.従来の検証法で用いられている一階述語論理は再帰的な表現ができないため,順序回路を含むようなハードウェアを表現できない.本稿では高階述語論理を用いることによってこの問題を解決する.本稿ではまず仕様である動作記述およびその設計である構造記述をそれぞれ高階述語論理式に変換する方法を示す.仕様記述および設計記述を表す論理式から"設計が仕様を満たしている"という意味を表す論理式を作り,この論理式を証明することによって検証を行なう.さらに本稿ではこの論理式を定理証明系を用いて証明する際の手順も示す.
- 社団法人電子情報通信学会の論文
- 1996-12-13
著者
関連論文
- IP高速迂回を実現する迂回可能経路の判別手法(経路制御,NGN管理,サービス管理,ユーザ管理及び一般)
- 動作領域モデルを用いたアナログ回路の解析法
- 入力名標集合と制御条件を用いたレジスタ転送レベルの設計検証法
- ADRによるバス上の多重縮退故障のマスク
- 誤り処理要素を特定可能なFFTの効果的構成法
- 帰納的関数のグラフ表現と設計検証への応用
- オンライン故障診断可能なFFTシステムの構成法
- ADRによるバス上の2重縮退故障のマスク
- 時間冗長方式と巡回符号を用いたバス上の多重縮退故障のマスク
- リンク状態型経路制御における局所更新手法(パラレル,インターネットと情報倫理教育,一般)
- リンク状態型経路制御における局所更新手法(パラレル,インターネットと情報倫理教育,一般)
- リンク状態型経路制御における局所更新手法(パラレル,インターネットと情報倫理教育,一般)
- AS間経路制御安定性向上のためのローカルリルート方式の提案(経路制御,NGN管理,サービス管理,ユーザ管理及び一般)
- ルータクラスタ構成における経路情報共有機構の提案(サービス管理,ビジネス管理,料金管理,及び一般)
- ルータクラスタ構成における経路情報共有機構の提案(サービス管理,ビジネス管理,料金管理,及び一般)
- インターネットチェックサムの2重, 3重誤り検出能力
- ADRを用いてバス上の多重縮退故障をマスクするためのベクトル集合の巡回符号による生成法
- 高階述語論理によるハードウェアの構造の形式的検証
- 時間冗長方式と誤り検出符号を用いたフォールトトレラント組合せ回路
- D-10-17 動作領域モデルを用いたディジタル回路の解析方法
- ローカルエリアネットワークにおけるパケット多重通信の一実験
- 論理合成組合せ回路に対するLFSRによるテスト長
- B-16-7 ID/Locator分離を用いたインターネットデータセンターにおける出力トラフィック制御(B-16.インターネットアーキテクチャ,一般セッション)
- ルータクラスタにおける二重パケット処理冗長方式(インターネット及び一般)
- ルータクラスタにおける二重パケット処理冗長方式(インターネット及び一般)
- IDDQテスト用電流センサ回路
- 電流テストを用いたフリップフロップのテスタビリティ
- D-10-16 アナログ動作を考慮したディジタル回路の簡易CADシステムの開発
- 電流テストを用いたA-Dコンバータの実時間テスト
- 混在信号LSIに対する電流テスト用入力の比較解析
- ヒストグラム法を用いたA/Dコンバータのテスト
- X-Yゾーン法と動作領域モデルを併用したアナログ回路の故障診断(ディペンダブルコンピューティング)
- ランプ電圧印加による信号線オープン故障の検出(非縮退故障モデルテスト, VLSI 設計とテスト及び一般)
- D-10-19 Application of Operation-Region Model to Analog and Mixed-Signal LSI Testing
- D-10-18 内部フィードバックブリッジ故障の故障動作とテスト
- B-6-76 OpenFlowを用いたReactiveな論理ネットワークの形成方法による運用管理の提案(B-6.ネットワークシステム,一般セッション)