Robert Brayton

Title:  ABC: An academic "industrial-strength" verification tool
Date:  April 28, 2011, at 3 p.m., in SF1105

About 6 years ago, ABC was started as a replacement for our synthesis tool SIS. As part of this development, we needed to put together an equivalence checker for assuring that synthesis algorithms had been implemented correctly. Some of the new synthesis algorithms in ABC involve scalable sequential operations, such as retiming and sequential SAT sweeping, which yield impressive results. A companion scalable sequential equivalence checker (SEC) was needed and developed. The resulting SEC engine was more general and is a powerful property as well. The verification part of ABC was packaged and submitted it to the model checking competitions of CAV’08, at which it won in 2 of 3 categories and at CAV’10 it won again in 2/3 categories.

Working on both synthesis and verification has allowed us to borrow ideas from the best of both worlds and to observe the growing synergy between the two areas. This synergy works in two directions; the ability to synthesize large problems and show impressive gains spurs on development of equivalently scalable SEC methods and the ability to scalably verify sequential equivalence problems spurs on the development, use, and acceptance of some sequential synthesis methods. In ABC, similar concepts and algorithms are used in both synthesis and verification, e.g. use of AIGs, rewriting, use of SAT, sequential SAT sweeping, retiming, and interpolation.

In this talk, we will provide an overview of ABC, discuss some ways in which synthesis and verification ideas have influenced each other, and illustrate how various algorithms have been assembled and employed to create a powerful model checking engine that can rival some commercial offerings.

Bio: Robert Brayton received the BSEE degree from Iowa State University in 1956 and the Ph.D. degree in mathematics from MIT in 1961. He was a member of the Mathematical Sciences Department of the IBM T. J. Watson Research Center until he joined the EECS Department at Berkeley in 1987. He held the Edgar L. and Harold H. Buttner Endowed Chair and retired as the Cadence Distinguished Professor of Electrical Engineering at Berkeley.

He is a member of the US National Academy of Engineering and has received the following awards: IEEE Emanuel R. Piore (2006), ACM Kanallakis (2006), European DAA Lifetime Achievement (2006), EDAC/CEDA Phil Kaufman (2007), D.O. Pederson best paper in Trans. CAD (2008), ACM/IEEE A. Richard Newton Technical Impact in EDA (2009), and Iowa State University Distinguished Alumnus (2010).  He has authored over 450 technical papers, and 10 books in the areas of the analysis of nonlinear networks, simulation and optimization of electrical circuits, logic synthesis, and formal design verification.