January 27, 2011: Distinguished Lecturer Seminar Series - Karem Sakallah: "Scalable Formal Hardware Verification Through Automatic Abstraction"

The University of Illinois at Chicago

Department of Computer Science

2010-2011 Distinguished Lecturer Series


Scalable Formal Hardware Verification Through Automatic Abstraction

Karem Sakallah
University of Michigan
Thursday, January 27, 2011
11:00 a.m., Room 1000 SEO


Abstract:

The paradigm of iterative abstraction and refinement has gained momentum in recent years as a particularly effective approach for the scalable verification of complex hardware and software systems. Dubbed counter example-guided abstraction refinement (CEGAR), its power stems from the elimination (i.e., abstraction)of details that are irrelevant to the property being checked and from analyzing any spurious counter examples to pinpoint and add just those details that are needed to refine the abstraction, i.e., to make it more precise. Originally pioneered by Kurshan, it has since been adopted by several researchers as a powerful means for coping with verification complexity. In particular, the use of abstraction-based verification has been thoroughly studied in the context of model checking by Clarke et al. and Cousot and Cousot for over two decades. Later methods by Clarke et al., Das et al. and Jain et al. have successfully demonstrated the automation of abstraction and refinement in the context of model checking for safety properties.

Whereas such a verification paradigm is appealing at a conceptual level, its success in practice hinges on effective automation of the abstraction and refinement steps, as well as the various checking steps requiring sophisticated reasoning. In this talk, I will describe how these issues are addressed by Reveal, an automatic CEGAR-based verification system. Reveal is used to formally verify complex hardware designs, including pipelined microprocessors whose Register-Transfer Level (RTL) descriptions have tens of thousands of Hardware Description Language (HDL) source lines, thousands of signals, and hundreds of thousands of state bits.

Specifically, I will describe Reveal's overall CEGAR flow and its abstraction and refinement algorithms. I will also analyze its behavior and compare its performance on several representative test cases against several existing automatic tools that perform formal verification of hardware, such as VCEGAR, BAT, UCLID, and VIS. For each test case, I will compare a number of methods to model and check the desired properties on the abstract design, including the use of a Satisfiability Modulo Theories (SMT) solver. I will also demonstrate the trade-offs between various refinement options, highlight the types of lemmas generated in the refinement stage, and analyze the idiosyncrasies leading to them. I will conclude with a brief update on the commercialization of Reveal technology and its use in an industrial verification setting.



Brief Bio:

Karem A. Sakallah is Professor of EECS and Associate Chair of CSE at the University of Michigan. Before coming to Michigan he was with Digital Equipment Corporation in Hudson, MA, where he headed the Analysis and Simulation Advanced Development Team. His research spans various aspects of computer-aided design, with emphasis on logic synthesis and verification, and he has made significant contributions in the area of Boolean satisfiability and its application to hardware verification for which he was a co-recipient of the 2009 CAV (Computer-Aided Verification) Award. Dr. Sakallah received the B.E. degree in electrical engineering from the American University of Beirut, and the M.S.E.E. and Ph.D. degrees in electrical and computer engineering from Carnegie Mellon University. He is a fellow of the IEEE.

Host: John Lillis












































 
Copyright 2016 The Board of Trustees
of the University of Illinois.webmaster@cs.uic.edu
WISEST
Helping Women Faculty Advance
Funded by NSF