複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法

• Item type: SIG Technical Reports(1)
• 公開日: 1997-12-11
• タイトル: 複数の制御部を持つ同期式順序回路に対する不変式の形式的検証法
• タイトル / 言語: en
• タイトル: A Formal Method of Proving Invariants for Synchronous Sequential Circuits with Plural Controllers
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属(英): en
• 著者所属(英): Department of Informatics and Mathematical Sciences, Graduate School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Informatics and Mathematical Sciences, Graduate School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Informatics and Mathematical Sciences, Graduate School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Informatics and Mathematical Sciences, Graduate School of Engineering Science, Osaka University
• 著者名: 齋藤, 義勝; 竹中, 崇; 北道, 淳司; 船曵, 信生
• 著者名(英): Yoshikatsu, Saitoh; Takashi, Takenaka; Junji, Kitamichi; Nobuo, Funabiki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 高位設計ににおける複数の制御部を持つ同期式順序回路を対象とする，不変式の証明を用いた一形式的検証法を提案する．不変式とは設計者あるいは検証者が回路の動作中にレジスタや制御信号などの間に成り立つと考える関係である．回路記述は，複数の有限状態部（制御部）とそれらが制御するデーターパスからなる．不変式は各制御部の任意の有限状態に設定することができる．制御部における実行条件，データパスにおける演算および不変式は，論理型，整数型，ユーザが定義したデータタイプの変数および関数などを用いて記述することができる．検証は，いくつかの不変式，データパス，実行条件，ユーザ定義関数に関する補題を前提として，証明すべき不変式を証明するという，有限状態に関する構造的掃納法を用いて行う．この証明作業は，各制御部と等価な直積制御部を生成しその上で行う．直積制御部の生成時に到達不能な状態の削減をはかる．プレスブルガー文真偽判定ルーチンを利用して，証明すべき式の十分条件を判定する．本手法の有用性をPCIバスインターフェース回路を用いて評価する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we propose a formal method of proving invariants for synchronous sequential circuits with plural controllers in high level design. The invariant is the relationship among registers and signals that the user asserts. The circuit design consists of several finite state machines (controllers) and datapath. The invariants can be set at arbitrary finite states by user. The execution conditions, operations in datapath, and invariants are described with variables and functions over Boolean, integer, and abstract data type defined by user. The invariants are proved on the assumption that several invariants, datapath, execution conditions, and lemmas for user-defined functions are correct. This proof uses the structural induction on finite states. On proving invariants, the system a product controller which is equivalent to each controllers and proves by structural induction with the product controller. We eliminate unreachable states on generating the product controller. The sufficient conditions of expressions to prove are proved with a decision algorithm for the truth of Pres-burger sentence. We evaluate the proposed method for verifying the correctness of the PCI bus interface circuit design.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 1997, 号 119(1997-SLDM-086), p. 41-48, 発行日 1997-12-11
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会