Abstract: Counterexample Guided Abstraction Refinement (CEGAR for short) has been shown to be an effective paradigm in a variety of hardware and software verification scenarios. Originally pioneered by Kurshan, it has since been adopted by several researchers as a powerful means for coping with verification complexity. The wide-spread use of such a paradigm hinges, however, on the automation of its abstraction and refinement phases. Without automation, CEGAR requires laborious user intervention to choose the right abstractions and refinements based on a detailed understanding of the intricate interactions among the components of the design being verified. Clarke et al., Jain et al., and Dill et al. have successfully demonstrated the automation of abstraction and refinement in the context of model checking for safety properties of hardware and software systems. In particular, these approaches create a smaller abstract transition system from the underlying concrete transition system and iteratively refine it with the spurious counterexamples produced by the model checker. Clarke et al.'s and Jain et al.'s approaches are additionally based on the extraction of unsatisfiability explanations derived from the infeasible counterexamples to provide stronger refinement of the abstract model and to significantly reduce the number of refinement iterations.

All of these approaches are examples of predicate abstraction which essentially projects the concrete model onto a given set of relevant predicates to produce an abstraction suitable for model checking a given property. In contrast, we have described a methodology for datapath abstraction that is particularly suited for equivalence checking. In this approach, datapath components in behavioral Verilog models are automatically abstracted to uninterpreted functions and predicates while refinement is performed manually using the ACL2 theorem prover.

The use of (near)-minimal explanations of unsatisfiability forms the basis of another class of abstraction methods. These include the work of Gupta et al. and McMillan et al. who employ “proof analysis” techniques to create an abstraction from an unsatisfiable concrete bounded model checking (BMC) instance of a given depth.

In this talk we explore the application of CEGAR in the context of microprocessor correspondence checking. The approach is based on automatic datapath abstraction augmented with automatic refinement using minimal unsatisfiable subset (MUS) extraction. One of our main conclusions is the necessity of basing refinement on the extraction of MUSes from both the abstract and concrete models. Additionally, refinement tends to converge faster when multiple MUSes are extracted in each iteration. Finally, localization and generalization of spurious counterexamples are also shown to be crucial for refinement to converge quickly. We will describe our implementation of these ideas in the Reveal system and discuss the effectiveness of the various refinement options in the verification of a few benchmarks.

Karem Sakallah received the B.E. degree, with distinction, in EE from the American University of Beirut, Lebanon, in 1975, and the M.S.E.E. and Ph.D. degrees in ECE from Carnegie Mellon University, Pittsburgh, in 1977 and 1981, respectively. In 1981 he joined the Department of EE at CMU as a visiting assistant professor. From 1982 to 1988 he was with Digital Equipment Corporation in Hudson, Massachusetts, where he headed the Analysis and Simulation Advanced Development team. Since 1988 he has been at the University of Michigan as professor of electrical engineering and computer science. He served as associate editor of the IEEE Transactions on CAD during 1995-1997, and has served on the program committees of ICCAD, DAC, ICCD, and numerous other workshops. He is currently an associate editor of the IEEE Transactions on Computers, and a member of the technical program committees of the International Workshop on Logic Synthesis and the Workshop on the Theory and Practice of Timed Systems. He has published more than 120 papers, and has presented seminars and tutorials at many professional meetings and various industrial sites. He is a fellow of the IEEE and a member of ACM and Sigma Xi.