複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法 (<特集>機能論理設計, アーキテクチャ設計支援と一般)

• 齊藤 義勝

  大阪大学大学院基礎工学研究科情報数理系専攻

• 竹中 崇

  大阪大学大学院基礎工学研究科情報数理系専攻

• 北道 淳司

  大阪大学大学院基礎工学研究科情報数理系専攻

• 船曵 信生

  大阪大学大学院基礎工学研究科情報数理系専攻

書誌事項

タイトル別名

• A Formal Method of Proving Invariants for Synchronous Sequential Circuits with Plural Controllers

抄録

高位設計における複数の制御部を持つ同期式順序回路を対象とする, 不変式の証明を用いた一形式的検証法を提案する. 不変式とは設計者あるいは検証者が回路の動作中にレジスタや制御信号などの間に成り立つと考える関係である. 回路記述は, 複数の有限状態部 (制御部) とそれらが制御するデータパスからなる. 不変式は各制御部の任意の有限状態に設定することができる. 制御部における実行条件, データパスにおける演算および不変式は, 論理型, 整数型, ユーザが定義したデータタイプの変数および関数などを用いて記述することができる. 検証は, いくつかの不変式, データパス, 実行条件, ユーザ定義関数に関する補題を前提として, 証明すべき不変式を証明するという, 有限状態に関する構造的帰納法を用いて行う. この証明作業は, 各制御部と等価な直積制御部を生成しその上で行う. 直積制御部の生成時に到達不能な状態の削減をはかる. プレスブルガー文真偽判定ルーチンを利用して, 証明すべき式の十分粂件を判定する. 本手法の有用性をPCIバスインターフェース回路を用いて評価する.

収録刊行物

• 情報処理学会研究報告. 設計自動化研究会報告

  情報処理学会研究報告. 設計自動化研究会報告 97 (119), 41-48, 1997-12-11

  一般社団法人情報処理学会

詳細情報

• CRID: 1571135651992437120
• NII論文ID: 110004028417
• NII書誌ID: AN1011091X
• 本文言語コード: ja
• データソース種別:
  • CiNii Articles