EVC: A Validity Checker for the Logic of Equality with

Abstract. The property of Positive Equality [2] dramatically speeds up validity checking of formulas in the logic of Equality with Uninterpreted Functions and Memories (EUFM) [4]. The logic expresses correctness of high-level microproces-sors. We present EVC (Equality Validity Checker)—a tool that exploits Positive Equality and other optimizations when translating a formula in EUFM to a proposi-tional formula, which can then be evaluated by any Boolean satisfiability (SAT) procedure. EVC has been used for the automatic formal verification of pipelined, superscalar, and VLIW microprocessors.