A Study on False Negative Reduction on Formal Verification of Logic Circuits

• Project/Area Number: 20700046
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Computer system/Network
• Research Institution: Nagoya University
• Principal Investigator: NAKAMURA Kazuhiro Nagoya University, 大学院・情報科学研究科, 助教 (90335076)
• Project Period (FY): 2008 – 2009
• Project Status: Completed (Fiscal Year 2009)
• Budget Amount: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000); Fiscal Year 2009: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2008: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
• Keywords: VLSI設計技術 / 諭理回路 / 形式的検証 / 順序回路 / フォールスネガティブ / 論理回路 / sequential SAT

Research Abstract

A reducing method of false nagatives on formal verification of sequential circuits with a circuit conversion is developed. In addition to the method, multi time-frame state reduction for accelerating sequential SAT is developed.

Research Products

• [Presentation] 順序回路の形成的検証におけるフォールスネガティブ削減のための回路変換 (2010)
  • Author(s): 成瀬智啓、中村一博、高木一義、高木直史
  • Organizer: 電子情報通信学会・VLSI設計技術研究会
  • Place of Presentation: 沖縄県男女共同参画センター
  • Year and Date: 2010-03-12
• [Presentation] Sequential SATの高速化のためのm-Trieを用いた時間フレームを跨いだ状態併合 (2010)
  • Author(s): 鳥居洸佑、中村一博、高木一義、高木直史
  • Organizer: 電子情報通信学会総合大会
  • Place of Presentation: 東北大学(宮城県)
• [Presentation] 順序回路の形式的検証におけるフォールスネガティブ削減のための回路変換 (2010)
  • Author(s): 尾野紀博、中村一博、高木一義、高木直史
  • Organizer: 電子情報通信学会VLSI設計技術研究会
  • Place of Presentation: 沖縄県男女共同参画センター(沖縄県)
• [Presentation] Sequential SATにおける時間フレームを跨いだ状態併合 (2009)
  • Author(s): 成瀬智啓、中村一博、高木一義、高木直史
  • Organizer: 電子情報通信学会・総合大会
  • Place of Presentation: 愛媛大学
  • Year and Date: 2009-03-18
• [Presentation] Sequential SATにおける時間フレームを跨いだ状態併合 (2009)
  • Author(s): 成瀬智啓、中村一博、高木一義、高木直史
  • Organizer: 電子情報通信学会総合大会
  • Place of Presentation: 愛媛大学(愛媛県)
• [Remarks]
  • URL: http://www.takagi.i.is.nagoya-u.ac.jp/~nakamura/