Inductive Invariantでの効率的フリップフロップ選択による形式的検証とその応用

• Item type: SIG Technical Reports(1)
• 公開日: 2022-03-03
• タイトル: Inductive Invariantでの効率的フリップフロップ選択による形式的検証とその応用
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 設計技術
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京大学大学院工学系研究科
• 著者所属: 東京大学大学院工学系研究科
• 著者名: 小池, 良吾; 藤田, 昌宏
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 近年では論理回路の設計が大規模化し，設計を数学的に検証する形式的検証技術はより重要な技術になっている．その形式的検証技術の 1 つに順序回路の到達可能性を解析する Inductive Invariant がある．Inductive Invariant では特定のフリップフロップの集合に対して，順序回路が到達可能状態を計算することができる．Inductive Invariant では回路が持つすべてのフリップフロップからその一部を対象として計算を行うことで得られる状態は到達可能状態の上位集合となる．このようにすることで真の到達可能状態を計算するよりも計算量を抑えて解析を行うことが可能である．ここで計算の対象とするフリップフロップによって計算される到達可能状態の上位集合の大きさが変化する．本論文ではこのフリップフロップの選択方法を効率的に探索するアルゴリズムを提案し，またその計算量を削減する方法を提案した．提案手法はまずフリップフロップを選択する問題を QBF 問題として定式化し，それをインクリメンタルに解くことによって効率的な探索を可能にした．また Inductive Invariant の応用として計算された到達不可能な状態を利用して回路を最適化する方法を提案した．いずれの手法に関しても実験によって有効性を確認した．
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA12149313
• 書誌情報: 研究報告組込みシステム（EMB）; 巻 2022-EMB-59, 号 29, p. 1-9, 発行日 2022-03-03
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-868X
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会