In this paper, we explore the application of counter-example-guided abstraction refinement (CEGAR) in the context of microprocessor correspondence checking. The approach utilizes automatic datapath abstraction augmented with automatic refinement based on 1) localization, 2) generalization, and 3) minimal unsatisfiable subset (MUS) extraction. We introduce several refinement strategies and empirically evaluate their effectiveness on a set of microprocessor benchmarks. The data suggest that localization, generalization, and MUS extraction from both the abstract and concrete models are essential for effective verification. Additionally, refinement tends to converge faster when multiple MUses are extracted in each iteration.

Abstraction plays a critical role in verifying complex sys-tems. A number of languages have been proposed to model hardware systems by, primarily, abstracting away their wide datapaths while keeping the low-level details of their control logic. This leads to a significant reduction in the size of the state space and makes it possible to verify intricate control interactions formally. These languages, however, require that the abstraction be done manually, a tedious and error-prone process. In this paper we describe Vapor, a tool that auto-matically abstracts behavioral RTL Verilog to the CLU lan-guage used by the UCLID system. Vapor performs a sound abstraction with emphasis on minimizing false errors. Our method is fast, systematic, and complements UCLID by serving as a back-end for dealing with UCLID counterexamples. Preliminary results show the feasibility of automatic abstraction and its utility in formal verification.

This paper describes a new algorithm for extracting unsatisfiable subformulas from a given unsatisfiable CNF formula. Such unsatisfiable cores can be very helpful in diagnosing the causes of infeasibility in large systems. Our algorithm is unique in that it adapts the learning process of a modern SAT solver to identify unsatisfiable subformulas rather than search for satisfying assignments. Compared to existing approaches, this method can be viewed as a bottom-up core extraction procedure which can be very competitive when the core sizes are much smaller than the original formula size. Repeated runs of the algorithm with different branching orders yield different cores. We present experimental results on a suite of large automotive benchmarks showing the performance of the algorithm and highlighting its ability to locate not just one but several cores.