Abstract: Counterexample Guided Abstraction Refinement (CEGAR) 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 the stages, without which 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. These approaches are based on predicate abstraction which projects the concrete model onto a set of relevant predicates to produce an abstraction suitable for model checking a given property.

In this talk we describe a methodology for datapath abstraction that is particularly suited for equivalence checking. Datapath components in behavioral Verilog models are automatically abstracted to uninterpreted functions and predicates, verification is then performed with a powerful Satisfiability Modulo Theories (SMT) solver, and refinement is performed automatically based on counterexamples and minimally unsatisfiable cores.

Zaher Andraus earned his B.sc. in Computer Engineering from Technion (Haifa, Israel) in '02, and his M.sc. in Computer Science and Engineering from the University of Michigan (Ann Arbor) in '04. He is currently a Ph.D. candidate at the University of Michigan, and works with Prof. Karem Sakallah on Microprocessor Verification. His thesis has recently won 2nd place in the CSE Student Honors Competition at the University of Michigan. He was also ranked 3rd in the CADathlon competition held in California in '04, and co-authored a paper on SAT that was nominated best paper in DAC the same year. His research interests include Satisfiability Algorithms, Timing Analysis, and Software and Hardware Verification. Since 2000, he has been collaborating with Synopsys and Intel on solving industrial EDA challenges. Appointments: dcm@cs.cmu.edu