Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas

Abstract

This paper deals with equivalence checking of high-level hardware design descriptions. For this purpose, we propose a method based on validity checking of the quantifier-free first-order logic with equality, combined with boolean validity checking. Since, in the first-order logic, arithmetic functions or inequalities can be abstractly represented by function or predicate symbols, its validity checking becomes more efficient than boolean-based one. The logic, however, ignores the original semantics of the function or predicate symbols. For example, the commutative law over addition cannot be handled. As a result, the verification results are often ‘false negative’. To overcome this difficulty, we propose an algorithm based on replacement of the function or predicate symbols with vectors of boolean formulas. To avoid replacing the entire original first-order formula with boolean functions, the algorithm utilizes counterexamples obtained from validity checking for the first-order logic. This paper also reports a preliminary experimental result for equivalence checking of high-level descriptions by a prototype implementation of the proposed algorithm.