Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints

Hiroaki KOZAWA; Kiyoharu HAMAGUCHI; Toshinobu KASHIWABARA

doi:10.1093/ietfec/e90-a.12.2778

Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints

Hiroaki KOZAWA, Kiyoharu HAMAGUCHI, Toshinobu KASHIWABARA

Full Text Views

0

Share
Cite this

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

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://globals.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 -