CEGAR+SMT: Formal Verification of Control Logic in the Reveal System

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 CounterExample-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 counterexamples 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 [9], 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. [3] and Cousot and Cousot [4] for over two decades. Later methods by Clarke et al. [2], Das et al. [5] and Jain et al. [8] 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 [8], BAT [10], UCLID [1], and VIS [7]. 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 [6]. 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.

Acknowledgments

This presentation summarizes the doctoral dissertation of Zaher S. Andraus. The Reveal system also relies on extraction of minimal explanations of infeasibility which are based on the doctoral dissertation of Mark H. Liffiton.

References

1. R. Bryant, S. Lahiri, and S. Seshia. Modeling and verifying systems using a logic of counter arithmetic with Lambda expressions and uninterpreted functions. In Proc. of Int'l Conference on Computer-Aided Verification, LNCS 2404, pages 78-92, 2002.
2. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction renement. In Proc. of Int'l Conference on Computer-Aided Verification, pages 154-169, 2000.
3. E. Clarke, O. Grumberg, and D. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(5):1512-1542, 1994.
4. P. Cousot and R. Cousot. Abstract interpretation: a unied lattice model for static analysis of programs by construction or approximation of xpoints. In Conference Record of the Sixth Annual ACM SI PLAN-SIGACT Symposium on Principles of Programming Languages, pages 238-252, 2006.
5. S. Das and D. Dill. Successive approximation of abstract transition relations. In IEEE Symposium on Logic in Computer Science, pages 51-58. 2001.
6. B. Dutertre and L. de Moura. A fast linear arithmetic solver for DPLL(T). In Proc. of Int'l Conference on Computer-Aided Verification, LNCS 4144, pages 81-94, 2006.
7. R. Brayton et al. VIS: a system for vercation and synthesis. In Proc. of Int'l Conference on Computer-Aided Verification, LNCS 1102, pages 428-432, 1996.
8. H. Jain, D. Kroening, N. Sharygina, and E. Clarke. Word-level predicate abstraction and renement for verifying rtl Verilog. In Proc. of Design Automation Conference, pages 445-450, 2005.
9. R. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1999.
10. P. Manolios, S. Srinivasan, and D. Vroon. Automatic memory reductions for RTL model verication. In Proc. of Int'l Conference on Computer-Aided Design, pages 786-793, 2006.

Karem Sakallah, University of Michigan, Ann Arbor, USA

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 is a co-founder of Reveal Design Automation, Inc., a start-up based in Ann Arbor, Michigan, that provides Architectural Verification solutions to the microelectronics industry. He 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.