Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints(Logic Synthesis and Verification,<Special Section>VLSI Design and CAD Algorithms)

スポンサーリンク

概要

• 論文の詳細を見る

• For formal verification of large-scale digital circuits, a method using satisfiability checking of logic with equality and uninterpreted functions has been proposed. This logic, however, does not consider specific properties of functions or predicates at all, e.g. associative property of addition. In order to ease this problem, we introduce "equivalence constraint" that is a set of formulas representing the properties of functions and predicates, and check the satisfiability of formulas under the constraint. In this report, we show an algorithm for checking satisfiability with equivalence constraint and also experimental results.

• 社団法人電子情報通信学会の論文
• 2007-12-01

著者

• Hamaguchi Kiyoharu

  Graduate School Of Infomation Science And Technology Osaka University

• Kashiwabara Toshinobu

  Graduate School Of Infomation Science And Technology Osaka University

• KOZAWA Hiroaki

  Graduate School of Infomation Science and Technology, Osaka University

• Kozawa Hiroaki

  Graduate School Of Infomation Science And Technology Osaka University

関連論文

• Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints(Logic Synthesis and Verification,VLSI Design and CAD Algorithms)

スポンサーリンク