IEICE TRANSACTIONS on Fundamentals
Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E90-A No.12 pp.2778-2789
- Publication Date
- 2007/12/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1093/ietfec/e90-a.12.2778
- Type of Manuscript
- Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
- Category
- Logic Synthesis and Verification
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Hiroaki KOZAWA, Kiyoharu HAMAGUCHI, Toshinobu KASHIWABARA, "Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints" in IEICE TRANSACTIONS on Fundamentals,
vol. E90-A, no. 12, pp. 2778-2789, December 2007, doi: 10.1093/ietfec/e90-a.12.2778.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e90-a.12.2778/_p
Copy
@ARTICLE{e90-a_12_2778,
author={Hiroaki KOZAWA, Kiyoharu HAMAGUCHI, Toshinobu KASHIWABARA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints},
year={2007},
volume={E90-A},
number={12},
pages={2778-2789},
abstract={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.},
keywords={},
doi={10.1093/ietfec/e90-a.12.2778},
ISSN={1745-1337},
month={December},}
Copy
TY - JOUR
TI - Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2778
EP - 2789
AU - Hiroaki KOZAWA
AU - Kiyoharu HAMAGUCHI
AU - Toshinobu KASHIWABARA
PY - 2007
DO - 10.1093/ietfec/e90-a.12.2778
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E90-A
IS - 12
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - December 2007
AB - 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.
ER -
English
