Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors

We compare SAT-checkers and decision diagrams on the evaluation of Boolean formulae produced in the formal verification of both correct and buggy versions of superscalar and VLIW microprocessors. The microprocessors are described in a high-level hardware description language, based on the logic of equality with uninterpreted functions and memories (EUFM). The formal verification is done with Burch and Dill’s correctness criterion, using flushing to map the state of the implementation processor to the state of the specification. The EUFM correctness formula is translated to an equivalent Boolean formula by exploiting the property of positive equality, and using the automatic tool EVC. We identify the SAT-checkers Chaff and BerkMin as significantly outperforming the rest of the SAT tools when evaluating the Boolean correctness formulae. We examine ways to enhance the performance of Chaff and BerkMin by variations when generating the Boolean formulae. We reassess optimizations we developed earlier to speed up the formal verification.